[Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1

[mechvel at scico.botik.ru]

On 2019-12-29 14:52, Matthew Daggitt wrote:
> As Andres said in his email, and as stated in the standard library
> README you need to use the `development` branch of the library rather
> the `master` branch with the release candidate.

Andres writes *experimental*, not `development`.
Also he writes
A> This branch is available at
A>
A> https://github.com/agda/agda-stdlib/

But I guess this is the master branch (?).
And how to download `experimental' ?

-- 
SM



> On Sun, Dec 29, 2019 at 7:39 PM <mechvel at scico.botik.ru> wrote:
> 
>> On 2019-12-22 14:41, Andres Sicard Ramirez wrote:
>>> [..]
>>> The Agda Team is very pleased to announce the first release
>> candidate
>>> of Agda 2.6.1.
>>> [..]
>>> The RC has been tested with GHC 8.8.1, 8.6.5, 8.4.4, 8.2.2 and
>> 8.0.2.
>>> [..]
>>> Standard library
>>> ==========
>>> 
>>> For the time being, you can use the *experimental* branch of the
>>> standard library which is compatible with the RC. This branch is
>>> available at
>>> 
>>> https://github.com/agda/agda-stdlib/
>>> [..]
>> 
>> I tried it on  ghc-8.6.3 under Ubuntu Linux 18.04 on a certain small
>> 
>> application
>> List0.agda:
>> 
>>> agda $agdaLibOpt List0.agda
>> 
>> As I guess, it first starts type-checking the needed part of the
>> "installed"
>> master library of December 29. And it reports
>> 
>> Checking List0 (/home/mechvel/inAgda/bfLib/0.3/List0.agda).
>> Checking Data.List.Relation.Unary.All.Properties
>> 
> (/home/mechvel/agda/stLib/master-dec29/src/Data/List/Relation/Unary/All/Properties.agda).
>> Checking Data.List.Membership.Propositional.Properties
>> 
> (/home/mechvel/agda/stLib/master-dec29/src/Data/List/Membership/Propositional/Properties.agda).
>> Checking Data.List.Relation.Unary.Any.Properties
>> 
> (/home/mechvel/agda/stLib/master-dec29/src/Data/List/Relation/Unary/Any/Properties.agda).
>> 
> /home/mechvel/agda/stLib/master-dec29/src/Data/List/Relation/Unary/Any/Properties.agda:251,16-27
>> B.b != q₁ of type Level
>> when checking that the inferred type of an application
>> Any.map _f_1489 y∈ys ≡ pq′
>> matches the expected type
>> Any.map (λ q₂ → p , q₂) (Any.map (λ x₁ → P.subst Q
>> x₁ _1452) y∈ys)
>> ≡ pq′
>> 
>> --
>> SM
>> 
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda