The Coq Proof Assistant

What is opam?

Opam is the package manager for the OCaml programming language, the language in which Coq is implemented. Opam 2.1 is the recommended version, and is assumed below. Instructions on how to install opam itself are available on the opam website. The following command displays the version of opam you have installed:

# Make sure opam version is 2.1.0 or above.
opam --version

Follow the instructions below to install the last stable version of Coq and additional packages. The instructions target an opam newcomer.

Note that these instructions will also work for Opam 2.0 but this may require you to manually install any external dependencies. In this case you will have to use opam-depext to see which external dependencies are missing.

For some operating systems, opam and opam-depext might still be unable to detect external dependencies, which will mean you have to check and install them yourself. To see more detailed information on external dependencies please consult the INSTALL.md documentation in the GitHub repository.

The Coq platform scripts

The Coq platform provides interactive scripts that allow installing Coq and a standard set of packages through opam without having to learn anything about opam.

If a standard setup works for you, then we recommend that you use these scripts. If you do, you can skip directly to Using opam to install Coq packages to learn how to add additional packages to the initial package set provided by the platform.

Note that the platform scripts are compatible with existing opam installations. They will create a fresh switch.

If you prefer to do a fully manual installation, you can proceed to the next section.

Initializing opam

Once opam is installed, it must be initialized before first usage:

opam init
eval $(opam env)

opam init will prompt you to allow opam to set up initialization scripts, which is generally fine to accept. Otherwise, every time a new shell is opened you have to type in the eval $(opam env) command above to update environment variables.

By default, opam will use the global installation of OCaml. You can initialize opam with an explicit compiler version, for example 4.10.2, with the option --compiler=ocaml-base-compiler.4.10.2. See also the section "Managing different versions of OCaml and Coq" below, about switches and roots.

Installing Coq

To install Coq, simply run the following command. Note that installing Coq using opam will build it from sources, which will take several minutes to complete:

# Pin the coq package to version 8.15.1 and install it.
opam pin add coq 8.15.1

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

opam pin add coq $NEW_VERSION

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

Installing CoqIDE

You may also want to install CoqIDE. Note that this requires GTK+ development files (gtksourceview3) to be available on the system. Opam (>=2.1) will ensure that these packages are installed (on most operating systems). To install CoqIDE, simply run:

opam install coqide

There exist many alternative user interfaces / editor extensions for Coq. See their respective websites for instructions on how to install them.

Using opam to install Coq packages

Coq packages live in a repository separate from the standard OCaml opam repository. The following command adds that repository to the current opam switch (you can skip this step if you used the platform scripts):

opam repo add coq-released https://coq.inria.fr/opam/released

The following command lists the names of all Coq packages along with short descriptions:

opam search coq

You can access a more detailed description of a package, say coq-sudoku, using the command:

opam show coq-sudoku

You can then install the package using the command:

opam install coq-sudoku

Managing different versions of OCaml and Coq

By default, opam will use the global OCaml installation. Opam can handle different versions of OCaml and other packages (including Coq) via switches or roots.

Switches

Switches provide separate environments, with their own versions of OCaml and installed packages. More information about opam switches can be found here.

The following command creates a switch named with-coq with OCaml 4.10.2:

# Run one of the following depending on your version of opam
opam switch create with-coq 4.10.2

Change to an existing switch named other-switch with this command:

opam switch other-switch
eval $(opam env)

Roots

Opam stores all its configuration (including switches) in a directory called root (by default, ~/.opam). The path to the root can be set using the $OPAMROOT environment variable, providing an alternative way of creating fresh opam environments.

The main benefit of roots is that they can be used simultaneously, but they require some external bookkeeping. In comparison. switches are entirely managed by opam, and they can share the global configuration of a single root.

# Set a new root location export
OPAMROOT=~/.opam-coq.8.15.1

# Initialize the root with an explicit OCaml version.
opam init -n --compiler=ocaml-base-compiler.4.10.2

# Install Coq in this new root (same commands as above)
opam pin add coq 8.15.1

Every time a new shell is opened, or you want to use a different root, type in the following lines:

export OPAMROOT=~/.opam-coq.8.15.1
eval $(opam env)

I still need help!

If the above does not work for you, or you are confused, then feel free to open a topic on Zulip or our other communication channels.