Get started

Install

For now, OPAM for Coq does not support Windows.

First, install the OPAM package manager as explained on install OPAM, and check that you have an external solver. Then, activate the Coq repository:

opam repo add coq-released https://coq.inria.fr/opam/released
and install the latest version of Coq:
opam pin add coq `opam show --field=version coq`
To install a specific version of Coq, list all the Coq versions:
opam show --field=available-versions coq
and specify the version to install:
opam pin add coq 8.4.6

If you list your installed packages:

opam list

you should get something like:

# Installed packages for system:
base-bigarray         base  Bigarray library distributed with the OCaml compiler
base-no-ppx           base  A pseudo-library to indicate lack of extension points support
base-threads          base  Threads library distributed with the OCaml compiler
base-unix             base  Unix library distributed with the OCaml compiler
camlp5                6.14  Preprocessor-pretty-printer of OCaml
coq                  8.4.6 (pinned)  Formal proof management system.

Use

Install a package:

opam install coq-io-hello-world

Install a package in a specific version:

opam install coq-io-hello-world.1.1.0

List the currently installed packages:

opam list

Update the list of available packages (do not upgrade the currently installed packages):

opam update

See the full description of a package:

opam show coq-io-hello-world

Add a package

To make a package, read the make a Coq package blog post.

FAQ

Upgrade

To upgrade your packages, run:

opam upgrade

Be cautious that this command may break your developments, by introducing breaking changes in your dependencies. This command does not upgrade Coq if this package is pinned.

Pinning of Coq

This is not necessary to pin Coq. Actually, you can install Coq like any other package. But we recommend you to pin Coq because new versions of Coq often introduce breaking changes.

Have several Coq versions

This is a common situation to need to work with different versions of Coq or libraries. The OPAM package manager provides the opam switch command to switch between different working environments, each working environment being defined by an OCaml version. You can also use the --root= option to change the folder in which you install the OPAM files, in order to have several independent installations of OPAM.

Coq beta

The development versions of Coq are in a separated repository. Activate it with:

opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev