[Agda] Working with Agda inside nix-shell

[Andreas Abel]

I do not really have an idea how to fix your problem due to limited 
emacs-lisp skills, but see comments below.

On 04.09.2014 21:53, Mateusz Kowalczyk wrote:
> 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:

This *should* indeed work, if nix-shell is able to pass all following 
arguments to agda instead of interpreting them for itself.

However, I do not know if agda2-program-name indeed can be arbitrary 
(string with spaces)...

> (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" ["."] )

The stuff in [...] is the include pathes.

> 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" ["."] )

Here you only have the current directory as include path, so it does not 
find the standard library.  Note that it is irrelevant what -i options 
you gave to Agda, the interactive command wants the whole path be given 
directly.

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


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/