<div dir="ltr"><div>Hi Sergei,</div><div><br></div><div>The reason why we chose to not leave --guardedness by default is because that would mean all libraries would use --guardedness by default as well, which would make it impossible to use those libraries together with --sized-types. It is easier to remember to enable --guardedness when you need it, instead of having to remember to <i>disable</i> it when you <i>don't</i> need it. I hope this explains why we decided to make this change.<br></div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, Jun 5, 2021 at 8:51 PM <<a href="mailto:mechvel@scico.botik.ru">mechvel@scico.botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On 2021-06-05 15:05, Jesper Cockx wrote:<br>
> Hi Sergei,<br>
> <br>
> As noted in the changelog, in Agda 2.6.2 the --guardedness flag (which<br>
> is used to typecheck modules that rely on the guardedness criterion<br>
> for checking productivity of coinductive functions) is no longer<br>
> enabled by default, so you need to add that flag if you want to use it<br>
> (or if you want to use another module that uses it, as is the case<br>
> here). If you do not want to add --guardedness to individual modules<br>
> in your library, you can also simply put `flags: --guardedness` in<br>
> your .agda-lib file to enable it for all modules in the library.<br>
> <br>
> (The reason for this change is that we have two ways to check<br>
> productivity: either --guardedness or --sized-types, but these two are<br>
> incompatible. So from 2.6.2 you now have to choose which one you want<br>
> to use.)<br>
<br>
<br>
But what is the reason for not keeping the default option, as in Agda <br>
2.6.1 ?<br>
<br>
I expect that many users (like myself) do not know what are coinductive <br>
functions,<br>
nor of productivity of these function, nor of sized types.<br>
These people simply need to print out the result of a computation <br>
(putStrLn).<br>
This forces them to import IO, and then, comes this --guardedness ...<br>
?<br>
<br>
Regards,<br>
<br>
--<br>
SM<br>
<br>
<br>
<br>
> <br>
> -- Jesper<br>
> <br>
> On Sat, Jun 5, 2021 at 1:15 PM <<a href="mailto:mechvel@scico.botik.ru" target="_blank">mechvel@scico.botik.ru</a>> wrote:<br>
> <br>
>> On 2021-05-25 18:40, Andrés Sicard-Ramírez wrote:<br>
>>> Dear all,<br>
>>> <br>
>>> The Agda Team is very pleased to announce a release candidate of<br>
>> Agda<br>
>>> 2.6.2. We plan to release 2.6.2 in a few days.<br>
>>> <br>
>> <br>
>>> # Standard library<br>
>>> <br>
>>> For the time being, you can use the *experimental* branch of the<br>
>>> standard library with Agda 2.6.2 RC. This branch is available at<br>
>>> <br>
>>> <a href="https://github.com/agda/agda-stdlib/" rel="noreferrer" target="_blank">https://github.com/agda/agda-stdlib/</a><br>
>>> <br>
>> <br>
>> I have downloaded the .zip archive from<br>
>> <a href="https://github.com/agda/agda-stdlib/" rel="noreferrer" target="_blank">https://github.com/agda/agda-stdlib/</a>, Code,<br>
>> <br>
>> and tried to type-check my application under Ubuntu-Linux 18.04,<br>
>> ghc-9.0.1.<br>
>> <br>
>>> agda $agdaLibOpt ForTests<br>
>> <br>
>> reports<br>
>> <br>
>> .../source/ForTests.agda:22,1-24,30<br>
>> Importing module IO using the --guardedness flag from a module<br>
>> which does not.<br>
>> when scope checking the declaration<br>
>> open import IO public<br>
>> using (Main; IO; run; putStr; putStrLn;<br>
>> readFiniteFile;<br>
>> writeFile;<br>
>> appendFile)<br>
>> <br>
>> Something has changed in standard library?<br>
>> <br>
>> --<br>
>> SM<br>
>> _______________________________________________<br>
>> Agda mailing list<br>
>> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>