<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
Hi Jesper,
<div class=""><br class="">
</div>
<div class="">I ran agda with the --rewriting flag, as in</div>
<div class=""><br class="">
</div>
<div class="">agda --rewriting Lambda.agda</div>
<div class=""><br class="">
</div>
<div class="">and got the following error:</div>
<div class=""><br class="">
</div>
<div class="">
<div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo;" class="">
<span style="font-variant-ligatures: no-common-ligatures" class="">Checking examples.Lambda (/Users/jsiek/abstract-binding-trees/src/examples/Lambda.agda).</span></div>
<div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo;" class="">
<span style="font-variant-ligatures: no-common-ligatures" class=""> Checking Syntax (/Users/jsiek/abstract-binding-trees/src/Syntax.agda).</span></div>
<div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo;" class="">
<span style="font-variant-ligatures: no-common-ligatures" class=""> Checking Data.List (/usr/local/Cellar/agda/2.6.0.1_1/lib/agda/src/Data/List.agda).</span></div>
<div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo;" class="">
<span style="font-variant-ligatures: no-common-ligatures" class=""> Checking Data.List.Base (/usr/local/Cellar/agda/2.6.0.1_1/lib/agda/src/Data/List/Base.agda).</span></div>
<div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo;" class="">
<span style="font-variant-ligatures: no-common-ligatures" class=""> Checking Data.Bool.Base (/usr/local/Cellar/agda/2.6.0.1_1/lib/agda/src/Data/Bool/Base.agda).</span></div>
<div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo;" class="">
<span style="font-variant-ligatures: no-common-ligatures" class=""> Checking Data.Unit.Base (/usr/local/Cellar/agda/2.6.0.1_1/lib/agda/src/Data/Unit/Base.agda).</span></div>
<div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo;" class="">
<span style="font-variant-ligatures: no-common-ligatures" class="">/usr/local/Cellar/agda/2.6.0.1_1/lib/agda/src/Data/Bool/Base.agda:11,1-37</span></div>
<div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo;" class="">
<span style="font-variant-ligatures: no-common-ligatures" class="">Cannot set OPTIONS pragma --rewriting with safe flag.</span></div>
<div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo;" class="">
<span style="font-variant-ligatures: no-common-ligatures" class="">when scope checking the declaration</span></div>
<div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo;" class="">
<span style="font-variant-ligatures: no-common-ligatures" class=""> open import Data.Unit.Base using (⊤)</span></div>
<div class=""><span style="font-variant-ligatures: no-common-ligatures" class=""><br class="">
</span></div>
<div class=""><span style="font-variant-ligatures: no-common-ligatures" class="">But now I’m thinking I don't need to add the --rewriting flag at the command line.</span></div>
<div class=""><span style="font-variant-ligatures: no-common-ligatures" class="">I can instead add</span></div>
<div class=""><span style="font-variant-ligatures: no-common-ligatures" class=""><br class="">
</span></div>
<div class=""><span style="font-variant-ligatures: no-common-ligatures" class="">
<div class="">{-# OPTIONS --rewriting #-}</div>
<div class=""><br class="">
</div>
<div class="">at the top of Lambda.agda and things seem to work.</div>
<div class=""><br class="">
</div>
<div class="">I originally thought I had to do both… I’m not sure what the distinction is between</div>
<div class="">using the command line flag versus the # OPTIONS… does the command line</div>
<div class="">flag apply --rewriting to all the files, whereas # OPTIONS only applies</div>
<div class="">the - -rewriting flag to one file?</div>
<div class=""><br class="">
</div>
<div class="">Cheers,</div>
<div class="">Jeremy</div>
</span></div>
<div class=""><span style="font-variant-ligatures: no-common-ligatures" class=""><br class="">
</span></div>
<div><br class="">
<blockquote type="cite" class="">
<div class="">On Apr 23, 2020, at 2:35 PM, Jesper Cockx <<a href="mailto:Jesper@sikanda.be" class="">Jesper@sikanda.be</a>> wrote:</div>
<br class="Apple-interchange-newline">
<div class="">
<div dir="ltr" class="">
<div class="">Hi Jeremy,</div>
<div class=""><br class="">
</div>
<div class="">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).</div>
<div class=""><br class="">
</div>
<div class="">-- Jesper<br class="">
</div>
</div>
<br class="">
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Thu, Apr 23, 2020 at 10:11 PM Siek, Jeremy <<a href="mailto:jsiek@indiana.edu" class="">jsiek@indiana.edu</a>> wrote:<br class="">
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div style="overflow-wrap: break-word;" class="">
<div class=""><br class="">
</div>
From a quick test run, it seems that --rewriting is incompatible with most if not
<div class="">all of the standard library. Is that correct? I was hoping to use --rewriting,</div>
<div class="">but using the standard library is rather more important.</div>
<div class=""><br class="">
</div>
<div class="">Cheers,</div>
<div class="">Jeremy<br class="">
<div class=""><br class="">
<div class="">
<div dir="auto" style="letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; text-decoration: none;" class="">
<div style="letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px;" class="">
<div style="letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px;" class="">
<div style="letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px;" class="">
<div class=""><span style="font-family: Menlo; font-size: inherit;" class="">__________________________________________</span><br style="font-family:Menlo" class="">
<span style="font-family:Menlo" class="">Jeremy G. Siek <<a href="mailto:jsiek@indiana.edu" target="_blank" class="">jsiek@indiana.edu</a>></span><br style="font-family:Menlo" class="">
<span style="font-family:Menlo" class="">Professor</span><br style="font-family:Menlo" class="">
<span style="font-family:Menlo" class="">Luddy School of Informatics, Computing, and Engineering</span><br style="font-family:Menlo" class="">
<span style="font-family:Menlo" class="">Indiana University Bloomington</span><br style="font-family:Menlo" class="">
<span style="font-family:Menlo" class=""><a href="http://homes.soic.indiana.edu/jsiek/" target="_blank" class="">http://homes.soic.indiana.edu/jsiek/</a></span><br class="">
</div>
<div class=""><span style="font-family:Menlo" class=""><br class="">
</span></div>
</div>
</div>
<br class="">
</div>
<br class="">
</div>
<br class="">
<br class="">
</div>
<br class="">
</div>
</div>
</div>
_______________________________________________<br class="">
Agda mailing list<br class="">
<a href="mailto:Agda@lists.chalmers.se" target="_blank" class="">Agda@lists.chalmers.se</a><br class="">
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank" class="">https://lists.chalmers.se/mailman/listinfo/agda</a><br class="">
</blockquote>
</div>
</div>
</blockquote>
</div>
<br class="">
<div class="">
<div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<div style="color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<div style="color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<div style="color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<div class=""><span style="font-family: Menlo; font-size: medium; orphans: 2; widows: 2;" class="">__________________________________________</span><br style="font-family: Menlo; orphans: 2; widows: 2;" class="">
<span style="font-family: Menlo; orphans: 2; widows: 2;" class="">Jeremy G. Siek <<a href="mailto:jsiek@indiana.edu" class="">jsiek@indiana.edu</a>></span><br style="font-family: Menlo; orphans: 2; widows: 2;" class="">
<span style="font-family: Menlo; orphans: 2; widows: 2;" class="">Professor</span><br style="font-family: Menlo; orphans: 2; widows: 2;" class="">
<span style="font-family: Menlo; orphans: 2; widows: 2;" class="">Luddy School of Informatics, Computing, and Engineering</span><br style="font-family: Menlo; orphans: 2; widows: 2;" class="">
<span style="font-family: Menlo; orphans: 2; widows: 2;" class="">Indiana University Bloomington</span><br style="font-family: Menlo; orphans: 2; widows: 2;" class="">
<span style="font-family: Menlo; orphans: 2; widows: 2;" class=""><a href="http://homes.soic.indiana.edu/jsiek/" class="">http://homes.soic.indiana.edu/jsiek/</a></span><br class="">
</div>
<div class=""><span style="font-family: Menlo; orphans: 2; widows: 2;" class=""><br class="">
</span></div>
</div>
</div>
<br class="Apple-interchange-newline">
</div>
<br class="Apple-interchange-newline">
</div>
<br class="Apple-interchange-newline">
<br class="Apple-interchange-newline">
</div>
<br class="">
</div>
</body>
</html>