An Environment for Interactive Development

So far, we have only run Agda through the various nix sub-commands. Agda however excels when being used interactively from within an editor. Our goal is to make the flake-based setup compatible with interactive editing.

Agda on demand with nix develop

Recall that earlier, we declared a shell environment in flake.nix:

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

This allows us to enter a shell that exposes all inputs to the derivations listed in inputsFrom. In particular, those of defaultPackage — the Agda library we declared in playground.nix. One of its inputs is agda itself, and we can make it available in a new shell by invoking nix develop:1

$ nix develop --bash-prompt "agda-env> "
agda-env> which agda # Agda as pinned by flake.lock
/nix/store/48wvmiiiw3cr6sjh38vp695h81kyzysj-agdaWithPackages-2.6.2.2/bin/agda

Inside this shell, we can access a version of Agda that knows of our standard-library dependency, and type-checking our library succeeds:

agda-env> agda Everything.agda
Checking Everything (/[...]/agda-playground/Everything.agda).
 Checking Playground.Hello (/[...]/agda-playground/Playground/Hello.agda).
 Checking Playground.WithStdlib (/[...]/agda-playground/Playground/WithStdlib.agda).

Details: How Agda finds dependencies

When using agdaPackages.mkDerivation to build our package, the real agda binary is wrapped with extra arguments. These arguments tell agda where to search for modules provided by other libraries:

agda-env> cat $(which agda)
#! /nix/store/dsd5gz46hdbdk2rfdimqddhq6m8m8fqs-bash-5.1-p16/bin/bash -e
exec "/nix/store/8i6s0m32mgcvd4vlakw752n40d6gkgsd-Agda-2.6.2.2/bin/agda" \
    --with-compiler=/nix/store/q468289jr01p5p2lllfs1s99wggbw00g-ghc-9.0.2-with-packages/bin/ghc \
    --library-file=/nix/store/2r00jip3577bzvmw79pb0rwqq3czhmq9-libraries \
    --local-interfaces "$@"

The flag --library-file=<...> receives as an argument a file containing paths to all libraries in which search for modules:

agda-env> cat /nix/store/2r00jip3577bzvmw79pb0rwqq3czhmq9-libraries
/nix/store/bj9k8disw7pjmwbybniqmafzgrfbk6zg-standard-library-1.7.1/standard-library.agda-lib

This environment also contains agda-mode, the program that powers interactive editing in many editors. If you've set up Emacs following the official instructions, emacs run from inside this shell should pick up our custom Agda environment:

agda-env> emacs Playground.WithStdlib # Loading the buffer (C-c C-l) should work.

I personally use Neovim together with Cornelis to work on Agda projects, and that works like a charm from inside this shell!

Automatically loading the environment

It is somewhat cumbersome to load this environment every time we want to hack on some code. Not only does it take time to instantiate the shell, the shell itself is also rather bare-bones. This is rather upsetting for anyone who has put time into customizing their interactive shell!

We are going to automate the process of loading the environment by using direnv, together with its Nix integration provided by nix-direnv. direnv works by hooking your shell and running some code whenever you change into a directory containing a file called .envrc. It is there that we put the instructions to load the Agda environment.

Go and follow the official installation instructions to install both direnv and nix-direnv. I use home-manager to manage my user programs, so this is as easy as enabling direnv and nix-direnv. We can then go ahead and write our hook to load the Agda environment, and put it on direnv's list of allowed environments:2

$ echo "use flake" > .envrc # Write flake hook to .envrc
$ direnv allow # Allow loading *this* .envrc
direnv: loading /[...]/agda-playground/.envrc
direnv: using flake
direnv: nix-direnv: renewed cache
$

Details: direnv caching

In the above output, nix-direnv tells us that it has renewed its cache: Flake environments are cached per directory and therefore load almost instantaneously when changing directory!

Notice how were not thrown into a subshell, as opposed to when using nix develop. We are still in the same interactive shell as before, but direnv has set up the environment (e.g. by modifying the $PATH) to give us access to the shell environment defined in our flake. We should now have access to Agda in our shell!

$ which agda
/nix/store/48wvmiiiw3cr6sjh38vp695h81kyzysj-agdaWithPackages-2.6.2.2/bin/agda

Since I am using Neovim from the shell directly, it picks up the custom environment. This might not be the case if you are launching your editor from elsewhere, perhaps a desktop shortcut or an application launcher. In this case you might want to consider a plug-in for your editor that provides direnv integration, such as:

Conclusion

You should now have a reproducible, per-project Agda environment that is loaded automatically whenever you hack on files in a project!

1

Passing --bash-prompt is optional. We do it here to distinguish between the different shells.

2

direnv will not blindly execute an .envrc it finds in the current directory. You have to explicitly allow the automatic execution of these files. By issuing direnv allow, the .envrc in the current directory is put onto direnv's allow-list. This can be reverted by issuing direnv revoke.