[Agda] ANNOUNCE: Agda 2.4.2.5 release candidate

[Sergei Meshveliani]

On Mon, 2015-12-14 at 21:47 +0100, Jesper Cockx wrote:
> Andrés is talking about a new unifier which I'm working on, but is not
> yet in the master branch because it still has some small problems.
> Currently, the only way to use it is by pulling the branch from my
> github and recompiling Agda from that version. You can do so by
> following the instructions by Andrés in
> https://lists.chalmers.se/pipermail/agda-dev/2015-December/000224.html:
> $ git branch -b unification
>   $ git fetch https://github.com/jespercockx/agda.git unification
>   $ git merge FETCH_HEAD
>   $ make install-bin
> I would be very grateful if you could test it on your code, and tell
> me if the performance is better or worse than the current unifier (I
> haven't optimized the code much yet, so it could very well be worse).
> If you have problems installing or get any unexpected error messages,
> I'd be glad to help of course.
> 

Thank you.
I am not sure that I would try it now, because it is very difficult to
advance the project when trying different tool versions.

You can use the test of  DoCon-A-0.03:

http://www.botik.ru/pub/local/Mechveliani/docon-A/0.03/


Under   Agda 2.4.2.2, MAlonzo, Linux
its type check needs 10 Gb space.

You can try your  agda-dev/2015-December  on it, and compare the
performance (space * time).

Regards,

------
Sergei
 

> 
> On Mon, Dec 14, 2015 at 8:30 PM, Sergei Meshveliani <mechvel at botik.ru>
> wrote:
>         On Sun, 2015-12-13 at 20:50 -0500, Andrés Sicard-Ramírez
>         wrote:
>         > On 13 December 2015 at 12:48, Sergei Meshveliani
>         <mechvel at botik.ru> wrote:
>         > > With
>         > >
>         > >   open import Relation.Binary using (Setoid)
>         > >
>         > > Agda-2.4.2.4.20151210  does not import  module Setoid.
>         > >
>         > > What is the relation between the language versions?
>         > > Which one is going to become 2.4.3 ?
>         >
>         > Agda 2.4.2.5 will be a bug-fix release and it won't include
>         the above behaviour.
>         >
>         > The above behaviour (see
>         >
>         https://github.com/agda/agda/blob/master/doc/release-notes/2-5-1.txt#L596
>         > ) will be include in Agda 2.4.4 whose release is planned for
>         early
>         > 2016.
>         >
>         > Since you are using the master version, did you test the new
>         > unification algorithm described in
>         >
>         >
>          https://lists.chalmers.se/pipermail/agda-dev/2015-December/000223.html
>         >
>         > ?
>         
>         
>         As I guess, this is about a certain new unifier which is a
>         part of the
>         type checker.
>         And how can I test it?
>         I only program a certain algebra library in Agda
>         (currently -- in Development of October 20, 2015).
>         And I do not know which unifier is used in its type checker.
>         I only observe that this my large application is type-checked
>         in 15
>         minutes under 13 Gb space. And Agda-2.4.2.4 needed somewhat
>         1.3 times
>         more space and time.
>         
>         What else can I test?
>         Are there some extended language possibility in this `master'
>         which can
>         increase the type check performance?
>         
>         I am writing an application, and I know almost nothing about
>         Agda
>         implementation.
>         
>         Generally, I think that the main current problem with Agda is
>         the type
>         check performance (space * time). This 13 Gb is somewhat 50
>         times more
>         that would look natural.
>         
>         Another problem is of how to make it essentially easier
>         composing
>         proofs. But this problem is much more difficult than the first
>         one.
>         
>         Regards,
>         
>         ------
>         Sergei
>         
>         
>         _______________________________________________
>         Agda mailing list
>         Agda at lists.chalmers.se
>         https://lists.chalmers.se/mailman/listinfo/agda
>         
> 
>