Continuous Integration with Nix

Generic setup

Creating a .travis.yml file with the following content:

language: nix

script:
- nix-build --argstr coq-version-or-url "$COQ" --extra-substituters https://coq.cachix.org --trusted-public-keys "cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= coq.cachix.org-1:Jgt0DwGAUo+wpxCM52k2V+E0hLoOzFPzvg94F65agtI="

env:
- COQ=https://github.com/coq/coq/tarball/master
- COQ=8.9
- COQ=8.8

and a default.nix file with the following content:

{ pkgs ? (import <nixpkgs> {}), coq-version-or-url, shell ? false }:

let
  coq-version-parts = builtins.match "([0-9]+).([0-9]+)" coq-version-or-url;
  coqPackages =
    if coq-version-parts == null then
      pkgs.mkCoqPackages (import (fetchTarball coq-version-or-url) {})
    else
      pkgs."coqPackages_${builtins.concatStringsSep "_" coq-version-parts}";
in

with coqPackages;

pkgs.stdenv.mkDerivation {

  name = "my-project-name";

  propagatedBuildInputs = [
    coq
    # list other dependencies, for instance:
    ssreflect
  ];

  src = if shell then null else ./.;

  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
}

allows to setup Continuous Integration on Travis using Nix.

This is the essential part of the setup that is proposed in templates/ for coq-community projects. Note that the actual .travis.yml is actually more complex because it also contains logic to test the opam file.

Simpler setup when not testing Coq's development branch

The very long line nix-build --argstr coq-version-or-url "$COQ" --extra-substituters https://coq.cachix.org --trusted-public-keys "cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= coq.cachix.org-1:Jgt0DwGAUo+wpxCM52k2V+E0hLoOzFPzvg94F65agtI=" includes logic for fetching binaries for the development version of Coq from https://coq.cachix.org. Without it, the line would just be nix-build --argstr coq-version-or-url "$COQ" but the development version of Coq would be built every time CI is run. If you don't need to test the development version, the logic can thus be reduced to the following:

language: nix

script:
- nix-build --argstr coq-version-or-url "$COQ"

env:
- COQ=8.9
- COQ=8.8

And if your project depends on a very specific version of Coq, you may even hard-code it, which would give a trivial .travis.yml file:

language: nix

and a reduced default.nix:

{ pkgs ? (import <nixpkgs> {}), shell ? false }:

with pkgs.coqPackages_8_9;

pkgs.stdenv.mkDerivation {

  name = "my-project-name";

  propagatedBuildInputs = [
    coq
    # list other dependencies, for instance:
    ssreflect
  ];

  src = if shell then null else ./.;

  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
}

Pinning the tested development version

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!

To do so, simply replace the line

- COQ=https://github.com/coq/coq/tarball/master

with

- COQ=https://github.com/coq/coq/tarball/d6a5375460

You may also add a default value to the coq-version-or-url argument from default.nix as such:

{ pkgs ? (import <nixpkgs> {}), coq-version-or-url ? "https://github.com/coq/coq/tarball/d6a5375460", shell ? false }:

in which case (and assuming you're only testing this version), you could simplify the .travis.yml configuration file to:

language: nix

script:
- nix-build --extra-substituters https://coq.cachix.org --trusted-public-keys "cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= coq.cachix.org-1:Jgt0DwGAUo+wpxCM52k2V+E0hLoOzFPzvg94F65agtI="

Learning more

• To learn more about Nix, you may read the Nix and the nixpkgs manuals.
• To learn more about Travis + Nix, you may read the Travis docs and the Travis page from the Nix wiki.

Alternative setup and comparison

An alternative method for setting up Continuous Integration 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

• The development version of Coq available for Nix CI is updated more frequently (several times per day) than Docker-Coq's nightly build;
• Beyond the ability to perform automated testing against stable releases and the latest master version of Coq, Nix allows one to pin the tested development version.

Advantages of Docker-Coq CI

• Docker-Coq provides an opam2 environment with Coq pre-built (and sudo apt-get available);
• Coq is pre-built using two different compilers, currently both 4.05.0 and 4.07.0+flambda (which could be useful especially for plugin developers or benchmarks, or possibly for other applications) while the Nix setup provides only one Coq pre-built with OCaml 4.06.1;
• Docker-Coq may be more easy to setup for projects built on GitLab CI, given its native Docker support, while Travis CI is more "Docker-agnostic" (in particular, the configuration file template docker-coq-gitlab-ci-demo-1/.gitlab-ci.yml appears to be less cumbersome than its Travis CI counterpart docker-coq-travis-ci-demo-1/.travis-ci.yml)