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

[John Leo]

Looking further the culprit seems to be this commit:
https://github.com/agda/agda/commit/85f1696c0963ca1c8a1930a97012b0bbcedd4cf6

Meanwhile the latest versions on both master and experimental show
agda-stdlib violating this constraint:
https://github.com/agda/agda-stdlib/blob/master/src/Data/Empty.agda

I don't know what version of stdlib agda is testing against, but this
stdlib change was made 2 months ago.

As I said I can file a bug if people want me to, but I guess this problem
is already known. I just wanted to mention it in case it wasn't.

John

On Sat, Feb 2, 2019 at 12:50 PM John Leo <leo at halfaya.org> wrote:

> 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/61731e04/attachment.html>