Nix shell for Agda development with the Agda standard library

shell.nix

let

  pkgs = import (builtins.fetchTarball {
    url =
      "https://github.com/NixOS/nixpkgs-channels/archive/b0bbacb52134a7e731e549f4c0a7a2a39ca6b481.tar.gz";
    sha256 = "15ix4spjpdm6wni28camzjsmhz0gzk3cxhpsk035952plwdxhb67";
  }) { };

  # The standard library in nixpkgs does not come with a *.agda-lib file, so we
  # generate it here.
  standard-library-agda-lib = pkgs.writeText "standard-library.agda-lib" ''
    name: standard-library
    include: ${pkgs.AgdaStdlib}/share/agda
  '';

  # Agda uses the AGDA_DIR environmental variable to determine where to load
  # default libraries from. This should have a few files in it, including the
  # "defaults" and "libraries" files generated below.
  #
  # More information (and possibilities!) are detailed here:
  # https://agda.readthedocs.io/en/v2.6.0.1/tools/package-system.html
  agdaDir = pkgs.stdenv.mkDerivation {
    name = "agdaDir";

    phases = [ "installPhase" ];

    # If you want to add more libraries simply list more in the $out/libraries
    # and $out/defaults folder.
    installPhase = ''
      mkdir $out

      echo "${standard-library-agda-lib}" >> $out/libraries
      echo "standard-library" >> $out/defaults
    '';
  };

in pkgs.mkShell {
  name = "agda-shell-with-stdlib";
  builtInputs = [ pkgs.haskellPackages.Agda pkgs.emacs ];

  # The build environment's $AGDA_DIR is set through this call.
  AGDA_DIR = agdaDir;
}

This nix expression installs the Agda toolchain, the Agda standard library, and emacs.

To start using Agda (on macOS/Linux):

1. Download and install Nix (https://nixos.org/nix/)
2. Place this shell.nix in the directory you will be working on Agda code with.
3. Open a terminal and run nix-shell in the directory where you placed this shell.nix.
4. Run emacs from the bash terminal that appears: emacs or emacs SomeFileYouWantToOpen.agda

Happy proving!