Rocq LSP

Github CI

coq-lsp is a Language Server for the Rocq Prover. It provides a single server that implements:

Key features of coq-lsp are: continuous, incremental document checking, real-time interruptions and limits, programmable error recovery, literate Markdown and LaTeX document support, multiple workspaces, positional goals, information panel, performance data, completion, jump to definition, extensible command-line compiler, a plugin system, and more.

coq-lsp is built on Flèche, a new document checking engine for formal documents based on our previous work on SerAPI and jsCoq.

Designed for interactive use and web-native environments, Flèche is extensible and supports advanced tooling integration and capabilities beyond standard Rocq.

See the User Manual and the General Documentation Index for more details.

This repository also includes the coq-lsp Visual Studio Code editor extension for the Rocq Proof Assistant, and a few other components. See our contributing guide for more information. Support for Emacs, Vim and Neovim is also available in their own projects.

Quick Install:

$ opam install coq-lsp && code --install-extension ejgallego.coq-lsp
 (use-package rocq-mode
    :vc (:url "https://codeberg.org/jpoiret/rocq-mode.el.git"
         :rev :newest)
    :mode "\\.v\\'"
    :hook
    (rocq-mode . rocq-follow-viewport-mode)
    (rocq-mode . rocq-auto-goals-at-point-mode))

Table of Contents

🎁 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.

Incremental checking

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!

👁 On-demand, Follow The Viewport Document Checking

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:

On-demand checking

🧠 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. 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!

Smart error recovery

🥅 Whole-Document Goal Display

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.

Whole-Document Goal Display

Goal display behavior is configurable in case you'd like to trigger goal display more conservatively.

🗒️ Markdown and LaTeX Support

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.

Coq + Markdown Editing

Moreover, you can use the usual Visual Studio Code Markdown or LaTeX preview facilities to render your markdown documents nicely!

👥 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 Outline Demo Document Symbols

🐝 Document Hover

Hovering over a Coq identifier will show its type.

Types on Hover

Hover is also used to get debug information, which can be enabled in the preferences panel.

📁 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.

Stats on Hover

🔧 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.

Configuration screen

🖵 Extensible, Machine-friendly Command Line Compiler

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.

🪄 Advanced APIs for Coq Interaction

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.

♻️ 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 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.

🏘️ Supported Coq Versions

coq-lsp supports Rocq 9.0, 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 Rocq 9.0 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

🏓 Server

🫐 Visual Studio Code

🦄 Emacs

The official Rocq Emacs mode is https://codeberg.org/jpoiret/rocq-mode.el , maintained by Josselin Poiret with contributions by Arthur Azevedo de Amorim.

✅ Vim

🩱 Neovim

🐍 Python

⇨ coq-lsp users and extensions

The below projects are using coq-lsp, we recommend you try them!

🗣️ 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

Coq upstream bugs

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:

Known problems

Troubleshooting

📔 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 and Extending the System

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.

🥷 Team

🕰️ Past Contributors

©️ Licensing Information

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

👏 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. 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.

rocq-lsp includes several components and tests from SerAPI, including serlib, goal display code, etc... Thanks to Karl Palmskog and all the SerAPI contributors.

As noted above, the original implementation was based on the Lambdapi LSP server, thanks Frédéric Blanqui, Rodolphe Lepigre and all Lambdapi contributors.