[Agda] --rewriting and the Agda standard library

[Siek, Jeremy]

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<mailto: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<mailto: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<mailto: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<mailto:Agda at lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda

__________________________________________
Jeremy G. Siek    <jsiek at indiana.edu<mailto:jsiek at indiana.edu>>
Professor
Luddy School of Informatics, Computing, and Engineering
Indiana University Bloomington
http://homes.soic.indiana.edu/jsiek/






-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200423/d1b91ce1/attachment.html>