Integration with native Coq LSP
Closed this issue · 20 comments
Dear @siegebell ,
we are getting ready for the release of native Coq LSP server, and we wondering what your plans would be wrt to this plugin.
Our LSP server strictly adheres to the protocol, so the model of interaction is a bit different.
What are you thoughts wrt vscoq? Do you think the plugin should be branch to work against the new server?
Great to hear about the LSP support! I've really enjoyed using Lean with VS Code, and having a similar experience with Coq would be excellent!
Perhaps it might be a good idea to start work on a new extension? Sadly this project seems to be abandoned, and having used it before, I found it had a bunch of usability issues, like opening up a broken proof pane to the side whenever I opened a file…
Thanks for the feedback @brendanzab , indeed I am optimistic in that this will be a welcome addition to the world of Coq UIs! :)
Perhaps it might be a good idea to start work on a new extension? Sadly this project seems to be abandoned, and having used it before, I found it had a bunch of usability issues, like opening up a broken proof pane to the side whenever I opened a file…
Indeed we may want to start a new extension at some point, so far we are testing with a mini-extension derived from this one, and IMO the new extension should be a fork [lots of useful stuff].
A big problem that vscoq had was that they had to implement their own server on top of the Coq's XML protocol, and this is very hard to do without bugs [for boring technical reasons], so quite a few bugs here were really the fault of Coq itself.
Anyways I hope we have a first public alpha really soon so we can start working on the real things, the main blocker is that quite a few Coq changes have to be incorporated upstream and that process is quite slooooow... :)
Oh cool! Great to hear about the progress.
If we can get Coq working nicely with a package manager like https://esy.sh/, (the author says that it might be possible), then Coq will be well on the road to providing a lovely, up-to-date tooling experience. I'm excited!
If we can get Coq working nicely with a package manager like https://esy.sh/, (the author says that it might be possible), then Coq will be well on the road to providing a lovely, up-to-date tooling experience. I'm excited!
What's the problem with esy? I am not familiar with it (yet), but most things should work I think, would you mind opening a tracker issue on the Coq repos to see what can we do on our part?
Yeah, I've not actually given it a good go yet, so I can pass on any issues to the issue tracker. Perhaps it's more an issue of providing some docs (even potentially on the esy.sh site). One of the things that has caused me to bounce off Coq in the past has been poor support for editors like VS Code, and struggling with _CoqProject, Opam and/or vendoring using git submodules.
Indeed @brendanzab we are very well aware of similar complains by other users, please don't hesitate to open an issue in the Coq bug tracker each time you find a less-than-optimal experience.
Unfortunately manpower is very limited [and Coq's slow dev model makes it hard to make progress] but we are getting to a point where things start to look a bit better in terms of tooling.
Thanks for your hard work! It's super important! 👏
I guess the interesting thing with package management is how it integrates with the editor support. Like with Rust I expect if I change the package file it will trigger the RLS to pick up on those changes seamlessly. I'm unsure whether there is support for Esy to provide that to a Coq extension though 🤔.
That's a very important point, it is still not very clear how we are going to do that, my plan was indeed to have the LSP server call dune so it can learn about what needs to be done project-wise. This will require a new call in Dune, similar to .merlin file generation [but file-less]
I'd have loved to reuse the merlin format but for some other reasons that was not a good choice. So indeed maybe Coq can piggyback on the "merlin 2.0" file format whatever such format is.
Yeah. I'm guessing it would make sense to try to figure out how to work with the existing _CoqProject format, but also provide a better solution in the future. I tried searching for info about this on the Esy issue tracker, but only found esy/esy#850 and esy/esy#853 - the latter shows something like:
"devDependencies": {
"@opam/merlin-lsp": "*"
}Which suggests the LSP might be driven from Esy, but that might be an idea for a future solution rather than a current one...
I'm much afraid that it will be hard to provide good workspace support for projects using _CoqProject as the format just lacks the needed information on lib dependencies. People will have to migrate to dune for that to work better.
Ah, that makes a lot of sense. Sounds better to rip off that band-aid then! Yeah, I can see how _CoqProject could be super annoying to work with.
Hi (esy developer here),
Firstly, I'm super excited about Coq LSP (thanks @ejgallego) - hope it will help make vim + Coq experience much better!
By the way what LSP lib do you use for Coq LSP? I'm working on LSP frontend for merlin and we have own implementation there. Would be nice to have a good OCaml lib for LSP generally usable though.
esy + Coq LSP
I'm beginner with Coq (going through SF slowly) and I'm using esy to install coq package from opam. Then I just do esy vim and vim sees coqtop (this is what's used by vim plugin right now) in $PATH.
So I suspect that if Coq LSP will be available as some command (coq-lsp for example) then it will be working with esy the same way.
Apart from putting needed things on $PATH (and handling other environment variables) esy doesn't do any special regarding LSP (or other tools for that matter). Though we have plans for LSP specific features esy in the future.
LSP + dune
That's a very important point, it is still not very clear how we are going to
do that, my plan was indeed to have the LSP server call dune so it can learn
about what needs to be done project-wise. This will require a new call in
Dune, similar to .merlin file generation [but file-less]
I was about to suggest to dune to drive LSP servers from dune via dune lsp command instead of generating .merlin (or any other files) in source trees (polluting source trees with artifacts doesn't work well with esy model though we have workarounds now).
Another advantage that you configure needed LSP in dune once (merlin LSP for *.ml and Coq LSP for *.v) and then have dune lsp route requests for different server it has spawned.
Also dune lsp might provide some assistance for editing dune/dune-project files.
So the gist of the mechanism is:
- User executes
dune lsp dune lspstartsocamlmerlin-lspor Coq LSP on demand (when user starts editing either OCaml or Coq source files).dune lsproutes requests to eitherocamlmerlin-lspor Coq LSP depending on URI file type.
Sorry to hijack the discussion!
Hi @andreypopp !
By the way what LSP lib do you use for Coq LSP? I'm working on LSP frontend for merlin and we have own implementation there. Would be nice to have a good OCaml lib for LSP generally usable though.
Indeed I just saw that yesterday! We use some very basic JSON handling as done here https://github.com/Deducteam/lambdapi/tree/master/lp-lsp , indeed it would be nice to share code, but we were worried by other design considerations.
I was about to suggest to dune to drive LSP servers from dune via
dune lspcommand instead of generating.merlin(or any other files) in source trees (polluting source trees with artifacts doesn't work well with esy model though we have workarounds now).
That's a very interesting idea! Thanks for the comments! I need to think a bit more about it, in my current mental model the lsp server is started by the editor so indeed dune would be an slave of it.
Though we have plans for LSP specific features esy in the future.
Any pointer to an issue roadmap?
I need to think a bit more about it, in my current mental model the lsp server is started by the editor so indeed dune would be an slave of it.
This still holds - the editor will start dune lsp in that case (which will route requests to either merlin lsp or coq lsp).
Though we have plans for LSP specific features esy in the future.
Any pointer to an issue roadmap?
Not yet, I'll put something together soon.
Excited to have you over here @andreypopp - I was tossing up whether to @ you - didn't want to be spammy or anything!
I would be very interested to have specific documentation for using Coq with esy. @brendanzab or @andreypopp or someone else: if you have time for this, it would be very nice to start writing a documentation page on the Coq wiki: https://github.com/coq/coq/wiki.
In particular, I'm interested to see if using esy would be making the life of non-tech users easier (I'm actually not fully sure about this given that installing esy requires to first install npm, but overall the workflow seems more straightforward than with opam).
I'm actually not fully sure about this given that installing esy requires to first install npm
Yeah, it'd be interesting if esy could eventually be installed using system package managers or installers, but I understand if it's hard to keep up with maintaining those in the early days of development. Thankfully(?) most newcomers to development have npm installed these days, so maybe that might make things a little easier. At any rate, I think this might be a more specific question for the esy issue tracker itself, for example: esy/esy#765
People here will be happy to know coq-community forked this plugin! #170
Indeed, we can close this issue.