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.
Quick Install:
- 🐧 Linux / 🍎 macOs:
$ opam install coq-lsp && code --install-extension ejgallego.coq-lsp
- 🪟 Windows: Download the Coq Platform installer
Key features of coq-lsp
are: continuous and incremental
document checking, advanced error recovery, hybrid Coq/markdown document
support, multiple workspace support, positional goals and information panel,
performance data, extensible command-line compiler, plugin system, and more.
See the coq-lsp User Manual for more information.
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
- ⏩ Incremental Compilation and Continuous Document Checking
- 👁 On-demand, Follow The Viewport Document Checking
- 🧠 Smart, Cache-Aware Error Recovery
- 🥅 Whole-Document Goal Display
- 🗒️ Markdown Support
- 👥 Document Outline
- 🐝 Document Hover
- 📁 Multiple Workspaces
- 💾
.vo
file saving - ⏱️ Detailed Timing and Memory Statistics
- 🔧 Client-Side Configuration Options
- 🖵 Extensible, Machine-friendly Command Line Compiler
- ♻️ Reusability, Standards, Modularity
- 🌐 Web Native!
- 🔎 A Platform for Research!
- 🛠️ Installation
- ⇨
coq-lsp
users and extensions - 🗣️ Discussion Channel
- ☎ Weekly Calls
- ❓FAQ
⁉️ Troubleshooting and Known Problems- 📔 Planned Features
- 📕 Protocol Documentation
- 🤸 Contributing and Extending the System
- 🥷 Team
- ©️ Licensing Information
- 👏 Acknowledgments
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!
coq-lsp
does also support on-demand checking. Two modes are available: follow
the cursor, or follow the viewport; the modes can be toggled using the Language
Status Item in Code's bottom right corner:
coq-lsp
won't stop checking on errors, but supports (and encourages) working
with proof documents that are only partially working. Error recovery integrates
with the incremental cache, and does recognize proof structure.
You can edit without fear inside a Proof. ... Qed.
, the rest of the document
won't be rechecked; you can leave bullets and focused goals unfinished, and
coq-lsp
will automatically admit them for you.
If a lemma is not completed, coq-lsp
will admit it automatically. No more
Admitted
/ Qed
churn!
coq-lsp
will follow the cursor movement and show underlying goals and
messages; as well as information about what goals you have given up, shelves,
pending obligations, open bullets and their goals.
Goal display behavior is configurable in case you'd like to trigger goal display more conservatively.
Open a markdown file with a .mv
extension, or a TeX
file ending in .lv
or
.v.tex
, then 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.
Moreover, you can use the usual Visual Studio Code Markdown or LaTeX preview facilities to render your markdown documents nicely!
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.
Hovering over a Coq identifier will show its type.
Hover is also used to get debug information, which can be enabled in the preferences panel.
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.
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.
Hover over any Coq sentence, coq-lsp
will display detailed memory and timing
statistics.
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.
coq-lsp
includes the fcc
"Flèche Coq Compiler" which allows the access to
almost all the features of Flèche / coq-lsp
without the need to spawn a
fully-fledged LSP client.
fcc
has been designed to be machine-friendly and extensible, so you can easily
add your pre/post processing passes, for example to analyze or serialize parts
of Coq files.
Thanks to Flèche, we provide some APIs on top of it that allow advanced use cases with Coq. In particular, we provide direct, low-overhead access to Coq's proof engine using petanque.
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.
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 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.
In order to use coq-lsp
you'll need to install both
coq-lsp
and a suitable LSP client that understands coq-lsp
extensions. The
recommended client is the Visual Studio Code Extension, but we aim to fully
support other clients officially and will do so once their authors consider them
ready.
coq-lsp
supports Coq 8.20, Coq 8.19, Coq 8.18, Coq 8.17, and Coq's master
branch. Code for each Coq version can be found in the corresponding branch.
We recommended using Coq 8.19 or master
version. For other Coq versions, we
recommend users to install the custom Coq tree as detailed in Coq Upstream
Bugs.
Note that this section covers user installs, if you would like to contribute to
coq-lsp
and build a development version, please check our contributing
guide
-
opam (OSX/Linux):
opam install coq-lsp
-
Nix:
- In nixpkgs: coqPackages.coq-lsp
- The
coq-lsp
server is automatically put in scope when runningnix-shell
in a project using the Coq Nix Toolbox (added to the toolbox Oct 10th 2023). - An example of a
flake
that usescoq-lsp
in a development environment is here https://github.com/HoTT/Coq-HoTT/blob/master/flake.nix .
-
Windows: Experimental Windows installers based on the Coq Platform are available at https://www.irif.fr/~gallego/coq-lsp/
This provides a Windows native binary that can be executed from VSCode normally. As of today a bit of configuration is still needed:
- In VSCode, set the
Coq-lsp: Path
to:C:\Coq-Platform~8.20-lsp\bin\coq-lsp.exe
- In VSCode, set the
Coq-lsp: Args
to:--coqlib=C:\Coq-Platform~8.20-lsp\lib\coq\
--coqcorelib=C:\Coq-Platform~8.20-lsp\lib\coq-core\
--ocamlpath=C:\Coq-Platform~8.20-lsp\lib\
- Replace
C:\Coq-Platform~8.20-lsp\
by the path you have installed Coq above as needed - Note that the installers are unsigned (for now), so you'll have to click on "More info" then "Run anyway" inside the "Windows Protected your PC" dialog
- Also note that the installers are work in progress, and may change often.
- In VSCode, set the
-
Do it yourself! Compilation from sources
- Official Marketplace: https://marketplace.visualstudio.com/items?itemName=ejgallego.coq-lsp
- Open VSX: https://open-vsx.org/extension/ejgallego/coq-lsp
- An experimental configuration for
lsp-mode
has been provided by Arthur Azevedo de Amorim, supporting goal display, see the Zulip thread for more information.
-
Experimental CoqTail support by Wolf Honore: whonore/Coqtail#323
See it in action https://asciinema.org/a/mvzqHOHfmWB2rvwEIKFjuaRIu
- Experimental client by Jaehwang Jung: https://github.com/tomtomjhj/coq-lsp.nvim
- Interact programmatically with Coq files by using the Coqpyt by Pedro Carrott and Nuno Saavedra.
The below projects are using coq-lsp
, we recommend you try them!
- Coqpyt, a Python client for coq-lsp
- CoqPilot uses Large Language Models to generate multiple potential proofs and then uses coq-lsp to typecheck them.
- jsCoq: use Coq from your browser
- Pytanque: a Python library implementing RL Environments
- ViZX: A Visualizer for the ZX Calculus.
- The Waterproof vscode extension helps students learn how to write mathematical proofs.
- Yade: Support for the YADE diagram editor in VSCode.
coq-lsp
discussion channel it at Coq's
Zulip, don't hesitate
to stop by; both users and developers are welcome.
We hold (almost) weekly video conference calls, see the Call Schedule Page for more information. Everyone is most welcome!
See our list of frequently-asked questions.
Unfortunately Coq releases contain bugs that affect coq-lsp
. We strongly
recommend that if you are installing via opam, you use the following branches
that have some fixes backported:
- For 8.20: No known problems
- For 8.19:
opam pin add coq-core https://github.com/ejgallego/coq.git#v8.19+lsp
- For 8.18:
opam pin add coq-core https://github.com/ejgallego/coq.git#v8.18+lsp
- For 8.17:
opam pin add coq-core https://github.com/ejgallego/coq.git#v8.17+lsp
- Current rendering code can be slow with complex goals and messages, if that's
the case, please open an issue and set the option
Coq LSP > Method to Print Coq Terms
to 0 as a workaround. coq-lsp
can fail to interrupt Coq in some cases, such asQed
or type class search. If that's the case, please open an issue, we have a experimental branch that solves this problem that you can try.- Working with multiple files in Coq < 8.17 requires a Coq patch, see below for instructions.
- If you install
coq-lsp/VSCode
simultaneously with theVSCoq
Visual Studio Code extension, Visual Studio Code gets confused and neither of them may work.coq-lsp
will warn about that. You can disable theVSCoq
extension as a workaround. _CoqProject
file parsing library will oftenexit 1
on bad_CoqProject
files! There is littlecoq-lsp
can do here, until upstream fixes this.
- Some problems can be resolved by restarting
coq-lsp
, in Visual Studio Code,Ctrl+Shift+P
will give you access to thecoq-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.
See planned features and contribution ideas for a list of things we'd like to happen.
coq-lsp
mostly implements the LSP
Standard,
plus some extensions specific to Coq.
Check the coq-lsp
protocol documentation for more details.
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.
Both Flèche and coq-lsp
have a preliminary plugin system. The VSCode
extension also exports and API so other extensions use its functionality
to query and interact with Coq documents.
- Ali Caglayan (co-coordinator)
- Emilio J. Gallego Arias (Inria Paris, co-coordinator)
- Shachar Itzhaky (Technion)
- Vincent Laporte (Inria)
- Ramkumar Ramachandra (Inria Paris)
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).
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. Gaëtan Gilbert contributed many key and challenging Coq
patches essential to coq-lsp
; we also thank Guillaume Munch-Maccagnoni for his
memprof-limits
library, which is essential to make coq-lsp
on the real world, as well for
many advice w.r.t. OCaml.
As noted above, the original implementation was based on the Lambdapi LSP server, thanks to all the collaborators in that project!