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 releases but also some older releases (going back to Coq 8.5 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.12 from nixpkgs:
nix-env -f '<nixpkgs>' -iA coq_8_12
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
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.
Thanks to this toolbox, it is easy to test the current development version of Coq:
nix-shell https://coq.inria.fr/nix/toolbox --argstr job coq --arg override '{coq = "master";}'
or even the version in an open PR:
nix-shell https://coq.inria.fr/nix/toolbox --argstr job coq --arg override '{coq = "#NNNNN";}'
To the extent possible under law, the contributors of the Rocq wiki have waived all copyright and related or neighboring rights to their contributions.
By contributing to the Rocq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.