[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