Language Server Protocol

[ejgallego]

We should support LSP to some degree.

https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md

[ejgallego]

An OCaml implementation of LSP data structures is here: https://github.com/facebook/hhvm/blob/master/hphp/hack/src/utils/lsp.ml

Would we get then a TODO list, it should be easy to support this in a basic sense. Some more advances capabilites of the LSP are quite hard to do due to Coq internals.

[ejgallego]

This is well on the road and working now; it wouldn't be unreasonable to expect SerAPI to build on the LSP kernel for 0.7.0

[carlpaten]

I'd like to help with this issue, do you know of some relatively self-contained work that needs to get done to support LSP?

[ejgallego]

@LilRed as I mentioned in the other issue, there is an in-progress branch. If you can I can give you access, but we'd still like to rewrite the whole server implementation before releasing to better account for the nuances of inter-process communication.

[carlpaten]

@ejgallego any chance I can get access to the in-progress branch?

[ejgallego]

@LilRed I could give you access to the tree however that wouldn't help a lot; the main issue here and where work is concentrated now is in the base Coq API for incremental document checking.

Until that is ready, proper LSP is too hard to implement reliably IMO. So first we are working on icheck, then coq-lsp will be built on top of that [and serapi too].

I hope a first "alpha" version of icheck is ready soon, so indeed at that point we could try to make the lsp code work; what are your goals? I'd be great indeed to setup the minimal amount of code so collaboration is possible.

As for now, the Coq branch of the LSP server is basically this code but adapted to Coq without significant changes.

[carlpaten]

what are your goals?

Broadly, to invest in something Coq-related for ~150 hours with between February and April. Also, I'd like to do my part towards moving on from CoqIDE to something more flexible and modern. Not that CoqIDE is particularly bad, in fact it's surprisingly good, but it's not easily extensible and I haven't figured out how to "look under the hood" and work around its warts.

the main issue here and where work is concentrated now is in the base Coq API for incremental document checking

Can you point me to that work? Or is it not publicly accessible?

Best

[ejgallego]

Hi @LilRed , indeed I think your timeframe should work pretty well.

Can you point me to that work? Or is it not publicly accessible?

Sure, I will give you some pointers in the next weeks; the reason the current prototype is not publicily accessible is that it is still not usable and I feel it would make many people lose a lot of time.

Indeed, the current prototype needs a full rewrite once we improve the Coq API itself, but that should happen pretty soon as we have made quite a bit of progress on the Coq side; the Coq PR allowing for the icheck / LSP prototype to function should land in master soon.

[carlpaten]

the Coq PR allowing for the icheck / LSP prototype to function should land in master soon.

What PR would that be? :)