Install the Rocq Prover

Install the Rocq Prover on Linux

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

The Rocq Prover is also available as a Docker image.

Set Up your Editor for Rocq

After installing the Rocq Prover, you should set up your editor to write Rocq code and proofs.

VS Code / VS Codium (recommended)

  • VsRocq 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. Using opam, you can install it with the following command:

    Starting from version 2025.01, the language server should already be installed if you installed the Rocq Platform.

    The language server is also available as a Nix package.

    For now, vsrocq-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).

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

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

Emacs

Emacs users usually use Proof General to interact with the Rocq Prover. It can be installed from the MELPA repository. It is often complemented with Company-Coq minor mode, which can also be installed from the MELPA repository.

Vim / Neovim

Vim users usually use Coqtail to interact with the Rocq Prover. Various installation methods are documented in the repository's README.

Standalone IDE

The Rocq Prover also has a standalone IDE called RocqIDE. It is distributed as part of the Rocq Platform and is available in many Linux distributions (sometimes as a separate package).

Install the Rocq Prover on macOS

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. Beginners and users who want to get started quickly should use the Rocq Platform binary installer for macOS.
  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.
Download the Rocq Platform binary installer Run the Rocq Platform scripts

Using Homebrew

The Rocq Prover is also available through Homebrew, a package manager for macOS. Similar to the Linux package managers, this presents the limitations of not having all the external packages available for Rocq.

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 Docker

The Rocq Prover is also available as a Docker image.

Set Up your Editor for Rocq

After installing the Rocq Prover, you should set up your editor to write Rocq code and proofs.

VS Code / VS Codium (recommended)

  • VsRocq 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. Using opam, you can install it with the following command:

    Starting from version 2025.01, the language server should already be installed if you installed the Rocq Platform.

    The language server is also available as a Nix package.

    If you have used Homebrew to install the Rocq Prover, there is no language server available yet. You can fall back to using VsCoq Legacy (see below).

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

  • 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. You can install VsCoq Legacy from the Visual Studio Code Marketplace or from Open VSX.

Emacs

Emacs users usually use Proof General to interact with the Rocq Prover. It can be installed from the MELPA repository. It is often complemented with Company-Coq minor mode, which can also be installed from the MELPA repository.

Vim / Neovim

Vim users usually use Coqtail to interact with the Rocq Prover. Various installation methods are documented in the repository's README.

Standalone IDE

The Rocq Prover also has a standalone IDE called RocqIDE. It is distributed as part of the Rocq Platform.

Install the Rocq Prover on Windows

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. Beginners and users who want to get started quickly should use the Rocq Platform binary installer for Windows.
  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.
Download the Rocq Platform binary installer Run the Rocq Platform scripts

Using Opam

If you want to be able to run opam commands directly, it is recommended to first install the Rocq Platform using the scripts. This will set up the environment variables needed to run opam commands.

Using WSL (Windows Subsystem for Linux) or a VM

All the installation methods for Linux are available on Windows Subsystem for Linux (WSL) or in a virtual machine running Linux.

Set Up your Editor for Rocq

After installing the Rocq Prover, you should set up your editor to write Rocq code and proofs.

VS Code / VS Codium (recommended)

  • VsRocq 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 the corresponding language server, which is distributed with the Rocq Platform starting from version 2025.01.

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

  • VsCoq Legacy is a legacy Rocq extension for Visual Studio Code that only relies on the RocqIDE protocol. You can install it from the Visual Studio Code Marketplace or from Open VSX.
  • If you have used WSL to install the Rocq Prover, then you can use the WSL VS Code extension to use a language server running in WSL. In this case, follow the instructions for Linux on how to install the language server.

Emacs

Emacs users usually use Proof General to interact with the Rocq Prover. It can be installed from the MELPA repository. It is often complemented with Company-Coq minor mode, which can also be installed from the MELPA repository.

Vim / Neovim

Vim users usually use Coqtail to interact with the Rocq Prover. Various installation methods are documented in the repository's README.

Standalone IDE

The Rocq Prover also has a standalone IDE called RocqIDE. It is distributed as part of the Rocq Platform.