[Agda] [ANNOUNCE] Agda 2.6.2 release candidate

[mechvel at scico.botik.ru]

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