Setting up a Project Skeleton

In a first iteration, we will set up a basic project that contains some Agda code, and add a Flake that...

  1. Describes how to install Agda and the Agda standard library.
  2. Has instructions for type-checking our code.

We'll call our project Playground. First, create a new directory that will contain the project, and enter it:

$ mkdir agda-playground
$ cd agda-playground

In the following, we call this directory the (project) root directory. If not stated otherwise, files are created and edited in the project root directory.

Next, we create the module structure for our project:

$ mkdir Playground
$ touch Playground/Hello.agda

Open the Agda module Playground/Hello.agda in your preferred editor, and enter the following code:

-- In Playground/Hello.Agda:
module Playground.Hello where

open import Agda.Builtin.String using (String)

hello : String
hello = "Hello, world"

You can re-use the shell from before and check whether Agda accepts the file:

$ nix-shell --packages 'agda' --run "agda --no-libraries Playground/Hello.agda"
Checking Playground.Hello (/tmp/agda-playground/Playground/Hello.agda).

We pass --no-libraries to temporarily ensure that Agda treats Hello.agda as a stand-alone module, without any library dependencies. In order to later specify dependencies we set up a proper Agda library, defined in a library file. Create playground.agda-lib and enter the following:

-- In playground.agda-lib:

-- The name of our library:
name: playground

-- Search for modules in directory of this file
-- (i.e. the project root)
include: .

-- This library has a dependency on the Agda standard library:
depend: standard-library

-- No compiler flags (yet):
flags:

Now, create and open the file flake.nix, and insert the following code (explanation follows below):

# In flake.nix:
{
  # 1.
  description = "An Agda Library set up with Nix Flakes";

  # 2.
  inputs = {
    nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";
    flake-utils.url = "github:numtide/flake-utils";
  };

  # 3.
  outputs = {
    self,
    nixpkgs,
    flake-utils,
    ...
  }: let
    # 4.
    inherit (flake-utils.lib) simpleFlake defaultSystems;

    # 5.
    name = "playground";

    # 6.
    overlay = final: prev: {
      ${name} = {
        # 7.
        defaultPackage = final.callPackage ./playground.nix {};
      };
    };
  in
    # 8.
    simpleFlake {
      inherit self nixpkgs name overlay;
      systems = defaultSystems;

      # 9.
      shell = {pkgs}:
        pkgs.mkShell {
          inputsFrom = [pkgs.${name}.defaultPackage];
        };
    };
}

Every flake.nix consists of three attributes: a description, some inputs and some outputs. Let's go over them in detail:

  1. description is a short human-readable string (duh).

  2. inputs to the Flake are Nix expressions that are fetched from elsewhere. In our case, we fetch two inputs:

    • The nixpkgs package index from GitHub, checking out the branch nixpkgs-unstable.
    • flake-utils, a self-contained library to help us write less boilerplate code.

  3. outputs is a function from the inputs (as downloaded and stored in your system) to any number of build artifacts. We take nixpkgs and flake-utils as inputs (ignore self for now), and produce a package that contains our type-checked library and some other goodies.

  4. We use a let ... in ...-expression to give names to values that we'll use later. First, we bring simpleFlake and defaultSystems into scope, ...

  5. ...assign a name for later use...

  6. ...and then create an Overlay that contains one attribute ${name} (i.e. "playground"). Overlays are nixpkgs's way of extending the package index with new packages or patching existing ones.

  7. We assign an attribute set to the key ${name} which contains one package built from a Nix expression in the file ./playground.nix. This file contains the actual definition of our package, and we'll go over it later.

  8. To return the package in a format that nix expects, we use the library function simpleFlake that puts our package together: We specify which snapshot of nixpkgs to use, what the name of our package is, which overlay to use (this contains our package), and which systems the package can be built for. In turn, simpleFlake returns an output in the correct format.

  9. We set up a custom interactive shell that has access to all build dependencies of our package. We will discuss how to use it in a later chapter.

Now, we can run nix build and attempt the first build of our project. Of course that will fail, but we can learn some things from the error message:

$ nix build
warning: creating lock file '/[...]/agda-playground/flake.lock'
error: getting status of '/nix/store/[...]-source/agda-playground/playground.nix': No such file or directory
(use '--show-trace' to show detailed location information)
  1. nix created the flake.lock containing snapshots of the inputs for us. It's a JSON file, so we can inspect it using jq: 
    $ nix-shell -p 'jq' --run "jq '.nodes.nixpkgs.locked.rev' < flake.lock"
"813836d64fa57285d108f0dbf2356457ccd304e3"
  2. nix cannot find playground.nix. This is where our package description goes.

Next, let us put together a Nix package for our Agda project in playground.nix.