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.
opam
manuallyIn 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
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:
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 vscoq-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 Vscoq: 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 rocqtop)
to find the corresponding path.