For now, OPAM for Coq does not support Windows.
opam repo add coq-released https://coq.inria.fr/opam/releasedand 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 coqand specify the version to install:
opam pin add coq 8.4.6
If you list your installed packages:
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.
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:
Update the list of available packages (do not upgrade the currently installed packages):
See the full description of a package:
opam show coq-io-hello-world
To make a package, read the make a Coq package blog post.
To upgrade your packages, run:
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.
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.
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.
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