I've seen references to both names, are they the same? I've seen hints they might be different ideas
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
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).
@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
I expect that we have to publish both extensions in parallel for some time. I found VsCoq & VsCoq2 more natural than VsCoq & VsCoq1.
(to support older Coq versions)
maybe also relevant, a presentation on coq-lsp: https://youtu.be/SsfvmFjUIrI
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