Comments (10)
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.
from coqtail.
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
from coqtail.
See also: https://github.com/ejgallego/pycoq
from coqtail.
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).
from coqtail.
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.
from coqtail.
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.
from coqtail.
@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.
from coqtail.
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.
from coqtail.
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.
from coqtail.
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".
from coqtail.
Related Issues (20)
- Anonymous implicit generalization is not recognized HOT 3
- Register command is not recognized
- Requires Python 3.6 error in Neovim HOT 2
- Comments with leading * cannot be joined using J HOT 1
- Formatting comments (e.g. using gqq) does not work correctly HOT 1
- coqtail hangs on first command with `-noinit`
- Plugin does not load; WSL2 Ubuntu HOT 2
- Set Firstorder Solver idtac. HOT 1
- Feature Request: option to omit proofs when scripting (auto-admit) HOT 1
- Breaking with after/syntax directory HOT 5
- [Syntax] Is there a lack of support for math symbol shortcuts? HOT 2
- Detach panels from neovim instance HOT 3
- Unexpected error when debugging Unicoq HOT 2
- Coqtail doesn't recognize the option `-arg "-w all"`
- Coqtail does not officially support your version of Coq (8.19.0) HOT 7
- Feature: better support for dune HOT 4
- :Coq Set Printing Width not persistent HOT 1
- Comments inside of strings are not highlighted correctly
- Error on some large operations HOT 4
- Wrong syntax highlight for `Structure` HOT 2
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from coqtail.