Coq developers have been recently pushing an LSP compatible interface (https://github.com/coq/coq/projects/30).
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.