Coq

Installation

The Coq proof assistant and associated tools (CoqIDE, coqtop, coqc, coq_makefile, …) may be installed globally, by a user, in its profile:

nix-env -iA nixpkgs.coq

Coq can also be run in a local, ephemeral, environment. For instance, the following command will launch CoqIDE without installing it:

nix-shell --packages coq --run coqide

Using libraries

A few third-party libraries are available under the coqPackages attribute set.

A simple way to use such a library is within a temporary shell, e.g.,

nix-shell --packages coq coqPackages.mathcomp

This will open a shell in which both Coq and the Mathematical Components library are available. Notice that even if Coq is globally installed, it is required to list it as an input of the shell.

Global installation of libraries

It is possible to globally install a Coq library as any other Nix package. Notice however that it will not be automatically visible to Coq. Coq search for libraries in the directories that are listed in the COQPATH environment variable. When using Coq in a Nix shell (as described above), this variable is automatically populated with paths to the Coq libraries that are provided by the shell inputs. You may manually define this variable to point to your profile, e.g.,

export COQPATH=$HOME/.nix-profile/lib/coq/8.7/user-contrib