Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Nix shell for Agda development with the Agda standard library
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;
}
@ryanorendorff

This comment has been minimized.

Copy link
Owner Author

@ryanorendorff ryanorendorff commented Dec 31, 2019

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!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment