Installing Coq via OPAM

What is OPAM

OPAM is the package manager for the OCaml programming language, the language in which Coq is implemented. Instructions on how to install OPAM itself are available on the OPAM website.

By following the instructions on this web page one installs the last stable version of Coq and all additional packages in the directory ~/opam-coq.8.9.0. Instructions target an OPAM newcomer.

Using OPAM to install Coq

Once the opam command is available, i.e. OPAM is installed, one can proceed as follows (using opam 2):

export OPAMROOT=~/opam-coq.8.9.0 # installation directory
opam init -n --comp=ocaml-base-compiler.4.02.3 -j 2 # 2 is the number of CPU cores
opam repo add coq-released
opam install coq.8.9.0 && opam pin add coq 8.9.0

If using opam 1.2, the init command should be:

opam init -n --comp 4.02.3

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. for Proof-General.

Running Coq

Every time a new shell is opened one has to type in the following lines in order to use Coq

export OPAMROOT=~/opam-coq.8.9.0
eval `opam config env`

After that coqc -v shall run and print the version of Coq.

Using OPAM to install Coq packages

If Coq has been installed as described above, the list of available Coq packages can be accessed as follows

opam search coq

The command lists the Coq package names followed by a short description. 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