[Agda] --rewriting and the Agda standard library

[Matthew Daggitt]

Hi Jeremy,
 As the error message says, the `-- rewriting` flag is not compatible
<https://agda.readthedocs.io/en/v2.6.1/language/safe-agda.html#safe-agda>with
the `--safe` flag, and (as one would hope!) the standard library uses
`--safe` flag extensively.

As you say, passing the flag via the command line applies it to all files,
and therefore setting `--rewriting` in such a manner is not compatible with
the standard library. In contrast, as the `-- rewriting` flag is
neither infective
nor co-infective
<https://agda.readthedocs.io/en/v2.6.1/tools/command-line-options.html?highlight=infective#consistency-checking-of-options-used>,
adding it via an OPTIONS pragma only applies it to that file.
Cheers,
Matthew

On Fri, Apr 24, 2020 at 4:48 AM Siek, Jeremy <jsiek at indiana.edu> wrote:

> Hi Jesper,
>
> I ran agda with the --rewriting flag, as in
>
> agda --rewriting Lambda.agda
>
> and got the following error:
>
> Checking examples.Lambda
> (/Users/jsiek/abstract-binding-trees/src/examples/Lambda.agda).
>  Checking Syntax (/Users/jsiek/abstract-binding-trees/src/Syntax.agda).
>   Checking Data.List
> (/usr/local/Cellar/agda/2.6.0.1_1/lib/agda/src/Data/List.agda).
>    Checking Data.List.Base
> (/usr/local/Cellar/agda/2.6.0.1_1/lib/agda/src/Data/List/Base.agda).
>     Checking Data.Bool.Base
> (/usr/local/Cellar/agda/2.6.0.1_1/lib/agda/src/Data/Bool/Base.agda).
>      Checking Data.Unit.Base
> (/usr/local/Cellar/agda/2.6.0.1_1/lib/agda/src/Data/Unit/Base.agda).
> /usr/local/Cellar/agda/2.6.0.1_1/lib/agda/src/Data/Bool/Base.agda:11,1-37
> Cannot set OPTIONS pragma --rewriting with safe flag.
> when scope checking the declaration
>   open import Data.Unit.Base using (⊤)
>
> But now I’m thinking I don't need to add the --rewriting flag at the
> command line.
> I can instead add
>
> {-# OPTIONS --rewriting #-}
>
> at the top of Lambda.agda and things seem to work.
>
> I originally thought I had to do both… I’m not sure what the distinction
> is between
> using the command line flag versus the # OPTIONS… does the command line
> flag apply --rewriting to all the files, whereas # OPTIONS only applies
> the - -rewriting flag to one file?
>
> Cheers,
> Jeremy
>
>
> On Apr 23, 2020, at 2:35 PM, Jesper Cockx <Jesper at sikanda.be> wrote:
>
> Hi Jeremy,
>
> How exactly is --rewriting incompatible with the standard library? It's
> true that it does not use --rewriting, but you can always import a file
> that does not use --rewriting from one that does (the other way around is
> more problematic).
>
> -- Jesper
>
> On Thu, Apr 23, 2020 at 10:11 PM Siek, Jeremy <jsiek at indiana.edu> wrote:
>
>>
>> From a quick test run, it seems that --rewriting is incompatible with
>> most if not
>> all of the standard library. Is that correct? I was hoping to use
>> --rewriting,
>> but using the standard library is rather more important.
>>
>> Cheers,
>> Jeremy
>>
>> __________________________________________
>> Jeremy G. Siek    <jsiek at indiana.edu>
>> Professor
>> Luddy School of Informatics, Computing, and Engineering
>> Indiana University Bloomington
>> http://homes.soic.indiana.edu/jsiek/
>>
>>
>>
>>
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
> __________________________________________
> Jeremy G. Siek    <jsiek at indiana.edu>
> Professor
> Luddy School of Informatics, Computing, and Engineering
> Indiana University Bloomington
> http://homes.soic.indiana.edu/jsiek/
>
>
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200424/430e1717/attachment.html>