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 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.0.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.

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.05.0, with the option --compiler=ocaml-base-compiler.4.05.0. See also the section "Managing different versions of OCaml and Coq" below, about switches and roots.

Installing Coq

Depending on your operating system, installing Coq using opam may require you to first install some system packages. The recommended way to determine the names of required system packages is via the opam-depext tool:

opam install opam-depext
opam-depext coq

For example, on Debian / Ubuntu, this command may list the m4 system package, which can then be installed as follows:

sudo apt-get install m4

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.13.0 and install it.
opam pin add coq 8.13.0

Pinning prevents opam from upgrading Coq automatically, which may cause 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. As for Coq, names of system packages to install can be determined using opam-depext:

opam-depext coqide

After the listed system packages have been installed, CoqIDE can be built and installed with the following command:

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 (more on switches below):

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.

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

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

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.13.0

# Initialize the root with an explicit OCaml version.

opam init -n --compiler=ocaml-base-compiler.4.05.0

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

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.13.0
eval $(opam env)