[Agda] [ANNOUNCE] Agda 2.5.1 release candidate

[Andreas Abel]

Thanks for testing Sergei!  Please do report a bug, so we can fix this 
regression before the release!  Cheers, Andreas

On 14.02.2016 20:26, Sergei Meshveliani wrote:
> On Sat, 2016-02-13 at 13:20 -0500, Andrés Sicard-Ramírez wrote:
>> Dear all,
>>
>> The Agda Team is very pleased to announce a release candidate of Agda
>> 2.5.1 available at
>>
>>    http://www1.eafit.edu.co/asr/tmp/Agda-2.5.0.20160213.tar.gz
>> [..]
>>    $ tar xzf Agda-2.5.0.20160213.tar.gz
>>    $ cd Agda-2.5.0.20160213.tar.gz
>>    $ cabal install
>>
>> [..]
>
>
> It does type-check my (large) project of DoCon-A.
>
> But it fails to compile it to Haskell. After compiling about 5 modules,
> it reports
>
> -----------------------------
> Compiling Structures1
> in /home/mechvel/agda/tosave/bugs/feb14-2016/Structures1.agdai
> to /home/mechvel/agda/tosave/bugs/feb14-2016/MAlonzo/Code/Structures1.hs
> Unbound name: Structures1.OfMonoidHomo.recCon-NOT-PRINTED
> [157]@263218534
> An internal error has occurred. Please report this as a bug.
> Location of the error: src/full/Agda/TypeChecking/Reduce/Monad.hs:174
> -----------------------------
>
> This is for  ghc-7.10.2, MAlonzo, Debian Linux.
>
> Main.agda  is made by  agda -c,
> it is only
>
> -------------------------------------------- Main.agda ---
> open import Foreign.Haskell
> open import IO.Primitive
> open import Data.String using (toCostring)
>
> open import Structures1
>
> main : IO Unit
> main = putStrLn (toCostring "done")
> ----------------------------------------------
>
> But if I merge  Main.agda  to  Structures1.agda  then it is compiled
> (!).
>
> I am currently trying to minimize the example.
>
> Regards,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/