Install Rocq

If you need more explicit instructions than provided on this quick-install page, you can find a more detailed explanation of the installation process here.

Install Rocq using the Rocq Platform (recommended)

Rocq 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 are encouraged to use one of the binary installers: we provide binary installers for Windows and macOS.

    Windows and macOS installers

  2. Experienced users (and Linux users) are advised to run the Rocq Platform scripts to install from sources, as this will allow them to install additional packages with opam.

    Platform scripts

Congratulations, you have now installed Rocq!

Install Rocq using Opam

  1. Install the opam package manager

    opam, the package manager for both OCaml and Rocq, can install the OCaml compiler, the Rocq prover, as well as any additional packages. Ensure gcc, build-essential, curl, unzip, and bubblewrap are installed on your system, then run the following in your terminal to download and install the newest version of opam:

    Other Installation Methods You can also install opam using your operating system's package manager - however, you may get an older version of opam that does not support the most recent OCaml compiler version. If you need the most recent version, you can build opam from sources, following the instructions at opam's GitHub repository.

  2. Initialise opam

    Opam needs to be initialised, which will create a default opam switch. An opam switch is an isolated environment for the OCaml compiler and any packages you install.

    During opam init, you will be asked if you want to add a hook to your shell to put the tools available in the current opam switch on your PATH.

  3. Activate the opam switch

    If you answered no when prompted in the previous step, you need to activate the opam switch by running eval $(opam env) or explicitly execute commands within the switch by using opam exec -- [CMD].

  4. Installing the Rocq Prover

    To install the Rocq Prover, simply run the following command. It will pin the Rocq package to version 9.0.0 and install it. Note that installing the Rocq Prover using opam will build it from sources, which will take several minutes to complete:

    Pinning prevents opam from upgrading Rocq automatically, to avoid causing inadvertent breakage in your Rocq projects. You can upgrade Rocq explicitly to $NEW_VERSION with essentially the same command:

    To ensure that installation was successful, check that rocq -v prints the expected version of Rocq.

Congratulations, you have now installed Rocq!

Set Up a VS Code for using Rocq

VsRocq is an extension for Visual Studio Code (VS Code) and VSCodium which provides support for the Rocq prover. It is built around a language server which natively speaks the LSP protocol. To install the language server in your current opam switch, run this command:

You can alternatively install rocq-lsp (and its corresponding VS Code extension).

If you would like to use a different editor, several alternatives (including Emacs and Vim) are supported. Check the corresponding documentation for more information.

Now you are ready to write some Rocq code and proofs!

Take A Tour of Rocq

Other Installation Methods

  1. The Rocq Prover is available through many package managers, including most Linux distribution package managers. However, in many cases, the available version is not the latest version. More importantly, these distributions might provide only a fraction of all the external packages available for Rocq, thus requiring some manual compilation and installation to add additional packages.
  2. Advanced users who want to install Rocq and extend it with external packages can rely on Nix.

    Nixpkgs manual section on Rocq

  3. Rocq is also available as a

    Docker image.

Congratulations, you have now installed Rocq!