search

coq / platform

Multi platform setup for Coq, Coq libraries and tools
Creative Commons Zero v1.0 Universal
189 stars 50 forks source link

Add coq-lsp to Coq Platform #319

Open ejgallego opened 1 year ago

ejgallego commented 1 year ago

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:

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

Other relevant issues / PRs:

ejgallego commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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