Integrate with coq-lsp?

[whonore]

Might be interesting to use https://github.com/ejgallego/coq-serapi instead of talking to coqtop directly.

[tomtomjhj]

See also: https://github.com/ejgallego/pycoq

[Alizter]

We now have https://github.com/ejgallego/coq-lsp which is designed for UI interaction. If you are interested ping Emilio @ejgallego he can explain further. (You can think of coq-lsp as a successor to serapi).

[whonore]

Thanks, I’ll take a look. From a quick skim of the features and FAQ, it’s not clear to me how easy it would be to swap out the XML protocol for coq-lsp without also redoing a lot of the Vim-side interface. For example, the continuous incremental checking seems great, but fundamentally a pretty different user experience from the current sentence-at-a-time approach. I wonder if it would make more sense to write something from scratch or to build on an existing Vim LSP plugin.

I’d be curious to hear more about how the jsCoq port went and how widespread the changes were.

[tomtomjhj]

I wonder if it would make more sense to write something from scratch or to build on an existing Vim LSP plugin.

For neovim, lean.nvim would be a good starting point. It uses neovim's built-in LSP client to communicate with Lean language server.

[ejgallego]

@whonore , thanks for the comments, I am not familiar with Coqtail's current internals, so I can't tell how much would the switch to lsp go. A few notes:

• coq-lsp is basically standard LSP + a goal info query
• the port of jsCoq to LSP went very well, we solved quite a few of issues we had, and removed a large amount of code; but of course, we did design coq-lsp with jsCoq in mind. So now jsCoq has moved from a complex protocol to basically a very clean model where it relays document changes to the LSP server, listens for diagnotics, and sends goals requests. It is really simple now, and for some documents like Software Foundations work much better.
• in general most people find great to be liberated from the prev/next command burden
• the step-by-step model can be emulated using Pull Diagnostics with a range, so you ask the coq-lsp to check only a particular range

Regarding SerAPI, it is to all effects deprecated, as in general coq-lsp provides a superset of the functionality with a better interface.

[whonore]

Thanks for the info. I'll need to look further into the details, but it seems like it would require some pretty significant changes to Coqtail, although mostly welcome simplifications. Basically, I think most of the backend dealing with XML, sentence parsing, tracking state IDs, etc. would be thrown out and replaced with LSP client code. A lot of the frontend (syntax highlighting, mappings for commands, goal/info panel display) could probably be kept.

In addition to looking at lean.nvim, it would be worth considering leveraging something like coc.nvim or ALE for the LSP part.

[ejgallego]

Indeed, the way we have implemented LSP means that all code dealing with the XML protocol goes away in favor of simple loop where the editors update the server, and query in a position-based setup.

But as you note this is an often welcome simplification, and provides some nice features due to coq-lsp supporting incremental-aware error recovery, so for example you can edit inside proofs without any special client code.

It also makes supporting things like Coq Markdown files (.mv) very easy for clients.

If there is something in coq-lsp we could do to make Coqtail's work easier I'd be very happy to hear.

[tomtomjhj]

In case anyone wants to quickly try coq-lsp in neovim, here's a very simple client implementation based on neovim's built-in lsp client. https://github.com/tomtomjhj/coq-lsp.nvim

[whonore]

I created an extremely preliminary, very experimental coq-lsp branch that uses vim-lsp for the LSP backend. It was relatively easy to get running and is fairly similar to @tomtomjhj's NeoVim version, but in vimscript instead of lua. I was able to reuse a lot of the existing logic for handling the goal panel and highlighting. I'd imagine it wouldn't be too difficult to set things up such that Coqtail supports a configurable LSP backend (vim-lsp, ALE, coc-nvim, nvim native, vim native, etc) by providing some interface that they can all implement (e.g., handling the proof/goals command and $/coq/fileProgress notification) and then using a common frontend to display goals, highlighting, etc.

[ejgallego]

That's amazing @whonore !

A point of interest for clients is how to communicate to coq-lsp that they would like the file not to be checked in full.

The solution that LSP 3.18 may provide and would work for Coq is Pull Diagnostics + a range parameter + a partialResult token, but there are other alternatives of course using non-standard calls.

The above is not yet implemented in coq-lsp (tho a prototype exists) as VS Code doesn't set the partialResult token in Pull Diagnostics mode.

An alternative to this is to allow coq-lsp to be set in "fully lazy mode", so only when a proof/goals request is done, we check up to that point; but that has bad latency properties.

We could also support a $/coq/inView notification, that would be emitted just after didChange, and would tell Coq "check this range".