<div dir="ltr"><div dir="ltr"><div>Hi Sergei,</div><div><br></div><div>As noted in the changelog, in Agda 2.6.2 the --guardedness flag (which is used to typecheck modules that rely on the guardedness criterion for checking productivity of coinductive functions) is no longer enabled by default, so you need to add that flag if you want to use it (or if you want to use another module that uses it, as is the case here). If you do not want to add --guardedness to individual modules in your library, you can also simply put `flags: --guardedness` in your .agda-lib file to enable it for all modules in the library.</div><div><br></div><div>(The reason for this change is that we have two ways to check productivity: either --guardedness or --sized-types, but these two are incompatible. So from 2.6.2 you now have to choose which one you want to use.)<br></div><div><br></div><div>-- Jesper<br></div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, Jun 5, 2021 at 1:15 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-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 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; 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></div>