Configuring Agda's standard library on NixOS

17 May, 2019 ⋅ programming

I’ve been using Agda on NixOS for a while (mostly via agda-mode in Emacs), but I remember it was a bit difficult to get going the very first time. Hopefully this becomes a searchable reference to getting it all set up quickly.

Prerequisites:

Working NixOS installation
Agda >=2.5.1

Install AgdaStdlib globally

# /etc/nixos/configuration.nix

...

environment.systemPackages = with pkgs; [

  ...

  AgdaStdLib

];

...

Link /share/agda

# /etc/nixos/configuration.nix

...

environment.pathsToLink = [ "/share/agda" ];

...

Rebuild: sudo nixos-rebuild switch
Navigate to or create ~/.agda

Create 3 files in ~/.agda: defaults, libraries, standard-library.agda-lib

[isaac:~/.agda]$ touch defaults
[isaac:~/.agda]$ touch libraries
[isaac:~/.agda]$ touch standard-library.agda-lib

Edit standard-library.agda-lib

[isaac:~/.agda]$ cat << EOF >> standard-library.agda-library
> name: standard-library
> include: /run/current-system/sw/share/agda/
> EOF

This says that there is a library located at the relevant NixOS path.

Edit libraries

[isaac:~/.agda]$ echo "/home/isaac/.agda/standard-library.agda-lib" >> libraries

This registers the .agda-lib file with Agda.

Edit defaults
```
[isaac:~/.agda]$ echo "standard-library" >> defaults
```
This tells Agda to include the standard-library library by default.

To check your installation, try compiling a simple Agda file:

[isaac:~]$ cat << EOF >> Test.agda
> module Test where
> open import Data.Nat
> EOF
[isaac:~]$ agda Test.agda
Checking Test (/home/isaac/Test.agda).

Let me know whether or not this works for you :)