[Agda] Working with Agda inside nix-shell

[Mateusz Kowalczyk]

On 09/04/2014 10:03 PM, Andreas Abel wrote:
> 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)...

When I checked it couldn't, it just complains about command not found.

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

OK, that's disappointing. Any chance Agda could be taught to not ignore
-i if ran with interaction? Maybe implicitly add them to the path list.
A temporary hack would be for me to override include paths in emacs
before C-c C-l by peeking into nix-shell but that's pretty ugly
considering it's effectively a global variable.

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