[Agda] ANNOUNCE: Agda 2.4.2.5 release candidate

[Sergei Meshveliani]

On Tue, 2015-12-15 at 15:02 +0100, Jesper Cockx wrote:
> As Andrés said, I unfortunately cannot test DoCon-A-0.03 with my new
> unifier because I get a parse error at
> source/Int/Integer1.agda:418,11-422,15. Do you have a version that is
> compatible with the current Agda master?
> 


Comparing the Agda versions

agda-unification  of December 18, 2015  (ghc-7.10.2)
to
Development Agda  of December 18, 2015  (ghc-7.8.3)

on the library  DoCon-A-dec15-2015.

Goal I:
         agda $agdaLibOpt +RTS -M<N>m -RTS  List/Sorting.agda
Goal II:
         agda $agdaLibOpt +RTS -M<N>m -RTS  Stuctures9.agda

Goal II is run after  Structures7.agda  is type checked, so that it
remans to type-check  Stuctures8.agda Stuctures9.agda.

Both versions are under Debian Linux,
the machine for  agda-unification  is of 3.6 GHz,
the machine for  Development Agda  is of 3.1 GHz.


***********************************************************************
agda-unification,            |   Development Agda of December 18, 2015,
     ghc-7.10.2,  3.6 GHz    |   ghc-7.8.3,  3.1 GHz
---------------------------- |-----------------------------------------
                             |
                          Goal I                       ghc-7.10.2
N       time
5000    105 sec.             |   150                   105
2000    154                  |   167                   153
1700    297                  |   Heap exhausted        414   ??
1000    Heap exhausted       |                         Heap exhausted

			Goal II
     (type-check Structures9 after Structures7 is type-checked)

14000   955 sec.              |  1029
13500                         |  1331
13000  1371                   |  ~infinity
12500  ~infinity              |
                              |
                          Code size
Sorting.agdai      2.870.818  |   2.871.180            2.868.337
Sorting.hs         1.513.926  |   1.513.926            1.513.926
Sorting.o          8.873.560  |   9.023.144            8.873.560
Structures9.agdai 15.819.837  |  15.828.265
                              |
                 time for `sort' for  e = 17
                              |
8.9 sec                       |  8.9 sec               9.0
                              |
************************************************************************

The rightmost column is for  Development Agda  on ghc-7.10.2.
But this yields certain error for the example  Structures9
-- which I am going to report.

As the second machine has 36/31 times less frequency, probably, the
timing numbers in the right columns need to be divided by 1.16.

It is visible that
* for the `light' example,  agda-unification  is slightly higher type 
  check performance (in space * time),

* for the `heavy' example,  the two versions have the same performance,

* the size of  .agdai      is almost the same,
* the size of  .hs and .o  is precisely the same,
* the performace of a certain executable test for compiled 
  Sorting.sort is the same,
* the minimal space size for type checking is unnaturally large for both
versions.


------
Sergei