Continuous Integration with Nix

There are two supported methods to set up continuous integration (CI) with Nix.

Using the templates

You can generate a lightweight CI setup to test your Coq project with both released versions and development versions of Coq using the templates.

This method is only supported if either:

• your project is already available in nixpkgs (cf. https://github.com/NixOS/nixpkgs/tree/nixpkgs-unstable/pkgs/development/coq-modules);
• your project has no extra dependencies and builds with the standard method (coq_makefile with a _CoqProject file).

In this case, follow these steps:

1. Create a meta.yml file with the following fields:

• nix: true: required to generate Nix CI configuration.
• One of action: true (GitHub Actions) or travis: true should be provided. Note that, at the moment, the template for GitHub Actions supports uploading to Cachix, but the template for Travis CI doesn't. For coq-community projects, GitHub Actions is recommended and Travis CI is disabled.
• shortname: this field is required and in case the package is available on nixpkgs, it should use the same (attribute) name (casing matters).
• tested_coq_nix_versions: a list of versions to test. If this field is not provided, the master branch of Coq will be tested (only works as is if the project has no extra dependencies). See ref.yml for a precise and complete reference of what to provide in this list.
• cachix: optional list of Cachix caches to use. The default includes coq, coq-community and math-comp. It is also possible to enable pushing to a cache from GitHub Actions if the CACHIX_AUTH_TOKEN secret variable is set. See ref.yml.

2. Clone the templates repository next to your project (git clone https://github.com/coq-community/templates).
3. Generate a CI configuration with the following command ../templates/generate.sh .github/workflows/nix-action.yml.

Examples

These are real world extracts from meta.yml files.

• AAC Tactics (Coq plugin, its master branch is only compatible with Coq's master branch, no extra dependencies):

  shortname: aac-tactics
  nix: true
  action: true

• Huffman (Coq library supporting a range of Coq versions, not packaged in nixpkgs but no extra dependencies):

  shortname: huffman
  nix: true
  action: true
  tested_coq_nix_versions:
  - coq_version: 'master'
  - coq_version: 'v8.14'

• Reglang (Coq library supporting a range of Coq versions, depends on mathcomp-ssreflect):

  shortname: reglang
  nix: true
  action: true
  tested_coq_nix_versions:
  - coq_version: 'master'
    extra_dev_dependencies:
    - nix_name: mathcomp
  - coq_version: 'v8.14'
    extra_dev_dependencies:
    - nix_name: mathcomp
  - coq_version: '8.13'
  ci_cron_schedule: '20 4 * * *'

Pinning the tested development version / using unmerged branches and pull requests

If your project is meant to be tested with the development version of Coq but you do not plan to be especially reactive to update it when it breaks, one big advantage of setting up CI with Nix over other solutions is that you can pin the tested version to the latest commit for which the build is known to pass, and still benefit from the cached binaries!

Here is how to pin CI with commit hash d6a5375460:

tested_coq_nix_versions:
- coq_version: 'coq:d6a5375460'

You can also use an unmerged branch like this:

tested_coq_nix_versions:
- coq_version: 'owner:branch'

Or an unmerged PR like this:

tested_coq_nix_versions:
- coq_version: '#12345'

Installing the Coq Nix Toolbox

To take full benefit of Nix, not just in CI but also to use it locally, it is recommended to install the Coq Nix Toolbox. It contains a command to generate a GitHub Actions workflow that will even test the reverse dependencies of your project (the projects that depend on yours).

Alternative setup and comparison

An alternative method for setting up CI for Coq projects is to use the opam + Docker setup described at: https://github.com/coq-community/docker-coq/wiki/CI-setup

Both setups are equally encouraged and may be used by projects from both inside and outside coq-community. The respective advantages of the two setups are summarized below.

Advantages of Nix CI

• Beyond the ability to perform automated testing against stable releases and the last master version of Coq, Nix allows one to pin the tested development version or to use any unmerged branch or pull request.
• Everything that is uploaded to Cachix is only built once. This means that you can check out locally a PR (with git fetch pull/XX/merge) and quickly fetch the build output instead of rebuilding it by running nix-build. When using the Coq Nix Toolbox, you can also use the cachedMake command.
• The Coq Nix Toolbox supports compatibility testing with reverse dependencies out of the box.

Advantages of Docker-Coq CI

• Docker-Coq provides an opam2 environment with Coq pre-built (and sudo apt-get available);
• Beyond the ability to perform automated testing many Coq releases (⩾ 8.4), the Docker image coqorg/coq:dev is automatically rebuilt after each push in the master branch of Coq (while caching Coq master is not automatic with Nix but on demand, when CI builds external projects that rely on Coq)
• Coq is pre-built using docker-keeper in GitLab CI, to provide each release of Coq with four different OCaml compilers, the default version being 4.13.1+flambda.