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

[Guillaume Allais]

I have pushed a fix to the experimental branch. It works on my machine with
agda 2.6.0-f220dda (aka the current HEAD).

On 03/02/2019 01:00, Guillaume Allais wrote:
> 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
>>
> 
> 
> _______________________________________________
> 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/c99b8629/attachment.sig>