[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