Installing Coq

We require the students to come with laptop on which Coq 8.18.0 is already installed. We additionally require MetaCoq 1.2.1 and Equations 1.3. The easiest way to install all of them at once, together with CoqIDE is to install the Coq Platform 2023.11.0 at the extended level.

You have several options: installing the Coq Platform from binaries, or installing the packages separately using opam. If you elect other ways to install Coq (eg. using Nix) then we may not be able to help you. In any case, check that everything works as expected on the test file we provide.

Important

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

Installing the platform from binaries

Installation should be as simple as downloading the binaries corresponding to your OS Coq Platform release and installing them. You may further read instructions corresponding to your OS: macOS, Windows or Linux.

You can also follow instructions in there to find alternative ways to install the extended level of the platform.

Warning

If you are on macOS make sure to read the notes towards the end of the file: macOS will probably refuse to launch CoqIDE unless you open your system settings and explicitly allow it to run.

Installing directly from opam

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 coq-released https://coq.inria.fr/opam/released
opam update
opam install coq.8.18.0 coq-metacoq-template.1.2.1+8.18 coq-equations.1.3+8.18

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

opam switch create coq.8.18
opam pin add coq 8.18.0
opam install coq-metacoq-template.1.2.1+8.18 coq-equations.1.3+8.18

Which editor to use?

We recommend you use either CoqIDE or Visual Studio Code (VSCode)/VSCodium with the VSCoq extension. The Coq website has a page listing most available options in case you really want to use a different editor.

If you installed the Coq Platform, then you should have CoqIDE ready to go with the correct version. It should be the simplest tool to use as the interface is built exactly for Coq. You can press button to evaluate a file etc.

VSCoq will let you use a more modern approach. Install VSCoq Legacy for VSCode or VSCodium. If you have installed Coq via opam, then it should be in your PATH and VSCoq 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 Coq installation). In case it doesn’t find it automatically—e.g. if you installed the Coq Platform—then you can try to launch VSCode from a terminal that finds Coq by running

code .

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

dirname $(which coqtop)

to find the corresponding path.

Advanced users: VSCoq2

For now, we recommend you use VSCoq Legacy, but a brand new version, VSCoq2, has been out for some time and is likely to be the default editor to use in the future. For now, it requires installing Coq with opam, and then the vscoq-language-server from opam too.

opam install vscoq-language-server