Benjamin Pierce (Oct 05 2023 at 13:35): Benjamin Pierce (Oct 05 2023 at 13:35):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.)
Emilio Jesús Gallego Arias (Oct 06 2023 at 13:14):I cc @Shachar Itzhaky ; thanks @Benjamin Pierce .
Hugo Herbelin (Oct 06 2023 at 17:32):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).
Shachar Itzhaky (Oct 06 2023 at 17:49):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?
Théo Zimmermann (Oct 06 2023 at 18:27):VsCoq2 is the "competing" implementation, yes.
Shachar Itzhaky (Oct 06 2023 at 18:28):yeah ok so really what @Hugo Herbelin wants to hear about is coq-lsp and the corresponding VSCode plugin
Hugo Herbelin (Oct 06 2023 at 18:29):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.
Théo Zimmermann (Oct 06 2023 at 18:29):[It is Benjamin that initially suggested having an update about VsCoq2.]
Emilio Jesús Gallego Arias (Oct 06 2023 at 18:30):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
Hugo Herbelin (Oct 06 2023 at 18:32):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.
Hugo Herbelin (Oct 06 2023 at 18:35):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.
Emilio Jesús Gallego Arias (Oct 06 2023 at 18:38):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.
Karl Palmskog (Oct 06 2023 at 18:40):nitpick: some of us use VSCodium and not VS Code...
Benjamin Pierce (Oct 11 2023 at 16:11):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?
Emilio Jesús Gallego Arias (Oct 11 2023 at 16:56):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?
Bhakti Shah (Oct 13 2023 at 04:43):I’d be happy to present although I’m not sure how much interest there will be because it’s quite domain specific :)
Romain Tetley (Oct 24 2023 at 07:56):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