Add coq-lsp to Coq Platform

[ejgallego]

Dear Coq Platform maintainers, this is to inform you that I'd like to add coq-lsp to the 8.16, 8.17, and dev set of packages. I'd be happy to prepare a 8.15 version if a release is planned.

Thanks to @jim-portegies for the feedback, I have tested coq-lsp to work fine on Windows, starting with the 0.1.6 release. There are a couple of issues to solve in order to get a smooth Windows experience tho:

Related issues:

• [windows] Newer SerAPI versions fail to build to path length limit #331
• [windows] findlib is not initalized correcty when called from coq-lsp #332
• [windows] Platform binaries can't find libgmp-10.dll when called from a native app #333

After all the above are fixed, I'm happy to report coq-lsp runs pretty well!

Other relevant issues / PRs:

• [extra-dev] coq-lsp for Coq 8.17+rc1 opam#2432
• [ci] Add coq-lsp to CI coq#16964

[ejgallego]

The depending PRs are ready / merged, thus I'm requesting inclusion, IIUC the guide states 4 TODO points:

• Packages are typically included on user request via a github issue.

This issue should work.

• Requests should contain a justification.

coq-lsp is of help to IDE users (VS Code client exists, server is usable within the standard) , moreover, coq-lsp is posed to replace SerAPI and sertop, so making testing easy is IMHO important.

• The author(s) or current maintainer(s) of the package shall agree to the inclusion of their package in the Coq Platform. This means that they agree to put reasonable effort into releasing a version of the package compatible with each new Coq release shortly after every Coq release and to maintain some relative stability between each release. The agreement of the authors is given via a comment in the respective github issue.

I agree and commit to all of this.

• All the dependencies of a platform package are also officially part of the platform.

That's the case now (serlib being the only annoying dep, and is already there).

[ejgallego]

Additionally, if you tell me which file to touch (sorry I couldn't manage to figure this out today) I'll be happy to do the pull request myself.

[ejgallego]

Thanks @Zimmi48 for both the suggestion to do this and the help with setting the right meta-data.

We have discussed a bit on the coq-lsp side and we think 0.1.4 (or 0.2.0) should offer the right compatibility story for the 8.17 release, so that's the version we will target for inclusion.

The main compatibility story is that client and server need to agree on the (only important) extension our LSP has, the goals request.

We have now a plan that should handle different versions reasonably.

[ejgallego]

Hi @MSoegtropIMC , is there any hope to include coq-lsp in the 2023.03 platform?

[ejgallego]

Dear @MSoegtropIMC , any update on this?

[MSoegtropIMC]

It is included in 2015.01, both in the 8.20 pick and the 8.19 pick.

Sorry forgot to close.

[MSoegtropIMC]

Hmm, sorry, I was too quick: what is included is vscoq-language-server.

I am not sure I understand what coq-lsp is used for.

[MSoegtropIMC]

opam list --depends-on coq-lsp

is empyt.

The Coq platform board is still in bring up. The only package we agreed on to add is vscoq-language-server. For all other packages there will be an update in about 3 months.

For coq-lsp I would need to understand what it is good for. The discussions mentions it is used by VSCoq, but this doesn't seem to be accurate.

[ejgallego]

Hi @MSoegtropIMC ,

I'm sorry there was a confusion between coq-lsp and vscode-language-server , these are different projects (coq-lsp predates VsCoq 2) and they have a very different set of features.

In particular, coq-lsp is used by many teaching setups (for example in the analysis courses at TUE, using WaterProof), jsCoq, and almost all of serapi users that have migrated to several features. These days, machine learning researchers are a common target users of coq-lsp + the petanque interaction protocol.

One of the use cases for coq-lsp is indeed replacing SerAPI (which has mostly happened in upstream projects)

As you aware I do maintain several platform installers for these windows users, which allows them to run Coq and coq-lsp natively on Windows (and with real-time interruption etc....)

For coq-lsp I would need to understand what it is good for. The discussions mentions it is used by VSCoq, but this doesn't seem to be accurate.

Indeed this is not accurate, coq-lsp provides it's own VSCode extension.

opam list --depends-on coq-lsp

That's the case for serapi and vscoq-language-server, on the VSCode side there are a few extensions that do depend on coq-lsp tho, for example CoqPilot, VIXZ, Coq Categroy Theory Diagrams, etc...

The Coq platform board is still in bring up. The only package we agreed on to add is vscoq-language-server. For all other packages there will be an update in about 3 month

Do you mean coq-lsp was discussed for inclusion or not?

Maintaining the installers is a lot of work, I'm a bit at a loss as how to proceed as I've been trying to get coq-lsp in the platform for over 2 years without success. This seems like a long time to me for what amounts to a one-line patch. Do you have any suggestion on how we move forward here?

[MSoegtropIMC]

All package inclusion requests are being discussed - the issue is that we didn't agree on the height of the bar for inclusion as yet. The opinion of the board members on this varies vastly. The issue is that the effort to main Coq Platform raises at least linearly with the number of packages and also the download size rises. For download size we would be fairly unlimited if we could support dynamic package installs but the main issue here is the lack of system compatibility of .vo files. But quite a few individual packages lead to specific system issues which need to be handled. More packages - more issues. We reached the limit of what is feasible to maintain and the maintainers - Romain and me - are reluctant to increase the effort further.

To give you an example of the efforts: serapi produced much longer paths during build than any other package. I implemented several hacks to reduce the path length, e.g. to put the opam folder into the root of cygwin (/opam instead of /home//.opam) to save a few characters. But the paths length increased in each version - even though I told you that this is problematic - and in the end the only option was to implement arbitrary PATH length support - which is tricky because it is not common to do this and not well documented how to do it (one has to do two things, a system wide registry setting and changes in the manifest of all executables and DLLs). If you know how to do it, it is trivial. This reminds me of a story of Richard Feynman where he watched two mathematicians discussing a proof for many hours and in the end one exclaimed "oh yes, now I see it - it's trivial - it's trivial". So Feynman concluded that for mathematicians "trivial" is a synonym for "provable". Many system issues are trivial in a similar sense.

Other individual packages have other package specific issues - finding DLLs, stack size, you name it.

[ejgallego]

Dear @MSoegtropIMC , thanks for your answer; I'm sorry but I am not sure I understand the status of this issue yet.

All package inclusion requests are being discussed

What is the status of the board discussion regarding this issue? In particular:

• has coq-lsp inclusion discussed?
• If so, what was the timeline?

To give you an example of the efforts: serapi produced much longer paths during build than any other package.

This is indeed unfortunate, but note that this issue is a general issue for any OCaml package that uses Dune on windows, see for example recent updates to Dune to shorten paths (which I think you are aware)

We reached the limit of what is feasible to maintain and the maintainers - Romain and me - are reluctant to increase the effort further.

What does this mean for coq-lsp?

[MSoegtropIMC]

see for example recent updates to Dune to shorten paths (which I think you are aware)

not really - as I said the issue is solved by allowing arbitrary path lengths on Windows and on other platforms it never was a problem anyway. The changes in dune came to late for Coq Platform.

What does this mean for coq-lsp?

I honestly can't say right now. As I said my plan is to do an update in 3 months. If coq-lsp is used in lectures, chances are good that it will be included. A few references to courses would help, including approximate student count.