Stream: VsCoq devs & users

Topic: coq-lsp and the vscoq2 roadmap


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Maxime Dénès (Dec 23 2022 at 11:07):

(to support older Coq versions)

view this post on Zulip Karl Palmskog (Dec 23 2022 at 12:35):

maybe also relevant, a presentation on coq-lsp: https://youtu.be/SsfvmFjUIrI

view this post on Zulip 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: May 18 2024 at 10:02 UTC