[Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1

[Sergei Meshveliani]

On Thu, 2018-05-24 at 07:53 -0500, Andrés Sicard-Ramírez wrote:
> On 23 May 2018 at 13:51, Sergei Meshveliani <mechvel at botik.ru> wrote:
> >   > agda -c $agdaLibOpt GCDTest.agda
> >
> > 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 = (:)
> 
> I have no problem using the *experimental* branch of the standard
> library (but I could reproduce the above error using its *master*
> branch).
> 
> Note that you should use the *experimental* branch of the standard
> library with Agda 2.5.4 RC 1.


Now, I follow your instruction:

>> 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 go to  
     https://github.com/agda/agda-stdlib/

and choose the button "Clone or download", choosing "download".
And it downloads 
                 agda-stdlib-master.zip  (483201 byte).

Is this the experimental branch?
I apply
  
  > agda -V
  Agda version 2.5.3.20180519

  > unzip agda-stdlib-master.zip
  > mv <appeared directory> master-may23
  > cd master-may23
  > cabal update
  > cabal install 

This seems to work.

I put  "/home/mechvel/agda/stLib/master-may23/src"
on the path in  $agdaLibOpt  and test it by

  > echo $agdaLibOpt
  -i . -i /home/mechvel/agda/stLib/master-may23/src  
  -i /home/mechvel/agda/UNPrelude/src

Then I apply

  > agda $agdaLibOpt GCD.agda
  > agda -c $agdaLibOpt GCDTest.agda

and again, it yieds

  MAlonzo/Code/Data/Colist.hs:295:11:
      Couldn't match type ‘MAlonzo.RTE.Inf (T48 xa xA)’ with ‘[xA]’
  ...

??

------
Sergei