[Agda] [ANNOUNCE] Agda 2.5.1 release candidate

[Philipp Hausmann]

I also encountered this issue, I opened an issue:
https://github.com/agda/agda/issues/1839

Philipp

On 02/14/2016 10:46 PM, Andreas Abel wrote:
> 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
>>
>
>


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
Url : http://lists.chalmers.se/pipermail/agda/attachments/20160215/3d67f978/signature.bin