Nix for Coq Development

I first learnt about Nix because of Haskell, eventually running into cabal hell while working on many different projects simultaneously. These used the same dependencies but with different versions, which could not be handled by cabal. The common solution is to use the stack build tool. This manages a database of compatible libraries in called stackage which contains a snapshot of hackage packages that have been tested together. This works very well for packages that are on stackage, however, if one uses dependencies that are only on hackage or, even worse, only available through git, it can become hard to integrate these into stack and use them. In addition to that, if one depends on specific versions of command line tools, these can only be documented and will not be installed or tracked by stack.

The other option is to use Nix, which is a general purpose package manager. The feature that sets it apart from other package managers is that it completely isolates every package using hashes and can therefore seamlessly support multiple versions of the same package. This inherently eliminates the cabal hell problem. In addition to that, if you create a nix derivation (name for a nix package) for the current project one is working on, you can launch a shell containing the exact versions that were specified in the derivation to let it build. This also gives Nix the ability to act as a package manager for reproducible builds, instead of needing to resort to Docker. In addition to that, Nix provides one command, nix-build, which will build the whole project.

For projects using Coq, this is exceptionally useful as one can specify dependencies for Coq, OCaml and the shell using the same nix derivation, and launch a shell which contains all the right versions which will let the project build.

** Nix Basics

First, to understand nix derivations it is important to go over some Nix basics and explain the language itself, as it is quite different to usual package descriptions. The most interesting fact about the language is that it is purely functional, only using immutable data structures.

The most important thing to know when learning a new language is where to look up existing functions and new syntax for that language. This is particularly important for Nix as it does not have that big of a presence on stackoverflow, and it can be hard to google for the Nix language as that is often an abbreviation “*nix” used for linux. I therefore tend to google for the term “nixpkgs” instead of “nix” which seems to give better results. The main resources are the following:

the amazing Nix manual, especially the Nix expression chapter,
Nix pills for a collection of useful tutorials, and finally
the Nix contributors guide for more information about how to package derivations.

Searching for anything on those sites should be much more useful than using Google.

There are three main important structures that need to be understood in Nix. There are

sets ({ a = 2; b = 3; }),
lists ([ 1 2 3 4 ]), and
functions (pattern: body).

These are the structures you will come across most often, however, there are many other useful features Nix has that makes it pleasant to work with.

Just like many other functional languages, Nix has let expressions which bind an expression to a name.

let name = expr; in body

It also supports importing an expression, which just evaluates and inserts an expression.

import ./expression.nix;

The with expression is also interesting, which makes all the attributes of a set available in the next expression, unqualified.

with set; expr

There are many other useful constructs such as recursive sets (allows you to refer to keys from the set inside the set), inheriting (copy the current scope into a set or let expression) or conditionals (if c then e1 else e2). However, this should be enough to learn about derivations.

** Nix Integration with Coq

I’ll go through an example of how I created a nix derivation for a Coq project which extracted to OCaml, going through all the steps that were necessary to make it more general. Each package in nix is actually a derivation. These are functions that take in the whole collection of all the derivations that are available, select the derivations that are needed using the pattern matching that functions inherently do and returns a new derivation. This is just a set containing information on how to build the package by defining multiple different stages in the build pipeline.

The main function we will use is the mkDerivation helper function which is a wrapper around the more manual derivation function. This function takes in a set which can be used to override various build stages and dependencies.

This example will build a Nix derivation for the Vellvm, so that it builds without any errors and contains all the nix packages that are required.

The first derivation one could come up with is the following, which is just a declaration of all the packages that are needed. The with declaration can be used to bring all the members of the <nixpkgs> set into scope. We then call the mkDerivation function to override some of the attributes inside the set, such as the name (name), the location of the source code (src). These are the only two required attributes for the mkDerivation function, however, that does not mean it will build yet.

with import <nixpkgs> {};

stdenv.mkDerivation {
  # Name of the derivation.
  name = "coq${coq.coq-version}-vellvm";

  # Location of the source code which is available on GitHub.
  src = fetchGit {
    url = "https://github.com/vellvm/vellvm";
  };
}

