[Agda] ANNOUNCE: Agda 2.4.2.5 release candidate

[Jesper Cockx]

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.

Best regards,
Jesper

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151214/efbb253f/attachment-0001.html