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

[John Leo]

Hi Nils,

Thanks for the info. However I don't see that commit on github either in
the master or experimental branch. Perhaps I'm missing something. Could you
send me a web link if you have it?

Also I've been pulling latest agda-stdlib from the master branch to go with
agda from the master branch. Are you saying I should be using experimental
stdlib with master agda?

John

On Sat, Feb 2, 2019 at 12:16 PM Nils Anders Danielsson <nad at cse.gu.se>
wrote:

> 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
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.chalmers.se/mailman/private/agda-dev/attachments/20190202/93aa0ce1/attachment.html>