[Agda] Packaging Agda and compiling it ahead of time

James Wood james.wood.100 at strath.ac.uk
Mon Mar 5 11:01:56 CET 2018

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
is what you want.

Best wishes,


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

More information about the Agda mailing list