[Agda] Working with Agda inside nix-shell

[Mateusz Kowalczyk]

Hi,

I recently added an Agda builder to nixpkgs, the main repository for the
nix package manager and it works quite well.

nix has a feature called ‘nix-shell’ which lets you drop into the
project with all the dependencies available to you. As a result, I would
like to change what emacs calls out to when I press C-c C-l.

Here I have two problems.

I thought it would be as simple as

(setq agda2-program-name "nix-shell --pure --command agda") but it
wasn't, there is a separate args variable. But even if I eval:

(setq agda2-program-name "nix-shell")
(setq agda2-program-args '("--pure" "--command" "agda"))

It fails (details in a sec). I noticed in in agda-mode source that
‘--interaction’ is always cons'd in front of the argument list which
would make ‘nix-shell --interaction --pure --command agda’ but even if I
remove the cons and manually ensure it is passed in the right place, it
fails.

So at this point I'm stuck, unable to convince emacs to see the agda
inside my shell. It always fails with the following in *agda2* buffer:

Process Agda2 exited abnormally with code 1
IOTCM "/home/shana/programming/bitvector/Data/BitVector.agda"
NonInteractive Indirect ( Cmd_load
"/home/shana/programming/bitvector/Data/BitVector.agda" ["."] )

Of course I'm loading Data.BitVector here.

For reference, I do a similar thing with GHCi:

(setq haskell-program-name "nix-shell --pure --command ghci") works
without a hitch, as does ‘cabal repl’.

I also have a second problem. Assume that I managed to convince emacs to
pass everything properly and it's happy. It seems that there is
something unexpected (to me) going on with include paths. Inside my
nix-shell, I have a thing called ‘configurePhase' which produces a
wrapped ‘agda’ binary which ‘-i’s my dependencies. So when I run the
full command (manually), I get something like this:

[shana at lenalee:~/programming/bitvector]$ nix-shell --pure --command
'eval "$configurePhase" && cat $(which agda) && agda --interaction'

/nix/store/3nr2shnd73jx84hhijgicnvahgj68z0i-haskell-Agda-ghc7.8.3-2.4.2-shared/bin/agda
-i /nix/store/x9gl9ik7b7z94djj0zvmvf00nymzh6ad-Agda-stdlib/share/agda -i
/nix/store/d6j1rjlrmhya72w31g4b9xybjvaq6s7j-bitvector -i src -i . "$@"

Agda2>

As you can see, my wrapper includes the standard library. But if I then
put the following into the prompt, it complains that it can't find the
standard lib:

IOTCM "/home/shana/programming/bitvector/Data/BitVector.agda"
NonInteractive Indirect ( Cmd_load
"/home/shana/programming/bitvector/Data/BitVector.agda" ["."] )

It would seem like --interaction either ignores preceding ‘-i’s or
something else is happening. I can confirm that my wrapper works because
when I run it on Everything.agda or any of the files in the project, it
sees the stdlib just fine.

It'd be great if someone could shed some light on both issues.


-- 
Mateusz K.