Paolo Giarrusso (Dec 23 2022 at 06:51): Paolo Giarrusso (Dec 23 2022 at 06:51):I've seen references to both names, are they the same? I've seen hints they might be different ideas
Huỳnh Trần Khanh (Dec 23 2022 at 07:35):1 thing I know for sure: if vscoq2 does exist, it only exists in the form of a top secret repository only accessible to a few community members. but I guess vscoq2 uses coq-lsp, and the vscode extension provided by coq-lsp is extremely bare bones just for testing. now, I have nothing to back up my claims, and I hope community members could correct me if I'm wrong
Théo Zimmermann (Dec 23 2022 at 09:49):No, nothing is secret. The two projects stem from the same initial ideas but are independent and moving in parallel (which is not ideal, but reasons...). coq-lsp is https://github.com/ejgallego/coq-lsp (with its own VS Code extension) and the efforts on VsCoq2 have been happening mostly on the server part at https://github.com/maximedenes/vscoq/tree/document-manager and lately also on the client part at https://github.com/coq-community/vscoq/tree/vscoq2. The VsCoq2 roadmap is https://github.com/coq-community/vscoq/wiki/VsCoq-1.0-Roadmap. (It was called VsCoq 1.0 at the time it was written, I don't know why the name change to VsCoq2).
Enrico Tassi (Dec 23 2022 at 10:36):@Maxime Dénès I think I chose 1 since we are at 0.x ... but maybe 2.0 is better since it is a new iteration
Maxime Dénès (Dec 23 2022 at 11:07):I expect that we have to publish both extensions in parallel for some time. I found VsCoq & VsCoq2 more natural than VsCoq & VsCoq1.
Maxime Dénès (Dec 23 2022 at 11:07):(to support older Coq versions)
Karl Palmskog (Dec 23 2022 at 12:35):maybe also relevant, a presentation on coq-lsp: https://youtu.be/SsfvmFjUIrI
Karl Palmskog (Dec 23 2022 at 12:36):also, I think we should try to get across to users that both coq-lsp and vscoq2 will be specific to Coq 8.16+ (no backwards compatibility)
Last updated: Jun 04 2023 at 23:30 UTC