Installing Rocq

We require the students to come with laptop on which Rocq 9.0.0 is already installed. We additionally require MetaRocq (the rocq-metarocq-template opam package is enough) and Equations 1.3.1.

The Rocq website has a page dedicated to installing the system and a corresponding editor, but it currently recommends the Rocq platform, which for now only provides Coq 8.20 (the previous version of Rocq). We will list various options that are valid for this course. If you elect other ways to install Rocq (e.g. using Nix) then we may not be able to help you.

Tip

Check ahead of time whether everything works as expected using the test file we provide.

Important

Please contact us ahead of time if you have trouble installing Rocq or checking that the test file works.

Installing from opam manually

In case you want to use the OCaml package manager opam, first make sure you have opam 2 installed. Then run the following commands:

opam repo add rocq-released https://rocq-prover.org/opam/released
opam update
opam install rocq-prover.9.0.0 rocq-metarocq-template

If you plan to use multiple versions of Rocq, then you can create an opam switch for each Rocq version. You can also use pinning to make sure you do not inadvertently change the Rocq version by running opam upgrade.

opam switch create rocq.9.0 # <-- you can use any name you want instead of rocq.9.0
opam pin add rocq-prover 9.0.0
opam install rocq-metarocq-template

Running the Rocq platform scripts

You may want to use the current preview for the Rocq platform by following the appropriate instructions corresponding to your OS and making sure you use the pick listed above:

Which editor to use?

We recommend you use Visual Studio Code (VSCode) or VSCodium (its free-software alternative) with the VSRocq extension. The Rocq website has a page listing most available options in case you want to use a different editor.

You can install VSRocq from:

Note that also need to install the corresponding language server (the extension will warn you to do it in case you haven’t). You can also do it from opam:

opam install vsrocq-language-server

If you have installed Rocq via opam, then it should be in your PATH and VSRocq should pick it up (if you open a .v file, such as the test file we provide, it will complain if it did not find a Rocq installation). In case it doesn’t find it automatically then you can try to launch VSCode from a terminal that finds Rocq by running

code .

If it doesn’t work, you can open the settings for VSCode and search for Vsrocq: Path, this will let you add the path to the folder containing the Rocq binary. It depends on where you installed it. If you have a terminal which finds rocq then you can run

dirname $(which rocq)

to find the corresponding path.