[Agda] [ANNOUNCE] Agda 2.6.2 release candidate

[Jesper Cockx]

Hi Sergei,

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 *disable* it when you *don't*
need it. I hope this explains why we decided to make this change.

-- Jesper

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

> On 2021-06-05 15:05, Jesper Cockx wrote:
> > 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.)
>
>
> But what is the reason for not keeping the default option, as in Agda
> 2.6.1 ?
>
> I expect that many users (like myself) do not know what are coinductive
> functions,
> nor of productivity of these function, nor of sized types.
> These people simply need to print out the result of a computation
> (putStrLn).
> This forces them to import IO, and then, comes this --guardedness ...
> ?
>
> Regards,
>
> --
> SM
>
>
>
> >
> > -- 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/20210606/f41b52c5/attachment.html>