Hello, On Sun, Jun 05, 2016 at 02:38:01PM +0200, Joachim Breitner wrote: > since Agda does not live with the other packages, I forgot about it. > Does anyone feel like upgrading it to 2.5.1? I got agda 2.5.1 to build but I haven't been able to test it (esp. the new dh_elpa package) because I can't figure out upgrading agda-stdlib. When building the new agda-stdlib, this happens: ,---- | ./GenerateEverything | agda +RTS -K1G -RTS -i /home/swhitton/src/agda-stdlib -i /home/swhitton/src/agda-stdlib/src /home/swhitton/src/agda-stdlib/Everything.agda | Checking Everything (/home/swhitton/src/agda-stdlib/Everything.agda). | Checking Algebra (/home/swhitton/src/agda-stdlib/src/Algebra.agda). | Checking Relation.Binary (/home/swhitton/src/agda-stdlib/src/Relation/Binary.agda). | Checking Data.Product (/home/swhitton/src/agda-stdlib/src/Data/Product.agda). | Checking Function (/home/swhitton/src/agda-stdlib/src/Function.agda). | Checking Level (/home/swhitton/src/agda-stdlib/src/Level.agda). | Finished Level. | Finished Function. | Checking Relation.Nullary (/home/swhitton/src/agda-stdlib/src/Relation/Nullary.agda). | Checking Data.Empty (/home/swhitton/src/agda-stdlib/src/Data/Empty.agda). | Finished Data.Empty. | Finished Relation.Nullary. | Finished Data.Product. | Checking Data.Sum (/home/swhitton/src/agda-stdlib/src/Data/Sum.agda). | Checking Data.Maybe.Base (/home/swhitton/src/agda-stdlib/src/Data/Maybe/Base.agda). | Checking Data.Bool.Base (/home/swhitton/src/agda-stdlib/src/Data/Bool/Base.agda). | Checking Data.Unit.Base (/home/swhitton/src/agda-stdlib/src/Data/Unit/Base.agda). | Checking Agda.Builtin.Unit (/usr/share/libghc-agda-dev/lib/prim/Agda/Builtin/Unit.agda). | Failed to write interface /usr/share/libghc-agda-dev/lib/prim/Agda/Builtin/Unit.agdai. | /home/swhitton/src/agda-stdlib/src/Data/Unit/Base.agda:13,13-30 | /usr/share/libghc-agda-dev/lib/prim/Agda/Builtin/Unit.agdai: | openBinaryFile: permission denied (Permission denied) | debian/rules:10: recipe for target 'override_dh_auto_build' failed `---- Does anyone happen to know why agda wants to write to /usr, and how I can stop it? My work is at https://git.spwhitton.name/agda-stdlib if anyone wants to hack on it themselves. -- Sean Whitton
Attachment:
signature.asc
Description: PGP signature