-
Notifications
You must be signed in to change notification settings - Fork 6
Continuous Integration with Nix
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:5QW/wwEnD+l2jvN6QRbRRsa4hBHG3QiQQ26cxu1F5tI="
env:
- COQ=https://github.com/coq/coq-on-cachix/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.
See also Nix on the Coq wiki.
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:5QW/wwEnD+l2jvN6QRbRRsa4hBHG3QiQQ26cxu1F5tI="
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}/";
}
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-on-cachix/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:5QW/wwEnD+l2jvN6QRbRRsa4hBHG3QiQQ26cxu1F5tI="
- 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.
- To learn more about the uses the
default.nix
file, you may read Developing and debugging with Nix.
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.
- 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.
-
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)