[Agda] on 2.5.2

Sergei Meshveliani mechvel at botik.ru
Fri Aug 5 14:24:16 CEST 2016


Dear Agda developers,

the release of 0.04 of DoCon-A library is ready.

All the test examples do work -- except the one of an Euclidean
ResidueRing.
This latter ends with Segmentation fault at the running time, 
due to a bug in Agda 2.5.1.1.

And the the bug tracker writes that this is going to be fixed in  
Agda 2.5.2.

I think, it is better to delay the DoCon-A release until  Agda 2.5.2.

Another point is the type checker performance.
install.txt  of DoCon-A writes about necessity of  8 Gb RAM, 
and about interrupting the type-check in the middle and repeating the
command in order to fit into  -M7G.

Generally, it is desirable to do something with the type checker to make
it less space eager
(for example, I can send the code of DoCon-A-0.04-pre, so the you could
try something).

Regards,

------
Sergei



More information about the Agda mailing list