Does anyone have proposals or wishes for topics / speakers / demos for a next Coq UI discussion?
(One that comes to mind for me is a deeper dive into the status and plans of the JsCoq team, maybe inviting some additional folks to join us from that part of the world. Another is an update on VSCoq, now that version 2 is actually out in the world.)
I cc @Shachar Itzhaky ; thanks @Benjamin Pierce .
Maybe it is too early to ask, in the sense that a first step could be to hear about VsCoq 2, but I'd be interested at some time to learn about the internals of UI, such as 1) what an LSP for proof assistants looks like (e.g. can we specify precisely the kind of extension needed to support proof assistants) 2) what a server for such LSP extension looks like (e.g. is its API fully specified by LSP or does it have to include other components) 3) eventually to understand how LSP compares to other protocols (e.g. Jupyter if ever the question makes sense).
I am a bit confused. Is VsCoq 2 the version that is using coq-lsp or is it the competing implementation that is a revival of the legacy VsCoq?
VsCoq2 is the "competing" implementation, yes.
yeah ok so really what @Hugo Herbelin wants to hear about is coq-lsp and the corresponding VSCode plugin
My understanding is that VsCoq 2 denotes both an LSP server (called VsCoq's vscoqtop server on the Coq web page) and a VsCoq client communicating with this server. It is developed in the same repository as legacy VsCoq (now renamed VsCoq 1). It is a different implementation than coq-lsp.
[It is Benjamin that initially suggested having an update about VsCoq2.]
I think @Hugo Herbelin may want to learn a bit more abstractly; both VsCoq 2 and coq-lsp use LSP + some extensions these days. VsCoq 1 vs VsCoq 2 is a bit confusing in the sense is a full reimplementation more than a "revival", little was preserved from the old implementation (in fact coq-lsp took some files from vsCoq as documented in the license / history) So VsCoq 1 vs 2 only share the name and the project page
Terminologically-speaking, there is the same overloading of concepts in coq-lsp which may refer either to the LSP server or to the VScode extension connecting to this server.
Yes, I'd like to learn a bit more abstractly what implementing LSP for a proof assistant means, independently of one or the other implementation.
Hugo Herbelin said:
Terminologically-speaking, there is the same overloading of concepts in coq-lsp which may refer either to the LSP server or to the VScode extension connecting to this server.
I agree Hugo, tho we are trying to imitate Isabelle (again) and use coq-lsp/VSCode
as to improve the situation.
nitpick: some of us use VSCodium and not VS Code...
We seem to have consensus that the group would be interested in hearing about JSCoq and/or an update about VSCoq 2. Do we have speakers that would be ready and willing to address these topics in a few weeks?
We'd love to do a jsCoq presentation but we jsCoq devs need to sync to see if that's feasible for us for the next meeting.
I'm not sure if they are ready to present, but maybe work by @Bhakti Shah and @Ambroise Lafont on graphical editors for Coq could be also interesting for the meeting?
I’d be happy to present although I’m not sure how much interest there will be because it’s quite domain specific :)
Hi ! Sorry for the late reply, I'm happy to give an update on VsCoq 2 :-)
Last updated: Oct 13 2024 at 01:02 UTC