Home

Awesome

Coq Nix Toolbox

General presentation

The Nix package manager is a package manager with a strong focus on reproducibility and isolation.

The Coq Nix Toolbox is a set of helper scripts to ease setting up a Coq project for use with Nix, for Nix and non-Nix users alike. One of its main features is to generate GitHub Actions configuration files to continuously test a Coq project and its reverse dependencies.

Besides Nix, the Coq Nix Toolbox relies on the nixpkgs package repository and its large collection of Coq packages.

The Coq Nix Toolbox provide the following features:

  1. It can generate GitHub Actions configuration files to trigger a CI for your Coq project and its reverse dependencies. This CI uses the Nix packaging system and a caching mechanism called Cachix.

  2. It offers Nix configurations files so that one can locally obtain a shell with all dependencies preloaded by simply running nix-shell in the development root directory.

  3. Multiple versions of dependencies (typically different versions of Coq) can be easily handled with "bundles" of (reverse) dependency versions/git refs.

  4. One can retrieve locally builds already performed on CI thanks to Cachix.

How to use

Standalone

Installing Nix locally is a prerequisite for this installation method (but a good thing to do anyway to take the most advantage of this toolbox). See https://nixos.org/download.html. Additionally, in order to use binary caches from recognized organizations, please do

nix-env -iA nixpkgs.cachix && cachix use coq && cachix use coq-community && cachix use math-comp

This only needs to be performed once, after the installation of Nix.

Then, run the following commands at the root of your project (using a project-specific name instead of YOURPACKAGENAME, below) :

nix-shell https://github.com/coq-community/coq-nix-toolbox/archive/master.tar.gz --arg do-nothing true --run generateNixDefault
nix-shell --arg do-nothing true --run "initNixConfig YOURPACKAGENAME"

This will create an initial .nix/config.nix that you should now manually edit. This file contains comments explaining each available option.

Once you have finished editing .nix/config.nix, you may generate GitHub Actions workflow(s) by running:

nix-shell --arg do-nothing true --run "genNixActions"

Do not forget to commit the new files.

Later, you may want to update to the latest version of the toolbox and regenerate GitHub Action workflow(s) by running:

nix-shell --arg do-nothing true --run "updateNixToolBox & genNixActions"

Overlays

You can create directories named after a Coq package and containing default.nix files in .nix/coq-overlays to override the contents of coqPackages. This can be useful in the following case:

To amend a package already present in nixpkgs, just run nix-shell --arg do-nothing true --run "fetchCoqOverlay PACKAGENAME". To create a package from scratch, run nix-shell --arg do-nothing true --run "createOverlay PACKAGENAME" and refer to the nixpkgs documentation available at https://nixos.org/manual/nixpkgs/unstable/#sec-language-coq.

Bundles and jobs

Bundles are defined in your config.nix file. If you didn't change this part of the auto-generated file, you have a single bundle called "default". Bundles are used to create sets of compatible packages. You can override the version of some packages and you can explicitly exclude some incompatible packages.

Jobs represent buildable outputs. You can build any package in coqPackages (including any package defined in your .nix/coq-overlays directory) with the following command:

nix-build --argstr job PACKAGENAME

One can replace PACKAGENAME with:

If the package depends on your main package, then it will use its local version as a dependency.

You can also specify the bundle to use like this:

nix-build --argstr bundle BUNDLENAME --argstr job PACKAGENAME

In case the bundle argument is omitted, the default bundle defined in config.nix is used.

If, for instance, you need to fix a reverse dependency of your project because it fails in CI, you can use the following command to get the dependencies for this reverse dependency:

nix-shell --argstr bundle BUNDLENAME --argstr job PACKAGENAME

This command will build all the dependencies of PACKAGENAME, including your project from the current sources. If these correspond to a version that has been tested in CI and you have activated Cachix (both so that CI pushes to it and on your local machine to use it), then this step should only fetch pre-built dependencies.

Again, the bundle argument is optional.

Available shell hooks

When you run nix-shell, you get an environment with a few available commands:

These three commands update the nixpkgs version to use (will create or override .nix/nixpkgs.nix):

After one of these three commands, you should leave and re-enter nix-shell if you want the update to be taken into account (e.g., before calling genNixActions).

Arguments accepted by nix-shell

One can pass the following arguments to nix-shell or nix-build:

Testing coqPackages updates in nixpkgs

To test a PR on nixpkgs that modifies the coqPackages set, clone this repository, cd into it, and run:

nix-shell --arg do-nothing true --run "updateNixpkgs <pr_owner> <pr_branch>"
nix-shell --arg do-nothing true --run "genNixActions"

Then, open a draft PR with the generated changes here, please include a reference to the nixpkgs PR in the first message of the coq-nix-toolbox PR.

Once the PR on nixpkgs has been merged, you can transform the draft PR into one that updates the version in use in coq-nix-toolbox by running the following commands, adapting the commit message and marking the PR as ready to merge:

nix-shell --arg do-nothing true --run "updateNixpkgsMaster"
nix-shell --arg do-nothing true --run "genNixActions"