Coq LSP

coq-lsp is a Language Server and Visual Studio Code extension for the Coq Proof Assistant. Experimental support for Vim and Neovim is also available in their own projects.

Key features of coq-lsp are continuous and incremental document checking, advanced error recovery, markdown support, positional goals and information panel, performance data, and more.

coq-lsp aims to provide a seamless, modern interactive theorem proving experience, as well as to serve as a maintainable platform for research and UI integration with other projects.

coq-lsp is built on top of Flèche, a new document checking engine for formal documents, designed from our experience in previous, projects. Flèche is specifically optimized for interactive use, SerAPI-like tooling integration, and web native usage, providing quite a few extra features from vanilla Coq.

coq-lsp supports 🐧 Linux, 🍎 macOS, 🪟 Windows , and ☕ JavaScript (Node/Browser)

🎁 Features
🛠️ Installation
🗣️ Discussion Channel
☎ Weekly Calls
❓FAQ
⁉️ Troubleshooting and Known Problems
- 📂 Working With Multiple Files
📔 Planned Features
📕 Protocol Documentation
🤸 Contributing
🥷 Team
- 🕰️ Past Contributors
©️ Licensing Information
👏 Acknowledgments

🎁 Features

⏩ Incremental Compilation and Continuous Document Checking

Edit your file, and coq-lsp will try to re-check only what is necessary, continuously. No more dreaded Ctrl-C Ctrl-N! Rechecking tries to be smart, and will ignore whitespace changes.

In a future release, coq-lsp will save its document cache to disk, so you can restart your proof session where you left it at the last time.

Incremental support is undergoing refinement, if coq-lsp rechecks when it should not, please file a bug!

🧠 Smart, Cache-Aware Error Recovery

coq-lsp won't stop checking on errors, but supports (and encourages) working with proof documents that are only partially working. Moreover, error recovery integrates with the incremental cache, and will recognize proof structure.

You can edit without fear inside a Proof. ... Qed., the rest of the document won't be rechecked, unless the proof is completed.

Moreover, if a lemma is not completed, coq-lsp will admit it automatically. No more Admitted / Qed churn!

Furthermore, you can leave bullets and focused goals unfinished, and coq-lsp will automatically admit them for you.

🥅 Whole-Document Goal Display

coq-lsp will follow the cursor movement and show underlying goals and messages; this is configurable in case you'd like to trigger goal display more conservatively.

The panel will also include goals that you have given up or shelved. This panel will also show the current info about open bullets and their goals.

🗒️ Markdown Support

Open a markdown file with a .mv extension, coq-lsp will check the code parts that are enclosed into coq language blocks! coq-lsp places human-friendly documents at the core of its design ideas.

👥 Document Outline

coq-lsp supports document outline and code folding, allowing you to jump directly to definitions in the document. Many of the Coq vernacular commands like Definition, Theorem, Lemma, etc. will be recognized as document symbols which you can navigate to or see the outline of.

🐝 Document Hover

Hovering over a Coq identifier will show its type.

📁 Multiple Workspaces

coq-lsp supports projects with multiple _CoqProject files, use the "Add folder to Workspace" feature of Visual Studio code or the LSP Workspace Folders extension to use this in your project.

💾 `.vo` file saving

coq-lsp can save a .vo file of the current document as soon as it the checking has been completed, using the command Coq LSP: Save file to .vo.

You can configure coq-lsp in settings to do this every time you save your .vo file, but this can be costly so we ship it disabled by default.

⏱️ Detailed Timing and Memory Statistics

Hover over any Coq sentence, coq-lsp will display detailed memory and timing statistics.

🔧 Client-Side Configuration Options

coq-lsp is configurable, and tries to adapt to your own workflow. What to do when a proof doesn't check, admit or ignore? You decide!

See the coq-lsp extension configuration in VSCode for options available.

♻️ Reusability, Standards, Modularity

The incremental document checking library of coq-lsp has been designed to be reusable by other projects written in OCaml and with needs for document validation UI, as well as by other Coq projects such as jsCoq.

Moreover, we are strongly based on standards, aiming for the least possible extensions.

🌐 Web Native!

coq-lsp has been designed from the ground up to fully run inside your web browser seamlessly; our sister project, jsCoq has been already been experimentally ported to coq-lsp, and future releases will use it by default.

coq-lsp provides an exciting new array of opportunities for jsCoq, lifting some limitations we inherited from Coq's lack of web native support.

🔎 A Platform for Research!

A key coq-lsp goal is to serve as central platform for researchers in Human-Computer-Interaction, Machine Learning, and Software Engineering willing to interact with Coq.

Towards this goal, coq-lsp extends and is in the process of replacing Coq SerAPI, which has been used by many to that purpose.

If you are a SerAPI user, please see our preliminary migrating from SerAPI document.

🛠️ Installation

In order to use coq-lsp you'll need to install both coq-lsp and a suitable client. We recommend the Visual Studio Code Extension.

🏘️ Supported Coq Versions

coq-lsp supports Coq 8.16, Coq 8.17, and Coq's master branch.

We recommended a minimum of Coq 8.17, due to better test coverage for that version. We also recommend users to install the custom Coq trees for 8.16 and 8.17 as detailed in Working With Multiple Files

Support for older Coq versions is possible; it is possible to make coq-lsp work with Coq back to Coq 8.10/8.9. If you are interested in making that happen don't hesitate to get in touch with us.

🏓 Server

opam:
```
opam install coq-lsp
```

Nix:

In nixpkgs: #213397
In your flake:

inputs.coq-lsp = { type = "git"; url = "https://github.com/ejgallego/coq-lsp.git"; submodules = true; };
...
coq-lsp.packages.${system}.default

