<div dir="ltr"><div><div><div>Thank you very much for running these tests. I'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'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.<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"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></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="">> As Andrés said, I unfortunately cannot test DoCon-A-0.03 with my new<br>
> unifier because I get a parse error at<br>
> source/Int/Integer1.agda:418,11-422,15. Do you have a version that is<br>
> compatible with the current Agda master?<br>
><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<N>m -RTS List/Sorting.agda<br>
Goal II:<br>
agda $agdaLibOpt +RTS -M<N>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' 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' example, agda-unification is slightly higher type<br>
check performance (in space * time),<br>
<br>
* for the `heavy' 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>