From what I understood, it seems that it greatly helped rebooting the VScoq plugin to VS code.
A few heavy users of Coq told me recently that they migrated from using emacs+PG to VS code + VS coq because the user experience is better in some aspects, in particular more reactive.
As a PG user, I must admit that I have been sometimes frustrated by the lack of responsiveness of the interface. At the same time, I really appreciate my current editing setup and Iām unwilling to change my editor.
There is an lsp-mode for emacs, so we may be able to take advantage of these developments.
Which lead to my questions:
Did anyone try to use coq + lsp in emacs ? Is there a project out there to use this ?
Could this provide an alternative to PG (or be used in PG directly) ?
How much work is there to make the coq + lsp + emacs interface reasonable ? And where should we target our efforts ?
I personally donāt have any experience with lsp and only little experience with emacs-mode development, so I hope knowledgeable developers on both side can enlighten me on the difficulties and struggles awaiting to transform this thought into a reality.
Hi
I donāt think there is real difficulty, except that coq changed its communication protocol about each year since several years (xml first protocol, xml second protocol, serapi, lsp, ), and the pg team donāt have time to follow these changes. I am still not convinced that LSP is the good protocol here, since it needs some extension to deal with a proof assistant.
On one hand it is clear that the current communication between coq and proofgeneral is outdated and should be replaced by some modern (asynchronous, state machine) stuff, but on the other hand proofgeneral is widely used and we need it to work 365 days a year on all coq versions 5 years back from present.
So for now and until I am wrong (which I would be very happy to be) I am afraid proofgeneral will remain based on an outdated (but rather stable) protocol.
An async branch of PG has been under development for quite some timeā¦ does anyone know what the latest status is of that? Is it anywhere close to being merged into master?
There seems to be a lot of confusion about LSP in the Coq community.
LSP is a standardized interface between an editor and a language server, which supports queries about the code. These queries include things like code completion, documentation lookup, types for expressions - think things the compiler knows about your code.
The core functionality of Proof General is to run coqtop and interactively send imperative commands to it, of the form āprocess this codeā and ārewind to this stateā. What makes this challenging is that processing isnāt instantaneous, so Proof General has to manage concurrency between the editor, commands being sent to Coq, and giving feedback from Coq (eg, when something finishes running). It also has the complicated job of displaying and maintaining a refreshed proof state to show the user, which requires additional UI. None of this is part of an ordinary language and hence it isnāt part of the standard editor support for LSP - this is what a Proof General replacement would have to re-implement.
What could potentially be implemented is an LSP-based server-side interface for these proof state commands, but this would just add to the many server protocols Coq has and wouldnāt be significantly better than SerAPI, for example. Again, the difficulty is in the editor-side features, not the server side.
What could also be useful is to implement the other LSP queries to get a standardized implementation of things like code completion. First, note that company-coq already does a good job of this. Second, normally one argument for using LSP is that itās much easier to add support for the language to other editors - this argument doesnāt really apply to Coq, because each new editor fundamentally requires an interactive proof mode to use for Coq at all, and code completion is a secondary concern.
I read through the LSP project and it seems my view of LSPās benefits are a bit too pessimistic, since empirically Coq will support LSP and they seem to be getting a benefit from it. Iām especially glad if this is useful for VS Code, since Iād love to see a real alternative to CoqIDE for students (whom we canāt tell to learn Emacs, but also have to apologize to for CoqIDEās quirks and bugs).
My understanding of PGās async branch is that development stopped when it was functional but not complete, and when I used it I immediately ran into show-stopping bugs (eg, I needed to restart Emacs within a few minutes).
Iām a fan of VSCoq, but IIUC it doesnāt use LSP; it uses the same protocol that CoqIDE uses as well, with the same speed benefits. The difference is that VSCoq runs in a richer editor. The async branch of PG also uses the same protocol (tho itās incomplete).
To complete and correct the answers that were given here:
Proof General was the first ever interface to efficiently write Coq proofs (before that, people just used coqtop + copy-paste in Emacs or another editor). Even CoqIDE was inspired by Proof General. It is no wonder that no editor protocol existed at that time and that Proof General had no choice but to parse coqtop output (which was intended for humans, not machines).
The XML protocol is already both old and stable (one could even say ālegacyā). It is used by the great majority of alternative user interfaces to Proof General. Furthermore, it is not going to be removed any time soon, so it is safe to use. However, it suffers from limitations which justify that the Coq development team would like to build a new editor protocol (which wonāt be an XML protocol, not because the limitations are connected to the XML format, but because XML is out of fashion).
The failure of the async branch of Proof General comes from software engineering and management issues rather than anything related to the XML protocol itself: the engineer that was working on it was on a fixed-term contract and left the branch in an unfinished state without any real knowledge transmission to the Proof General maintainers. Furthermore, the branch kills the Proof General support for other languages than Coq. There are also licensing issues. It is not likely that it will ever get merged back.
SerAPI was never an official protocol (as witnessed by the independent distribution). It was always clearly marked as experimental (but it has actually become more and more stable). SerAPI is going to strongly influence whatever the next editor protocol turns out to be.
There is no LSP support in Coq as of today. As was correctly stated above, VSCoq uses the XML protocol behind the scenes. Whenever a new editor protocol is made available, it will be migrated to it.
VSCode support was a priority given the popularity of this editor and the ease of access to newcomers (and the fact that CoqIDE suffers from limitations stemming from the Coq development team not being expert on editor development). VSCode was already supported in Isabelle and Lean for instance (and now also in PVS and Mizar).
LSP is targeted at more traditional languages, and support for doing proofs require extensions. These extensions can be minimal or very large depending on the strategy that is adopted. There could be an opportunity to design a standard extension that would be provided by most proof systems and would allow a single editor support package to understand them all. However, such an opportunity is unlikely to become concrete because basically every one has been doing their own thing on their side for now.
Communication between the Coq development team and editor support package maintainers has not always been very effective. As a tentative to improve communication, I created this chat room recently: https://gitter.im/coq/user-interfaces. It has successfully attracted many of the relevant people, but discussion has not started there yet. If there is sufficient motivation, we could also try to organize a special user interface / editor protocols session at an upcoming Coq Working Group or Coq Users and Developers Workshop, to at least try to gather a shared set of needs and establish priorities.