Install Coq with opam

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:

opam --version

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

Initialize opam

Once opam is installed, it must be initialized before its 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.

Install Coq

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

Pinning prevents opam from upgrading Coq automatically, as it may cause inadvertent breakage in your Coq projects. You can choose to upgrade Coq explicitly to $NEW_VERSION with essentially the same command:

opam pin add coq $NEW_VERSION

To check that the installation was successful, coqc -v should print the version of Coq.

Install CoqIDE

One may also want to install CoqIDE. Note that this requires GTK+ development files (gtksourceview2) to be available on the system.

opam install coqide

For alternative user interfaces / editors, see instructions on their own homepage, e.g. https://proofgeneral.github.io/#quick-installation-instructions for Proof General.

Using opam to install Coq packages

Coq packages live in a repository separate from the standard OCaml repository. The following command adds that repository to opam:

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

The next command lists all the Coq package names followed by a short description:

opam search coq

One can access a more detailed description of a package, say coq-sudoku, by typing

opam show coq-sudoku

One can install the package by typing

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

# 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.10.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.10.1
eval $(opam env)