I E

Configuring Agda's standard library on NixOS

17 May 2019

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:

  1. Install AgdaStdlib globally

    # /etc/nixos/configuration.nix
    
    ...
       
    environment.systemPackages = with pkgs; [
       
      ...
       
      AgdaStdLib
        
    ];
       
    ...
    
  2. Link /share/agda

    # /etc/nixos/configuration.nix
       
    ...
       
    environment.pathsToLink = [ "/share/agda" ];
       
    ...
    
  3. Rebuild: sudo nixos-rebuild switch

  4. Navigate to or create ~/.agda

  5. 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
    
  6. 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.

  7. Edit libraries

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

    This registers the .agda-lib file with Agda.

  8. 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 :)