[Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1

[Matthew Daggitt]

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.
Best,
Matthew

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191229/d857a789/attachment.html>