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

[Guillaume Allais]

My bad. The CI worked, including the stdlib-based tests (?!) so I assumed
everything was OK. I'll look into updating the experimental branch of the
stdlib.

We're discussing the situation on this re-opened issue:
https://github.com/agda/agda-stdlib/issues/547

Looks like I'll need to add some explicit uses of `--sized-types` too now
that Agda thoroughly checks the OPTIONS a module's dependencies are using.

Cheers,


On 02/02/2019 22:04, John Leo wrote:
> 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
>>>
>>
> 
> 
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <https://lists.chalmers.se/mailman/private/agda-dev/attachments/20190203/7d5db072/attachment.sig>