[Agda] ANNOUNCE: Agda 2.4.2.5 release candidate

[Jesper Cockx]

Thank you very much for running these tests. I'm happy to see that no new
problems were introduced by the new unifier.

For the performance problems, I guess the unifier used for pattern matching
is not a big performance bottleneck. I've noticed the same thing with my
tests on the standard library, where unification takes less than 1 second
of the total time. So I'm sorry that my new unifier didn't solve your
performance problem. Still, it's good to see that its performance doesn't
get worse on big projects.

regards,
Jesper

On Sat, Dec 19, 2015 at 2:48 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151219/8c30a487/attachment-0001.html