Philipp Joram's Place

Type checking Agda Code with Nix

Let us now build our Agda package with Nix by creating a derivation. Create playground.nix in the project root with the following contents, explained below:

# In playground.nix:

# 1.
{ agdaPackages
, lib
, ...
}:
# 2.
agdaPackages.mkDerivation {
  # 3.
  pname = "playground";
  version = "0.1.0";

  # 4.
  src = builtins.path {
    path = lib.sources.cleanSource ./.;
    name = "agda-playground";
  };

  # 5.
  buildInputs = [ agdaPackages.standard-library ];

  # 6.
  everythingFile = "./Everything.agda";

  # 7.
  meta = {
    description = "An Agda playground 🛝";
    longDescription = ''
      A longer description of the package.

      Potentially spanning multiple lines.
    '';
    platforms = lib.platforms.all;
  };
}

The file contains a single Nix expression, namely a function that takes one argument and returns a derivation. This way of writing packages is called the callPackage design pattern, and is used extensively throughout the nixpkgs package index.

The file contains the following:

1. The argument to the function; passed in from our main flake.nix. It is a single attribute set, and expected to contain keys lib and agdaPackages. The former contains some necessary helper functions; the latter is the collection of all Agda packages present in nixpkgs, together with some packaging utilities.

2. The final derivation containing our package, created by agdaPackages.mkDerivation. This function is a wrapper around the nixpkgs's stdenv.mkDerivation. It takes an attribute set describing the package to be built. Some keys of this set are specific to Agda packages, others are passed on to stdenv.mkDerivation.

3. Some general information about the package: its name (pname) and version (version). These have no semantic meaning, they are here for human consumption.

4. The src key tells mkDerivation where to find the source files of our package. In its simplest form this would be src = ./.;, indicating that the source is the current directory (.). We opt to "clean" the source from files related to VCS etc. to avoid rebuilding when unrelated files change. Advanced filtering can be done via other nixpkgs filtering functions, or even by respecting your .gitignore.

5. buildInputs contains a list of dependencies necessary to build our library. For now, we will depend on the Agda standard library, packaged in nixpkgs at agdaPackages.standard-library. Later we will see how to use libraries that require special Agda options (such as Cubical Agda), and how to use custom revisions of libraries.

6. The everythingFile contains the path to an Agda module that transitively imports all other modules that are meant to be part of our library, the module index. mkDerivation will run agda on this file, type checking all library modules in the process. Many Agda libraries take this approach, as Agda defines no manifest format for this purpose.

   See below for a detailed explanation.

7. Some metadata. This is optional, but having a description is nice. Since our package is platform independent (or at least as independent as agda is), it is common courtesy to set meta.platforms = lib.platforms.all.

Everything.agda: The module index

As mentioned before, agdaPackages.mkDerivation requires a single Agda module importing all other modules that are meant to be part of a library. We call this file the module index.

So far our "library" consists of a single module, Playground/Hello.agda. Let's first add another module that uses the Agda standard library, and then reference both of them in the module index.

Create a new module that uses the type of natural numbers from the standard library:

-- In Playground/WithStdlib.agda:

module Playground.WithStdlib where

-- Imported from standard-library:
open import Data.Nat.Base using (ℕ)

answer : ℕ
answer = 42

Now, create module index at Everything.agda and import the modules:

-- In Everything.agda:

import Playground.Hello
import Playground.WithStdlib

Building the derivation

Finally, we can build the derivation for the first time. By default, nix will not print any output unless it encounters an error. We pass --print-build-logs (short: -L) to instruct it to please 🥺 tell us what it is doing:

$ nix build --print-build-logs
[...]
playground> building
playground> Checking Everything (/build/agda-playground/Everything.agda).
playground>  Checking Playground.Hello (/build/agda-playground/Playground/Hello.agda).
playground>  Checking Playground.WithStdlib (/build/agda-playground/Playground/WithStdlib.agda).
playground> installing
[...]

If we did everything correctly, a symbolic link called result should appear in our working directory. It points to the finished derivation, in the Nix store...

$ readlink result
/nix/store/[...]-playground-0.1.0

...and contains our library modules, including their corresponding interface files created by the type checking process:

$ nix-shell -p exa --run 'exa -T result/*'
result/Playground
├── Hello.agda
├── Hello.agdai
├── WithStdlib.agda
└── WithStdlib.agdai
result/playground.agda-lib

Now, whenever we make a change to the Agda code, we'll have to re-run nix build to type check it. This is cumbersome, and definitely not interactive theorem proving. In the next section we will learn how to create a shell with all of our library's dependency available, so that we can use agda interactively as usual.