Open herbelin opened 1 year ago
- 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.
- 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.
- 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.
- 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.
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 https://github.com/coq/ceps/pull/68#discussion_r1235370659, you said jsCoq is another STM user. I guess there you meant jsCoq 1 as opposed to jsCoq 2?
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)
@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.
@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:
BTW: is there a way to render the page changed by the PR?
I use:
make
make run
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.
PS: I can make a PR depending on comments.