Add vscoq-language-server to the platform

[gares]

We would like to have the vscoq 2 language server to be integrated in the platform. CC the others authors: @maximedenes @rtetley

vscoq2 main branch is currently tested in Coq's CI, see https://github.com/coq/coq/pull/17678 .

Once the .dev packages is added to the extra-dev opam repo (pr in progress: https://github.com/coq/opam-coq-archive/pull/2606 ) I'll propose here a PR adding the package (and exposing one more binary vscoqtop from the snap). So far we have no release for 8.17, ad we do not plan to have one. The first one will target 8.18.

About the smoke test kit, I'm a bit unsure what to propose. We do have end to end tests (xvfb, mocha, node, vscode ...) in our CI, but that is a bit heavy to add here, and in any case it would not fix the current framework. But I could make a separate CI job firing up vscode under xvfb and just checking the language server is found and runs. What do you think?

[rtetley]

@gares what is the status on this ? Is there work to be done for the merge to pass ? We need to move fast to be included in the next release

[gares]

My guess is that the platform maintainers / editorial board should consider all issues with label "package inclusion" from time to time.

See also https://github.com/coq/platform/pull/348#issuecomment-1617509353 by @MSoegtropIMC

[gares]

If you have the time, we need something in the smoke test kit.

At least check that coq-prover.vscoqtop --help executes fine (on snap) and vscoqtop.exe --help on windows and something similar on OSX. We may also want to ask for an alias on the snap store, so to elide the coq-prover. prefix, see https://github.com/coq/platform/blob/main/doc/README_Linux.md#aliases . Since it takes some days, we may act now for this one.

[MSoegtropIMC]

@gares : just a note: the smoke test kit does not use the aliases, but uses a direct path to the coqc binary. See:

create_smoke_test_kit.sh

The main reason is that this requires fewer changes to the script. It should be fine to test everything else this way as well, but it would of course also make sense to test the aliases. Maybe one should add a run time option to the smoke test script to either use the (hacky) direct path or the aliases.

IMHO when we want the aliases to be used, we should at least make sure that the coq_makefile template does support this. Otherwise many (to most) snap users will use the direct path method. That the direct path method works is btw. an effect of that the situation of a snap used this way is quite similar to what happens on Windows and macOS.