Install the Rocq Prover on Linux

Using the Rocq Platform (Recommended)

The Rocq Prover has a rich ecosystem of external packages (libraries and plugins) that extend it and make it more powerful. The Rocq Platform provides an easy way to install Rocq and a consistent set of packages on Windows, macOS and Linux.

  1. Currently, there is no longer a Rocq Platform binary installer for Linux.
  2. The Rocq Platform scripts install the Rocq Prover and its packages from sources, while abstracting over the details of running opam. This provides the flexibility to install additional packages with opam later on. It also supports installing multiple versions of the Rocq Platform and switching between them.
    3. Run the Rocq Platform scripts

Using Opam

If you want some finer-grained control over the installation process, you can install the Rocq Prover by running opam commands directly.

Install Rocq using Opam

Using Nix

Nix support for the Rocq Prover is well-maintained and provides a way to install the Rocq Prover and its packages on any Linux distribution, or on macOS. See the Nix installation instructions and the Nixpkgs manual section on Rocq for more information.

Using your system's package manager

The Rocq Prover is available through many package managers, including most Linux distribution package managers. While this is currently the easiest way to install the Rocq Prover, it has the following limitations:

  • Depending on the distribution, the available version may not be the latest version. See Repology to know which version is available in your distribution.
  • The available packages may not include all the external packages available for the Rocq Prover. Installing additional packages may require manual compilation and installation.

Using Docker

The Rocq Prover is also available as a Docker image.

Set Up VS Code / VS Codium for Rocq

After installing the Rocq Prover, you should set up VS Code or VS Codium to write Rocq code and proofs.

VsCoq (Recommended)

The renaming of VsCoq to VsRocq is in progress.

VsCoq is the official Rocq extension for Visual Studio Code. It is available in the Visual Studio Code Marketplace and on Open VSX. To use it, you need to install the corresponding language server.

Be careful, that there is a version of the extension per version of the language server. Both version need to be the same for the extension to work.

Install VsCoq

Starting from version 2025.01, the language server should already be installed if you have installed the Rocq Platform, so you should not try to install it again.

If you are using opam, you can install the language server with the following command:

The language server is also available as a Nix package.

For now, vscoq-language-server is not available in all Linux distributions that have the Rocq Prover. If you have used your Linux distribution's package manager to install the Rocq Prover and it does not include the language server, you can fall back to using VsCoq Legacy (see below).

Troubleshooting

In case of installation troubles, or a bug with the extension please report on the dedicated Zulip stream. In which case, please mention:

  • your operating system (Linux),
  • the version of Rocq and of the language server you have installed,
  • the installation method used to install Rocq, and the language server
You can access setup information, and if needed logs, by clicking on the Rocq button. It is is displayed in the top-right corner when viewing a .v file, provided the extension is installed.

Coq LSP

Coq LSP is an alternative language server and VS Code extension for the Rocq Prover featuring hybrid Rocq/markdown document support.

VsCoq Legacy

VsCoq Legacy is a legacy Rocq extension for Visual Studio Code that only relies on the RocqIDE protocol and therefore does not require installing a language server. Linux distributions that have the Rocq Prover usually also install the RocqIDE server in their main package. You can install VsCoq Legacy from the Visual Studio Code Marketplace or from Open VSX.