Discussion:
Packaging Agda and compiling it ahead of time
(too old to reply)
Alex ter Weele
2018-03-04 16:45:29 UTC
Permalink
Hello all,

I am packaging Agda for Guix. With my package, when I try to load or
compile an Agda file, I see

$ agda test.agda
/gnu/store/17lci61ny0c0fw54304s38bf8lq4nj8q-agda-2.5.3/share/x86_64-linux-ghc-8.0.2/Agda-2.5.3/lib/prim/Agda/Primitive.agdai:
openBinaryFile: permission denied (Read-only file system)

/gnu/store is the immutable store where Guix packages live and is
mounted as read-only to regular users. It looks like the compiler is
trying to write an interface file in its installed location in the
store. Is there a way to generate all agdai files when
compiling/installing Agda itself?

TIA!
James Wood
2018-03-05 10:01:56 UTC
Permalink
Hi Alex,

The same problem comes up for Nix, and the answer is to compile all Agda
files at the time of installation. The postInstall of the Agda package
in
https://github.com/NixOS/nixpkgs/blob/master/pkgs/development/haskell-modules/hackage-packages.nix
is what you want.

Best wishes,

James
Post by Alex ter Weele
Hello all,
I am packaging Agda for Guix. With my package, when I try to load or
compile an Agda file, I see
$ agda test.agda
openBinaryFile: permission denied (Read-only file system)
/gnu/store is the immutable store where Guix packages live and is
mounted as read-only to regular users. It looks like the compiler is
trying to write an interface file in its installed location in the
store. Is there a way to generate all agdai files when
compiling/installing Agda itself?
TIA!
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Loading...