## 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
```