[Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1

[Sergei Meshveliani]

On Sat, 2018-05-19 at 15:33 -0500, Andrés Sicard-Ramírez wrote:
> Dear all,
> 
> The Agda Team is very pleased to announce the first release candidate
> of Agda 2.5.4. We plan to release 2.5.4 in one week.
> 
> 
> Installation
> =======
> 
> This RC can be installed using the following instruction:
> 
>   $ cabal install
> http://hackage.haskell.org/package/Agda-2.5.3.20180519/candidate/Agda-2.5.3.20180519.tar.gz
> 
> 
> GHC supported versions
> ===============
> 
> This RC has been tested with GHC 7.10.3, 8.0.2, 8.2.2 and 8.4.2 on
> Linux, macOS and Windows.
> 
> Please note that GHC 8.4.2 requires cabal-install ≥ 2.2.0.0.
> 
> 
> Standard library
> ==========
> 
> For the time being, you can use the `experimental` branch of the
> standard library which is compatible with
> this RC. This branch is available at
> 
>   https://github.com/agda/agda-stdlib/
> []
> 


I am porting  Binary-3.1  (see it on the web) to this
Agda-2.5.4-candidate (version 2.5.3.20180519) 
under ghc-7.10.2, MAlonzo, Debian Linux. 

First, this needs to change
  import Data.List.Any.Membership as Membership
  -->
  import Data.List.Membership.Setoid as Membership

in several files.
Then, everything is type-checked by

  > agda $agdaLibOpt GCD.agda

Then, `making' the test 

  > agda -c $agdaLibOpt GCDTest.agda
    
compiles several modules and then, reports

----------------------------------
...
[ 72 of 103] Compiling MAlonzo.Code.Data.Bool.Properties
( MAlonzo/Code/Data/Bool/Properties.hs,
MAlonzo/Code/Data/Bool/Properties.o )
[ 73 of 103] Compiling MAlonzo.Code.Data.List.NonEmpty
( MAlonzo/Code/Data/List/NonEmpty.hs,
MAlonzo/Code/Data/List/NonEmpty.o )
[ 74 of 103] Compiling MAlonzo.Code.Data.Colist
( MAlonzo/Code/Data/Colist.hs, MAlonzo/Code/Data/Colist.o )
Compilation error:

MAlonzo/Code/Data/Colist.hs:295:11:
    Couldn't match type ‘MAlonzo.RTE.Inf (T48 xa xA)’ with ‘[xA]’
    Expected type: xA
                   -> MAlonzo.RTE.Infinity xa (T48 xa xA) -> T48 xa xA
      Actual type: xA -> [xA] -> [xA]
    Relevant bindings include
      check60 :: xA -> MAlonzo.RTE.Infinity xa (T48 xa xA) -> T48 xa xA
        (bound at MAlonzo/Code/Data/Colist.hs:295:1)
    In the expression: (:)
    In an equation for ‘check60’: check60 = (:)
-------------------------------------

Regards,

------
Sergei