Windows: To install coq-lsp on windows, we recommend you use a cygwin build, such as the one described here, tho any OCaml env where Coq can be built should work.
- build coq-lsp from source (branch v8.16, which will become 0.1.7)
- Set the path to coq-lsp.exe binary in VS Code settings
- Set the --ocamlpath=c:\$path_to_opam\lib argument in VS Code settings if you get a findlib error. The Coq Platform ships with an un-configured binary. Note, the path should be unquoted
- If the binary doesn't work, try to run it from the file explorer; if you get a .dll error you'll need to copy that dll (often libgmp-10.dll) to the C:\Windows folder for coq-lsp to work.
Coq Platform (coming soon)
- See the bug tracking coq-lsp inclusion
Do it yourself!

🫐 Visual Studio Code

Official Marketplace: https://marketplace.visualstudio.com/items?itemName=ejgallego.coq-lsp
Open VSX: https://open-vsx.org/extension/ejgallego/coq-lsp
Nix:

inputs.coq-lsp = { type = "git"; url = "https://github.com/ejgallego/coq-lsp.git"; submodules = true; };
...
programs.vscode = {
  enable = true;
  extensions = with pkgs.vscode-extensions; [
    ...
    inputs.coq-lsp.packages.${pkgs.system}.vscode-extension
    ...
  ];
};

✅ Vim

Experimental CoqTail support by Wolf Honore: whonore/Coqtail#323

See it in action https://asciinema.org/a/mvzqHOHfmWB2rvwEIKFjuaRIu

🩱 Neovim

Experimental client by Jaehwang Jung: https://github.com/tomtomjhj/coq-lsp.nvim

🗣️ Discussion Channel

coq-lsp discussion channel it at Coq's Zulip, don't hesitate to stop by; both users and developers are welcome.

☎ Weekly Calls

We hold (almost) weekly video conference calls, see the Call Schedule Page for more information. Everyone is most welcome!

❓FAQ

See our list of frequently-asked questions.

⁉️ Troubleshooting and Known Problems

Some problems can be resolved by restarting coq-lsp, in Visual Studio Code, Ctrl+Shift+P will give you access to the coq-lsp.restart command. You can also start / stop the server from the status bar.
In VSCode, the "Output" window will have a "Coq LSP Server Events" channel which should contain some important information; the content of this channel is controlled by the Coq LSP > Trace: Server option.
If you install coq-lsp simultaneously with VSCoq, VSCode gets confused and neither of them may work. coq-lsp will warn about that. If you know how to improve this, don't hesitate to get in touch with us.

📂 Working With Multiple Files

coq-lsp can't work with more than one file at the same time, due to problems with parsing state management upstream. This was fixed in Coq master branch (to become Coq 8.18).

As this is very inconvenient, we do provide a fixed Coq branch that you can install using opam pin:

For Coq 8.17:

opam pin add coq-core https://github.com/ejgallego/coq.git#v8.17+lsp

For Coq 8.16:

opam pin add coq https://github.com/ejgallego/coq.git#v8.16+lsp

📔 Planned Features

See planned features and contribution ideas for a list of things we'd like to happen.

📕 Protocol Documentation

coq-lsp mostly implements the LSP Standard, plus some extensions specific to Coq.

Check the coq-lsp protocol documentation for more details.

🤸 Contributing

Contributions are very welcome! Feel free to chat with the dev team in Zulip for any question, or just go ahead and hack.

We have a contributing guide, which includes a description of the organization of the codebase, developer workflow, and more.

Here is a list of project ideas that could be of help in case you are looking for contribution ideas, tho we are convinced that the best ideas will arise from using coq-lsp in your own Coq projects.

🥷 Team

Ali Caglayan (co-coordinator)
Emilio J. Gallego Arias (Inria Paris, co-coordinator)
Shachar Itzhaky (Technion)
Ramkumar Ramachandra (Inria Paris)

🕰️ Past Contributors

Vincent Laporte (Inria)

The license for this project is LGPL 2.1 (or GPL 3+ as stated in the LGPL 2.1).

This server forked from our previous LSP implementation for the Lambdapi proof assistant, written by Emilio J. Gallego Arias, Frédéric Blanqui, Rodolphe Lepigre, and others; the initial port to Coq was done by Emilio J. Gallego Arias and Vicent Laporte.
Syntax files in editor/code are partially derived from VSCoq by Christian J. Bell, distributed under the terms of the MIT license (see ./editor/code/License-vscoq.text).

👏 Acknowledgments

Work on this server has been made possible thanks to many discussions, inspirations, and sharing of ideas from colleagues. In particular, we'd like to thank Rudi Grinberg, Andrey Mokhov, Clément Pit-Claudel, and Makarius Wenzel for their help and advice.

As noted above, the original implementation was based on the Lambdapi LSP server, thanks to all the collaborators in that project!

Name		Name	Last commit message	Last commit date
Latest commit History 823 Commits
.github		.github
.vscode		.vscode
controller		controller
coq		coq
editor/code		editor/code
etc		etc
examples		examples
fleche		fleche
lang		lang
lsp		lsp
test		test
vendor		vendor
.envrc		.envrc
.gitignore		.gitignore
.gitmodules		.gitmodules
.ocamlformat		.ocamlformat
.prettierignore		.prettierignore
CHANGES.md		CHANGES.md
CODE_OF_CONDUCT.md		CODE_OF_CONDUCT.md
CONTRIBUTING.md		CONTRIBUTING.md
LICENSE		LICENSE
Makefile		Makefile
README.md		README.md
coq-lsp.opam		coq-lsp.opam
default.nix		default.nix
dune		dune
dune-project		dune-project
flake.lock		flake.lock
flake.nix		flake.nix
shell.nix		shell.nix

License

TDiazT/coq-lsp

Folders and files

Latest commit

History

Repository files navigation