[Agda-dev] COMPILE pragma not allowed in safe mode.

[Nils Anders Danielsson]

On 01/02/2019 18.07, John Leo wrote:
> I just pulled the latest agda and agda-stdlib and while agda builds
> fine I get a bunch of errors in the stdlib code (for example in
> Data/Empty.agda): COMPILE pragma not allowed in safe mode.
> 
> I don't know if this is a new check that was added and the stdlib has
> just not been updated yet but I thought I'd point it out. If you like
> I can file a bug. I've just commented out the offending COMPILE
> statements in my own code for now.

One part of the Agda test suite is to type-check the standard library.
At the moment this test seems to pass for a standard library commit with
hash 6ed677928b0d7c54521b1d0c7cef7e3181f293a8.

I think the idea is that the experimental branch of the standard library
should be compatible with bleeding edge Agda, but I am not aware of any
automated tests that warn if this property does not hold.

-- 
/NAD