[Agda] [ANNOUNCE] Agda 2.6.2 release candidate

[Jesper Cockx]

Hi Sergei,

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.

(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.)

-- Jesper


On Sat, Jun 5, 2021 at 1:15 PM <mechvel at scico.botik.ru> wrote:

> On 2021-05-25 18:40, Andrés Sicard-Ramírez wrote:
> > Dear all,
> >
> > The Agda Team is very pleased to announce a release candidate of Agda
> > 2.6.2. We plan to release 2.6.2 in a few days.
> >
>
> > # Standard library
> >
> > For the time being, you can use the *experimental* branch of the
> > standard library with Agda 2.6.2 RC. This branch is available at
> >
> >     https://github.com/agda/agda-stdlib/
> >
>
> I have downloaded the .zip archive from
> https://github.com/agda/agda-stdlib/, Code,
>
> and tried to type-check my application under Ubuntu-Linux 18.04,
> ghc-9.0.1.
>
>   > agda $agdaLibOpt ForTests
>
> reports
>
> .../source/ForTests.agda:22,1-24,30
> Importing module IO using the --guardedness flag from a module
> which does not.
> when scope checking the declaration
>    open import IO public
>                   using (Main; IO; run; putStr; putStrLn; readFiniteFile;
> writeFile;
>                          appendFile)
>
> Something has changed in standard library?
>
> --
> SM
> _______________________________________________
> 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/20210605/75fd648d/attachment.html>