Nix

The Nix package manager can be used on any Linux distribution or on macOS or on Windows (thanks to Windows Subsystem for Linux). It is a source-based package manager with a binary cache.

The nixpkgs collection includes packages for the latest Coq releases but also many older releases (going back to Coq 8.6 at the time of writing): when installing any of these Coq versions, the package binary will be fetched from Nix's official binary cache.

The collection also includes many Coq libraries and plugins. These packages are available in the official binary cache for the default version of Coq. For other stable versions, you should install the coq-community binary cache, otherwise Nix will build these packages from sources.

You can find the available packages (for the default version of Coq) thanks to Nix search.

The following command will install Coq 8.16 from nixpkgs:

nix-env -f '<nixpkgs>' -iA coq_8_16

The following command will open a shell where the default Coq version and the Bignums package are available (and $COQPATH has been set properly):

nix-shell -p coq coqPackages.bignums

Or using Nix flakes and the Nix 2.0 CLI:

nix shell nixpkgs#coq nixpkgs#coqPackages.bignums

CoqIDE

Starting with Coq 8.14, CoqIDE is split into a separate package. Note that you still need to explicitly request Coq to avoid CoqIDE silently picking a globally installed version of Coq (see #16521). So to get CoqIDE 8.15, you can do the following:

nix-shell coq_8_15 coqPackages_8_15.coqide --run coqide

Or with Nix flakes:

nix shell nixpkgs#coq_8_15 nixpkgs#coqPackages_8_15.coqide -c coqide

And for versions older than Coq 8.14, the following works:

nix-shell coq_8_12 --run coqide

or

nix shell nixpkgs#coq_8_12 -c coqide

Also note the buildIde = true; argument in the Overriding Coq section below.

Coq Nix Toolbox

A Nix toolbox is available at https://github.com/coq-community/coq-nix-toolbox to simplify setting up a project for use with Nix and generating CI configuration files. See the documentation on this repository to learn more. See also: https://github.com/coq-community/manifesto/wiki/Continuous-Integration-with-Nix.

Overriding Coq

The Coq derivation supports several arguments, whose value can be overridden, including a very powerful version argument (see the description of the supported values here). In particular, it is easy to test the current development version of Coq:

nix-shell -p 'coq.override { version = "master"; buildIde = true; }' --run coqide

or even the version in an open PR:

nix-shell -p 'coq.override { version = "#NNNNN"; buildIde = true; }' --run coqide

Historic Coq versions using Nix

As already explained above, many Coq versions are available through nixpkgs, and you can get access to them using a version specific attribute. By overriding Coq, you can get an even larger number of versions, such as previous patch-level releases which are known to nixpkgs, but not exposed through an attribute. See the list of known releases in the Coq derivation source: https://github.com/NixOS/nixpkgs/blob/nixos-22.05/pkgs/applications/science/logic/coq/default.nix#L201. Finally, you can also use an older nixpkgs version (see the list below) to get any previously available Coq version and have some assurance that it will compile fine. Note that since all the dependencies will come from this old nixpkgs version, this may eat much more disk space than the previous solutions.

Nixpkgs Version List

Here are a list of hashes for nixpkgs where a version of Coq was introduced.

Each major version of Coq may have several patch-level releases, so the specific nixpkgs hash in which each of those has been introduced is provided. Note that new nixpkgs still support the older versions of Coq if the coq_X_Y package name is used. Newer nixpkgs may however drop support for these older versions.

Coq Ver               nixpkgs SHA                    CoqIDE package
V8.16.0 a037a50b4696632977dadd61747b02492a109478 coq_8_16 coqPackages_8_16.coqide
V8.15.2 442db9429b9fbdb6352cfb937afc8ecccfe2633f coq_8_15 coqPackages_8_15.coqide
V8.15.1 3d0a9d166851548a7182ca7e4fadd1425e125757 coq_8_15 coqPackages_8_15.coqide
V8.15.0 20e7213d16eef3c3591f0452796b8d42245da865 coq_8_15 coqPackages_8_15.coqide
V8.14.1 48406e3fca5be837df5cfa3a5b891dd3d6557e1b coq_8_14 coqPackages_8_14.coqide
V8.14.0 e242eef8a45f7e149f7af64ae07e0c45ab51c044 coq_8_14 coqPackages_8_14.coqide
V8.13.2 ab16ad87649b6ea845be46fa7df7e9466ed4e05d coq_8_13
V8.13.1 cd43a539477b1b7a5af4edb70b500184beaf240b coq_8_13
V8.13.0 813d14b9b7769a4550fbf9a42fa8af779ab6c475 coq_8_13
V8.12.2 c5556b7454f733cf7c2528a8c131c56b2dbd34bc coq_8_12
V8.12.1 2806eb27431abf2ffcff7404783198c4b767e6de coq_8_12
V8.12.0 b8dfca143c5b9e632530720ab472bd54d9d21137 coq_8_12
V8.11.2 48f0d8b3c8678185420231e8cda1139794325dee coq_8_11
V8.11.1 d6a8d0ca5b03dbdb84070b47021b2b852429348e coq_8_11
V8.11.0 13dd5844fdf4be744c359f8559f8727011cb7bf1 coq_8_11
V8.10.2 3806eff9ca233b9b3580a8421b52c2db8e60c6bf coq_8_10
V8.10.1 a8892b0d76b02210b0c37e180b9db6535f001ab0 coq_8_10
V8.10.0 b4db381443ed25a2664a12ca110f9a2a44c1b4bc coq_8_10
V8.9.1  57c3da07eb8524dd8ba9a000c2003f762af50bfa coq_8_9
V8.9.0  b76961124d938dae59e4c9db90832b87ccb1b42b coq_8_9
V8.8.2  23900febe79a3a6aaab1276cde8689e0fa3f3d5c coq_8_8
V8.8.1  314eb884ecd22803db4149936a2c95b48ad2f60b coq_8_8
V8.8.0  76a43d765cc9d5ed31d275abfe28b52f842f6b15 coq_8_8
V8.7.2  90252481bfe233c3fe5a54f9d6d73e93f08e1e27 coq_8_7
V8.7.1  40627000f773d7a51b496f07be29b8498c1324a7 coq_8_7
V8.7.0  89720d851aafe7be2aafc129fd729941a4db18af coq_8_7
V8.6.1  c0dca2fb00a4e94f995b2752c78f4e67a6c6e7c8 coq_8_6
V8.6    a30e8db9f04315730f83f324c4079f69bbac44a5 coq_8_6
V8.5    a30e8db9f04315730f83f324c4079f69bbac44a5 coq_8_5
V8.4pl5 2b9e43b513bb2c85eb59826b32ab3eba565d5a0c coq_8_4
V8.4pl4 5bbcebf2dbe29b7e17d718db6b774991e3070748 coq_8_4
V8.4pl3 fa118fc6777d5ddaf8e91911b007a642c7e10b73 coq_8_4
V8.4pl2 c9f59592851036eef99ac2ed2096aa46935531ec coq_8_4
V8.4    706cbc9318ef56d76a48883d9a0b6539e30985c7 coq_8_4
V8.3pl3 699de0f3f9ec9e03ca2792c1667308dbf86d9f3e coq_8_3
V8.3pl1 bec1a9c44f4b07ebd80a7257271b8c3bf57ace0a coq_8_3
V8.3    0430167083c1cdca354b295f87290d7b10a930e7 coq_8_3
V8.2pl2 c0f343b7527e5c706dfc687b4bd0f17143afd0ef ??
V8.2pl1 a0207b3dc7ff3583df37f2bb8bab939390f964c7 No CoqIDE!
V8.1pl2 12ca68d11447fc5e9d3163caf822b6e98b3a65af No CoqIDE!