Comments on the user interface page

[herbelin]

Hi, A few months ago, I wrote these comments on the page https://coq.inria.fr/user-interfaces.html. Considering the discussion started at https://coq.zulipchat.com/#narrow/stream/237661-User-interfaces-devs-.26-users/topic/Is.20there.20any.20supported.20IDE.20for.20Coq.20these.20days.3F, I make them public.

1. I would move jscoq (currently in "Standalone interfaces") in a different box entitled e.g. "Coq in the browser" or "online web interface" since it seems to be of a different nature and purpose than "standalone interfaces".
2. The JsCoq text does not look accurate: " However, it is too limited to conduct actual projects: it lacks access to the VM and native computing machineries of Coq, and may hit out-of-memory and stack-overflow failures quicker than native versions of Coq "? (At least, I thought the out-of-memory and stack-overflow failures were addressed.)
3. For coq-lsp: mention the historical role of Isabelle/JEdit, besides the reference to Lean? also: continous -> continuous
4. It would be clearer to me if what is about the underlying technology is separated from what is useful for end users. For instance, in terms of technology, what seems relevant is:
   • editor plugin / standalone / in the browser (note: this difference is already done for editor/standalone)
   • the interaction model: evaluation has to be done "explicitly" (using explicit navigation commands, as in coqide, PG, vscoq1, vscoq2) or it is done "implicitly" (continuous evaluation, implicitly following the cursor, as in coq-lsp)
   • where the UI features are implemented (in the server, or the client, or Coq) and how the communication with Coq works, typically:
     • Proog General:
       • the graphical part of the features are implemented in emacs (elisp)
       • communication is using textual commands to coqtop (so the Coq API is the one of coqtop commands)
       • the semantic part of the features are either provided by Coq commands (e.g. implicit arguments, searching, etc.) or written in elisp in Proof General (e.g. memoizing the proof steps)
     • CoqIDE (resp. coqtail, - and also vscoq1?) rely on coqidetop which is an extension of coqtop providing not only textual command (like in PG) but specific structured data (e.g. goals) obtained using the OCaml API of Coq
       • the semantic part of the features are implemented in Coqide (resp. coqtail, vscoq1) using OCaml (resp. typescript, vim scripting language), or sometimes provided by Coq commands (as above)
       • the graphical part of the features are provided by a specific GUI calling the lablgtk ocaml bindings to gtk+3 (resp. provided by VsCode editor, Vim editor)
       • the protocol is an XML-based syntax to transfer structured data (e.g. goals as a list) between coqidetop (= coq + the communication protocol) and coqide/coqtail/vscoq1
     • vscoq2 (resp coq-lsp):
       • LSP-standardized features are natively supported by the editor (e.g. hovering, right-click, completion, ...)
       • the GUI part of extra features have to be implemented in the editor (e.g. typescript for vscode)
       • the semantic part of the LSP-standard features are implemented in a server talking with the GUI using the LSP protocol (sometimes provided by Coq commands as above)
       • LSP is extensible and the semantic part of the extra features are in the server; the server itself is typically an OCaml-based extension of coqtop

PS: I can make a PR depending on comments.

[ejgallego]

1. I would move jscoq (currently in "Standalone interfaces") in a different box entitled e.g. "Coq in the browser" or "online web interface" since it seems to be of a different nature and purpose than "standalone interfaces".

Sounds good to me, tho note that the barriers between web and desktop are blurring, jsCoq 2.0 is coq-lsp compiled for the web with a different package manager and editor. The coq-lsp vsCode extension does work on their web enviroment pretty good already, and that is basically almost the same.

2. The JsCoq text does not look accurate: " However, it is too limited to conduct actual projects: it lacks access to the VM and native computing machineries of Coq, and may hit out-of-memory and stack-overflow failures quicker than native versions of Coq "? (At least, I thought the out-of-memory and stack-overflow failures were addressed.)

Yes, it is outdated. The production version is much better, but indeed limited for "industrial" scale mainly due to speed / memory and of course less packages.

3. For coq-lsp: mention the historical role of Isabelle/JEdit, besides the reference to Lean? also: continous -> continuous

That's a good one. coq-lsp does indeed owe way more to Isabelle and Makarius than to Lean.

4. It would be clearer to me if what is about the underlying technology is separated from what is useful for end users. For instance, in terms of technology, what seems relevant is:

Indeed it could be useful to do a kind of matrix, but that's also quite a lot of work and hard to keep updated.

[Zimmi48]

Sounds good Hugo, and I'm happy to review a PR from you. I think the distinction you want to make is sensible. I would just avoid going too much into the technical / implementation details on this page. Perhaps, it should be on another page (like a wiki page) that would be linked from this page. But this user-interfaces page should really be focused on answering the question "Which interface do I use?" from users.

Some specific responses:

the interaction model: evaluation has to be done "explicitly" (using explicit navigation commands, as in coqide, PG, vscoq1, vscoq2) or it is done "implicitly" (continuous evaluation, implicitly following the cursor, as in coq-lsp)

Note that VsCoq2 has the two modes available.

Emilio said:

Sounds good to me, tho note that the barriers between web and desktop are blurring, jsCoq 2.0 is coq-lsp compiled for the web with a different package manager and editor. The coq-lsp vsCode extension does work on their web enviroment pretty good already, and that is basically almost the same.

In coq/ceps#68 (comment), you said jsCoq is another STM user. I guess there you meant jsCoq 1 as opposed to jsCoq 2?

[ejgallego]

Yes @Zimmi48 I mean jsCoq "2" which has its own branch here https://github.com/jscoq/jscoq/tree/v8.16+lsp (it was fully functional at some stage, but now needs a rebase)

[Zimmi48]

@herbelin Don't forget to submit your PR before you leave. Even if imperfect, what you currently have will anyway be an improvement over the current state.

[herbelin]

@Zimmi48: I submitted a PR. Following discussions with a few people (including you), it differs from the head message of the issue by the following:

• The technical part 4. is done in a wiki page: https://github.com/coq/coq/wiki/Basic-architecture-of-Coq-User-Interfaces.
• Rather than adding a box distinguishing interfaces in the browser, it is a box for commonly used interfaces today (whether it is about via an editor, a standalone UI, or the browser), a box for UIs under development, and a box for other UIs.

[herbelin]

BTW: is there a way to render the page changed by the PR?

[Zimmi48]

I use:

make
make run