[Agda] Packaging Agda and compiling it ahead of time

Alex ter Weele alex.ter.weele at gmail.com
Sun Mar 4 17:45:29 CET 2018


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!


More information about the Agda mailing list