[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