<div dir="ltr"><div><div><div>I understand completely that you don't want to try it yet, there's enough new versions of Agda coming out already. I'll let you know when the new unifier makes it to the master branch.<br><br></div>I will try to find a machine to run the DoCon-A-0.03 test on, as I only have 8GB of ram in my system.<br><br></div>regards,<br></div>Jesper<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Dec 14, 2015 at 10:10 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 Mon, 2015-12-14 at 21:47 +0100, Jesper Cockx wrote:<br>
> Andrés is talking about a new unifier which I'm working on, but is not<br>
> yet in the master branch because it still has some small problems.<br>
> Currently, the only way to use it is by pulling the branch from my<br>
> github and recompiling Agda from that version. You can do so by<br>
> following the instructions by Andrés in<br>
> <a href="https://lists.chalmers.se/pipermail/agda-dev/2015-December/000224.html" rel="noreferrer" target="_blank">https://lists.chalmers.se/pipermail/agda-dev/2015-December/000224.html</a>:<br>
> $ git branch -b unification<br>
> $ git fetch <a href="https://github.com/jespercockx/agda.git" rel="noreferrer" target="_blank">https://github.com/jespercockx/agda.git</a> unification<br>
> $ git merge FETCH_HEAD<br>
> $ make install-bin<br>
> I would be very grateful if you could test it on your code, and tell<br>
> me if the performance is better or worse than the current unifier (I<br>
> haven't optimized the code much yet, so it could very well be worse).<br>
> If you have problems installing or get any unexpected error messages,<br>
> I'd be glad to help of course.<br>
><br>
<br>
</span>Thank you.<br>
I am not sure that I would try it now, because it is very difficult to<br>
advance the project when trying different tool versions.<br>
<br>
You can use the test of DoCon-A-0.03:<br>
<br>
<a href="http://www.botik.ru/pub/local/Mechveliani/docon-A/0.03/" rel="noreferrer" target="_blank">http://www.botik.ru/pub/local/Mechveliani/docon-A/0.03/</a><br>
<br>
<br>
Under Agda 2.4.2.2, MAlonzo, Linux<br>
its type check needs 10 Gb space.<br>
<br>
You can try your agda-dev/2015-December on it, and compare the<br>
performance (space * time).<br>
<br>
Regards,<br>
<br>
------<br>
Sergei<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
><br>
> On Mon, Dec 14, 2015 at 8:30 PM, Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>><br>
> wrote:<br>
> On Sun, 2015-12-13 at 20:50 -0500, Andrés Sicard-Ramírez<br>
> wrote:<br>
> > On 13 December 2015 at 12:48, Sergei Meshveliani<br>
> <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>> wrote:<br>
> > > With<br>
> > ><br>
> > > open import Relation.Binary using (Setoid)<br>
> > ><br>
> > > Agda-2.4.2.4.20151210 does not import module Setoid.<br>
> > ><br>
> > > What is the relation between the language versions?<br>
> > > Which one is going to become 2.4.3 ?<br>
> ><br>
> > Agda 2.4.2.5 will be a bug-fix release and it won't include<br>
> the above behaviour.<br>
> ><br>
> > The above behaviour (see<br>
> ><br>
> <a href="https://github.com/agda/agda/blob/master/doc/release-notes/2-5-1.txt#L596" rel="noreferrer" target="_blank">https://github.com/agda/agda/blob/master/doc/release-notes/2-5-1.txt#L596</a><br>
> > ) will be include in Agda 2.4.4 whose release is planned for<br>
> early<br>
> > 2016.<br>
> ><br>
> > Since you are using the master version, did you test the new<br>
> > unification algorithm described in<br>
> ><br>
> ><br>
> <a href="https://lists.chalmers.se/pipermail/agda-dev/2015-December/000223.html" rel="noreferrer" target="_blank">https://lists.chalmers.se/pipermail/agda-dev/2015-December/000223.html</a><br>
> ><br>
> > ?<br>
><br>
><br>
> As I guess, this is about a certain new unifier which is a<br>
> part of the<br>
> type checker.<br>
> And how can I test it?<br>
> I only program a certain algebra library in Agda<br>
> (currently -- in Development of October 20, 2015).<br>
> And I do not know which unifier is used in its type checker.<br>
> I only observe that this my large application is type-checked<br>
> in 15<br>
> minutes under 13 Gb space. And Agda-2.4.2.4 needed somewhat<br>
> 1.3 times<br>
> more space and time.<br>
><br>
> What else can I test?<br>
> Are there some extended language possibility in this `master'<br>
> which can<br>
> increase the type check performance?<br>
><br>
> I am writing an application, and I know almost nothing about<br>
> Agda<br>
> implementation.<br>
><br>
> Generally, I think that the main current problem with Agda is<br>
> the type<br>
> check performance (space * time). This 13 Gb is somewhat 50<br>
> times more<br>
> that would look natural.<br>
><br>
> Another problem is of how to make it essentially easier<br>
> composing<br>
> proofs. But this problem is much more difficult than the first<br>
> one.<br>
><br>
> Regards,<br>
><br>
> ------<br>
> Sergei<br>
><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>
><br>
><br>
><br>
<br>
<br>
</div></div></blockquote></div><br></div>