To actually get it to build, there are a few attributes that we need to specify in addition to those. The first is customise the build step using the buildPhase attribute. By default, the build will just execute make, however, in this project the makefile is actually in the src directory. We therefore have to change to that directory first before we can do anything.

{ ...;
  buildPhase = ''
    cd src && make
  ''; }

This will now execute the makefile correctly, however, it will fail the build because Vellvm has a few dependencies that need to be installed first. These are described in the README, so we can just try and find them in Nix and can add them as build dependencies. Here we can specify Coq dependencies using coqPackages, OCaml dependencies using ocamlPackages, and finally command line tools such as the OCaml compiler or the OCaml build system dune.

{ ...; buildInputs = [ git coq ocamlPackages.menhir dune coqPackages.flocq
                       coqPackages.coq-ext-lib coqPackages.paco
                       coqPackages.ceres ocaml ]; }

Finally, Nix will execute make install automatically at the end to install the program correctly. In this case, we need to set the COQLIB flag so that it knows where to place the compiled Coq theories. These can be set using the installFlags attribute.

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

We then have the following Nix derivation which should download Vellvm and build it correctly.

with import <nixpkgs> {};

stdenv.mkDerivation {
  name = "coq${coq.coq-version}-vellvm";

  src = ./.;

  buildInputs = [ git coq ocamlPackages.menhir dune coqPackages.flocq
                  coqPackages.coq-ext-lib coqPackages.paco
                  coqPackages.ceres ocaml ];

  buildPhase = ''
      cd src && make
  '';

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

However, one last problem we’ll have is that coqPackages.ceres does not actually exist in coqPackages, we were a bit too optimistic. To solve this, however, we can easily define a derivation for ceres from the GitHub repo and insert it as a dependency into the set. Luckily ceres has a nice makefile at the base of the repository and does not have any external dependencies, except for Coq itself. We can therefore define a derivation in the following way. We can use propagatedBuildInputs to define dependencies that the package needs and that derivations using this package will also need. In this case, any derivation using ceres will need Coq, otherwise it would not be useful.

let ceres = stdenv.mkDerivation {
  name = "coq${coq.coq-version}-ceres";

  src = fetchGit {
    url = "https://github.com/Lysxia/coq-ceres";
  };

  propagatedBuildInputs = [ coq ];

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

Finally, we can use a let expression to insert it as a dependency into our own derivation. We now have a complete nix expression that will always build Vellvm correctly in a containerised manner.

nix-prefetch-url --unpack https://github.com/Lysxia/coq-ceres/archive/4e682cf97ec0006a9d5b3f98e648e5d69206b614.tar.gz

with import <nixpkgs> {};

let
  ncoq = coq_8_10;
  ncoqPackages = coqPackages_8_10;
  ceres = ncoqPackages.callPackage
    ( { coq, stdenv, fetchFromGithub }:
      stdenv.mkDerivation {
        name = "coq${coq.coq-version}-ceres";

        src = fetchFromGitHub {
          owner = "Lysxia";
          repo = "coq-ceres";
          rev = "4e682cf97ec0006a9d5b3f98e648e5d69206b614";
          sha256 = "0n3bjsh7cb11y3kv467m7xm0iygrygw7flblbcngklh4gy5qi5qk";
        };

        buildInputs = with coq.ocamlPackages; [ ocaml camlp5 ];
        propagatedBuildInputs = [ coq ];
        enableParallelBuilding = true;

        installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
      } ) { } ;
in
stdenv.mkDerivation {
  name = "coq${coq.coq-version}-vellvm";

  src = fetchGit {
    url = "https://github.com/vellvm/vellvm";
  };

  buildInputs = [ git ncoq ocamlPackages.menhir dune ncoqPackages.flocq
                  ncoqPackages.coq-ext-lib ncoqPackages.paco ceres ocaml ];

  buildPhase = ''
      cd src && make
  '';

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

If one saves the file in default.nix, one can then build the nix expression using the nix-build command. This should return a binary that runs the compiled OCaml code, which was extracted from Coq.