[Agda] [ANNOUNCE] Agda 2.5.4 release candidate 2

Sergei Meshveliani mechvel at botik.ru
Sat May 26 20:11:35 CEST 2018


On Sat, 2018-05-26 at 00:20 -0500, Andrés Sicard-Ramírez wrote:
> Dear all,
> 
> The Agda Team is very pleased to announce the second release candidate
> of Agda 2.5.4. We plan to release 2.5.4 in one week.
> 
> [..]
> 
> Enjoy the RC and please test as much as possible.


I have ported DoCon-A-2.02  from  Agda-2.5.3  to  Agda 2.5.3.20180519

(both under MAlonzo, ghc-7.10.2, Debian Linux).

* The obtained DoCon-A-2.02.1 differs only in some paths to Standard
library modules, in changing order of arguments in the gmap standard
function, changing _,_ to _,′_ is a couple of places.

* This porting does not reveal any bug in the candidate Agda (!).

* I tried two tests for running executable. They show that the 
  candidate produces the executable code that performs about 10% faster 
  than under Agda-2.5.3.

* I compared time of type-checking/making respectively  
  DoCon-A-2.02   under Agda-2.5.3  and
  DoCon-A-2.02.1 under Agda-2.5.3.20180519.

The type checker of Agda-2.5.3.20180519 is about 30% less space eager
(at this test).
For the restriction of -M15G,  the candidate `makes' DoCon-A 15% faster.
The minimal space to type-check DoCon-A is 30% smaller than under
Agda-2.5.3. The candidate Agda needs 10 G byte for this.

I wonder what may be further optimization. 

Regards,

------
Sergei



More information about the Agda mailing list