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 http://coq.inria.fr/opam/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. https://proofgeneral.github.io/#quick-installation-instructions 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
Syndicate