coq Getting started with coq Installation with Nix

Example

Warning: this is not the standard way of installing Coq.

For users of Linux (and MacOS) who wish to gain access to up-to-date versions of Coq or to be able to use several versions of Coq on the same machine, without the hassle of using opam, and without having to compile from source, this is an alternative solution.

Nix is a package manager for Unix-type OS such as Linux and MacOS. It comes with its own collection of packages which is generally kept much more up-to-date than Debian's or Ubuntu's. It does not conflict with your distribution's package manager because it does not install anything in /usr/bin and such.

First, you need to install Nix:

$ curl https://nixos.org/nix/install | sh

To ensure that the necessary environment variables are set, either log in again, or type:

. $HOME/.nix-profile/etc/profile.d/nix.sh

Then the following command will install the latest version of Coq:

$ nix-env -iA nixpkgs.coq_8_6

You can also run CoqIDE without adding anything to your PATH:

$ nix-shell -p coq_8_6 --run coqide

Similarly (supposing you already have Emacs and Proof-General installed):

$ nix-shell -p coq_8_6 --run emacs

This is very useful to run different versions when you need them. For instance, to run Coq 8.5 use the following command:

$ nix-shell -p coq_8_5 --run coqide