[Agda] ANNOUNCE: Agda 2.4.2.5 release candidate

[Sergei Meshveliani]

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