[Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1
Sergei Meshveliani
mechvel at botik.ru
Fri May 25 19:56:24 CEST 2018
On Sat, 2018-05-19 at 15:33 -0500, Andrés Sicard-Ramírez wrote:
> Dear all,
>
> The Agda Team is very pleased to announce the first release candidate
> of Agda 2.5.4. We plan to release 2.5.4 in one week.
>
Can you please delay it a bit?
For I have ported only about 1/10 of DoCon-A-2.02.
Changelog says
> * Call-by-need reduction.
> Compile-time weak-head evaluation is now call-by-need, but each
> weak-head reduction has a local heap, so sharing is not maintained
> between different reductions.
>
> The reduction machine has been rewritten from scratch and should be
> faster than the old one in all cases, even those not exploiting
> laziness.
So that there are likely bugs to reveal during this porting.
It is strange that I do not meet them, so far.
By the way, do the above "compile-time", "reduction machine", and
"call-by-need" refer to the type check stage?
------
Sergei
More information about the Agda
mailing list