<div dir="ltr"><div><div><div>Thank you very much for running these tests. I&#39;m happy to see that no new problems were introduced by the new unifier.<br><br></div>For the performance problems, I guess the unifier used for pattern matching is not a big performance bottleneck. I&#39;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&#39;m sorry that my new unifier didn&#39;t solve your performance problem. Still, it&#39;s good to see that its performance doesn&#39;t get worse on big projects.<br><br></div>regards,<br></div>Jesper<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Dec 19, 2015 at 2:48 PM, Sergei Meshveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Tue, 2015-12-15 at 15:02 +0100, Jesper Cockx wrote:<br>
</span><span class="">&gt; As Andrés said, I unfortunately cannot test DoCon-A-0.03 with my new<br>
&gt; unifier because I get a parse error at<br>
&gt; source/Int/Integer1.agda:418,11-422,15. Do you have a version that is<br>
&gt; compatible with the current Agda master?<br>
&gt;<br>
<br>
<br>
</span>Comparing the Agda versions<br>
<br>
agda-unification  of December 18, 2015  (ghc-7.10.2)<br>
to<br>
Development Agda  of December 18, 2015  (ghc-7.8.3)<br>
<br>
on the library  DoCon-A-dec15-2015.<br>
<br>
Goal I:<br>
         agda $agdaLibOpt +RTS -M&lt;N&gt;m -RTS  List/Sorting.agda<br>
Goal II:<br>
         agda $agdaLibOpt +RTS -M&lt;N&gt;m -RTS  Stuctures9.agda<br>
<br>
Goal II is run after  Structures7.agda  is type checked, so that it<br>
remans to type-check  Stuctures8.agda Stuctures9.agda.<br>
<br>
Both versions are under Debian Linux,<br>
the machine for  agda-unification  is of 3.6 GHz,<br>
the machine for  Development Agda  is of 3.1 GHz.<br>
<br>
<br>
***********************************************************************<br>
agda-unification,            |   Development Agda of December 18, 2015,<br>
     ghc-7.10.2,  3.6 GHz    |   ghc-7.8.3,  3.1 GHz<br>
---------------------------- |-----------------------------------------<br>
                             |<br>
                          Goal I                       ghc-7.10.2<br>
N       time<br>
5000    105 sec.             |   150                   105<br>
2000    154                  |   167                   153<br>
1700    297                  |   Heap exhausted        414   ??<br>
1000    Heap exhausted       |                         Heap exhausted<br>
<br>
                        Goal II<br>
     (type-check Structures9 after Structures7 is type-checked)<br>
<br>
14000   955 sec.              |  1029<br>
13500                         |  1331<br>
13000  1371                   |  ~infinity<br>
12500  ~infinity              |<br>
                              |<br>
                          Code size<br>
Sorting.agdai      2.870.818  |   2.871.180            2.868.337<br>
Sorting.hs         1.513.926  |   1.513.926            1.513.926<br>
Sorting.o          8.873.560  |   9.023.144            8.873.560<br>
Structures9.agdai 15.819.837  |  15.828.265<br>
                              |<br>
                 time for `sort&#39; for  e = 17<br>
                              |<br>
8.9 sec                       |  8.9 sec               9.0<br>
                              |<br>
************************************************************************<br>
<br>
The rightmost column is for  Development Agda  on ghc-7.10.2.<br>
But this yields certain error for the example  Structures9<br>
-- which I am going to report.<br>
<br>
As the second machine has 36/31 times less frequency, probably, the<br>
timing numbers in the right columns need to be divided by 1.16.<br>
<br>
It is visible that<br>
* for the `light&#39; example,  agda-unification  is slightly higher type<br>
  check performance (in space * time),<br>
<br>
* for the `heavy&#39; example,  the two versions have the same performance,<br>
<br>
* the size of  .agdai      is almost the same,<br>
* the size of  .hs and .o  is precisely the same,<br>
* the performace of a certain executable test for compiled<br>
  Sorting.sort is the same,<br>
* the minimal space size for type checking is unnaturally large for both<br>
versions.<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
------<br>
Sergei<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>