[Agda] Packaging Agda and compiling it ahead of time

[James Wood]

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


On 04/03/18 16:45, Alex ter Weele wrote:
> 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!
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda