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:
# 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.
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. 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.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.1 and install it.
opam pin add coq 8.13.1
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 (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.
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.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.13.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.13.1
eval $(opam env)