Agda fails to compile files without --local-interfaces in nixos

[alexarice]

I'm not sure if this is a nixos problem or an agda problem but currently if you try to compile an empty file with agda 2.6.1 which is not in a library, agda tries to build the interface file in /nix/store/_build which is read only. The problem seems to go away with --local-interfaces

Would be good if anyone has any ideas as to what is causing this.

[turion]

Example setup to reproduce:

$ cd /tmp
$ cat mylib/mylib.agda-lib 
name: mylib
include: src

$ cat mylib/src/TestModule.agda 
module TestModule where
import IO

$ cat TestUserLibrary.agda 
import TestModule

$ agda -l standard-library -l mylib -i . TestUserLibrary.agda -v 10000
Importing the primitive modules.
Library dir = "/nix/store/7hbp89vwrih5hhdja12warhh5s8svn4n-Agda-2.6.1-data/share/ghc-8.8.3/x86_64-linux-ghc-8.8.3/Agda-2.6.1/lib"
SetRange is setting the current range to /nix/store/7hbp89vwrih5hhdja12warhh5s8svn4n-Agda-2.6.1-data/share/ghc-8.8.3/x86_64-linux-ghc-8.8.3/Agda-2.6.1/lib/prim/Agda/Primitive.agda:5,8-22 which is outside of the current file Nothing
/nix/store/_build: createDirectory: permission denied (Read-only
file system)

[alexarice]

For me I can reproduce just by:

cd $(mktemp -d)
touch test.agda
agda test.agda

[gallais]

This is very strange. _build directories should only be created at the root
of an Agda project. Surely you don't have an .agda-lib file in /nix/store/?

(Note that there is another, unrelated, issue with nix that should get fixed in
a minor release: #4526)

[alexarice]

I think there probably is a .agda-lib file in my nix store but It was my understanding that it shouldn't matter because as it's in a different directory to my temp directory?

[gallais]

With the (new) project-based interface stashes, we do not dump the .agdai files
next to the corresponding source file anymore if we can find a project root
(i.e. an .agda-lib file somewhere up in the hierarchy).
This allows us to avoid retypechecking a project from scratch every time a user
switches between versions of Agda.

Here the presence of an .agda-lib file in /nix/store leads Agda to believe
that the root project for the primitives is /nix/store and so it tries to
regenerate the agdai files for the builtins there (well, in _build/2.6.1
to be exact).

I think this demonstrates we do need to ship an .agda-lib for the builtins
and get them compiled into the appropriate _build/VERSION at installation
time.

[alexarice]

Ah I forgot about the primitives, that makes perfect sense

[turion]

So we could patch this quickly by distributing our own .agda-lib for builtins in Nixos I guess?

[alexarice]

That might be the best solution

[gallais]

If you do so, you need to make sure that the .agdai files for the builtins
end up in the corresponding _build/2.6.1 directory. At the moment Setup.hs
compiles the builtins using --local-interfaces so they are dumped next to the
source file (the assumption was that there would never be an .agda-lib file
for Agda to find but that was a really bad assumption to make in retrospect.
Sorry about that! 😭).

So you could:

• add an .agda-lib file for the builtins
• remove --local-interfaces from Setup.hs

and hopefully that should do it? 🤞

[alexarice]

Should the .agda-lib file just go in the same folder as the builtins?

[gallais]

I would put a file agda-builtins.agda-lib in lib/prim/:

name: agda-builtins
include: .

[laMudri]

I think there probably is a .agda-lib file in my nix store

Wait, surely not? I thought everything directly in /nix/store/ was a directory or a .drv.

[alexarice]

I think there probably is a .agda-lib file in my nix store

Wait, surely not? I thought everything directly in /nix/store/ was a directory or a .drv.

Ah, this only started when we started trying to write tests, this is why it took so long to notice

[alexarice]

$ ls | grep ".agda-lib"
blxg8dm9ipq86028q9qp8qij2j4rr8rn-mylib.agda-lib
bqp854jr20z2y9x9v0391hm6cjswyska-mylib.agda-lib.drv
hlyi5ims19lca5rmzhhgxwkfjrmaaklq-mylib.agda-lib.drv
qcfx5glrzps4mf67clrknsw551f7bms7-mylib.agda-lib

[laMudri]

Aah, are blxg8dm9ipq86028q9qp8qij2j4rr8rn-mylib.agda-lib and qcfx5glrzps4mf67clrknsw551f7bms7-mylib.agda-lib actually directories whose names happen to end with .agda-lib?

[alexarice]

no they are files, A derivation can be a single file

[laMudri]

Oh okay, I suppose this should be a won't-fix from the Agda side, then.

[gallais]

Oh okay, I suppose this should be a won't-fix from the Agda side, then.

I think our fix should be to add an .agda-lib file to the lib/prim.

[alexarice]

As a side note, Agda also seems to recognise directories as agda-lib files for the purposes of determining what a library is

[guilhermehas]

In my machine, it compiles, but it takes a very long time.

[turion]

In my machine, it compiles, but it takes a very long time.

What system do you have?

[guilhermehas]

What system do you have?

Nixos too.

[alexarice]

The problem only occurs if you end up with an .agda-lib file in your nix store. This only happened to us when we tried to make some nixos tests

[gallais]

@guilhermehas is probably suffering from #4526

[andreasabel]

@gallais : Is this fixed by this PR?

• Provide a .agda-lib for Agda builtins #6988

[gallais]

I don't know, I'm not a nix user. :D

[andreasabel]

Ok, I'll remove it from the milestone again. I also removed your assignment.
We would need new input from users whether this is still a problem.

[alexarice]

I'll check this now, though need to built the release candidate

[alexarice]

As far as I can tell, everything is working with release candidate 2, with or without the --local-interfaces flag