Language Server Protocol proposal

[artagnon]

The Language Server Protocol is a widely-used communication protocol, with first-class support in VSCode, and decent support in Vim and Emacs. Very many servers and client implementations exist today, for a wide variety of languages. However, a cursory look at the document is enough to know that the protocol has not standarized any functionalities that are relevant to interactive proof assistants, and in particular, Coq. However, it is easy to deviate from the standard described in the document, and implement custom extensions. The particular ease-of-implementation of a server and client makes LSP a particularly attractive choice.

Today, we have VSCoq communicating via an XML-protocol, and the server implementation is in coqidetop. However, VSCoq suffers from the problem of being difficult to understand and maintain, let alone extend, due to its sheer size. Besides, the XML protocol is poorly documented, and CoqIDE is the first-class consumer. While it is possible to enhance the XML protocol to support some additional functionality, to expose more of the information available in Vernac.State.t, and enhance the overall experience of writing Coq, adding complexity to an already complex VSCoq would probably be unwise.

It would indeed be most pleasant if we manage to manage to augment LSP to support interactive proof assistants in an agnostic way. It would benefit all proof assistants across the board, and eliminate the burden of having to develop and maintain a separate IDE. It would reduce the burden on Proof General too, as they can use the Emacs LSP extension and get most of the low-level functionality for free. Indeed, it would reduce the burden on us too, if we consider phasing out CoqIDE and moving to this proposed setup, in the long term. While I've opened microsoft/language-server-protocol#1414, much of its success depends on presenting a working implementation.

On the subject of this particular patch, I'm proposing to create a ide/lsp, where we can carry out these experiments. I'm feeling mildly optimistic about its success. Of course, there's always the risk that it won't gain traction, in which case, tant pis. The effort brings a lot of potential benefits for everyone, and it's not too hard.

I'm stuck at the moment with a compiler error in lsptop.ml which I haven't been to resolve. I don't know if streams are a good solution, and I'm not an OCaml expert to convert from byte streams written into some buffer into a string stream. Otherwise, the rest of the code should be pretty straightforward.

[ejgallego]

@artagnon we already have at least two fucntioning lsp servers for Coq, and they are way more advanced than this. I'd suggest coordination with us over Zulip, I can give you access to my own private repos and I'd love to discuss more.

I tell you something, this is not trivial at all to get right.

Moreover, there is no need to have this server, in such experimental state, in the codebase, it can live perfectly as a separate project for the moment.

[artagnon]

Some things to address:

1. Can you share the draft of the custom LSP extensions that you've implemented?
2. I need access to Vernac, Vernacexpr, Vernacprop, and Vernacstate. Out of curiosity, considering these things, wouldn't it be easier to develop in-tree?
3. idetop.ml already does the work of collecting subgoals and processing goals. Much of the extra work has gone into the XML parser, which wouldn't be necessary if we were to use Yojson in LSP.
4. lsptop has to be significantly simpler than idetop, right? Of course, this is assuming feature-parity with idetop, not the extra bells and whistles provided by LSP.
5. Personally, I prefer public in-tree development to private out-of-tree development, for precisely this reason: a new contributor cannot be expected to be aware of private development.
6. If the LSP servers you have work, why not move them in-tree, to give them visibility and attract contributors?

I have no particular stake in this: it was 1.5 days of work, and I put it up because I needed help at this point.

[ejgallego]

@artagnon see my message on zulip

1. I don't share it because it is not ready for users, so I don't want people to use it and lose their time. But I'm happy to share with you.
2. No, it is easier to develop out of tree
3. first thing you need for lsp is incremental document processing, that's out of reach for idetop, and many other things, I'll be happy to explain in person or in a video chat
4. coq-lsp is a full reimplementation of the docuemnt manager, and while the code is easier to read, it is incomparable as they follow very different designs
5. in-tree development means your commits are blocked, vs the freedom we have in outer projects such as jscoq or serapi; moreover, it is more modular, and flexible wrt development workflows
6. designing a proper document manager for Coq is a very hard topic, so cannot be done so easily as just putting some code out, it requires actually even new research in a few areas. But actually we are indeed planning to do a UI meeting soon precisely to coordinate this

[artagnon]

Okay, I'm dropping this in favor of @ejgallego's coq-lsp, which I will see in person next week.