[Agda-dev] 2.4.4 roadmap

Jesper Cockx Jesper at sikanda.be
Mon Sep 28 14:37:07 CEST 2015


There's issue 1408 (https://github.com/agda/agda/issues/1408) and related,
which is the reason why I started writing a new unifier for pattern
matching from scratch. There's also quite some changes to the LHS splitting
and related parts. Most parts are already working, but error messages are
not yet implemented and it obviously needs testing before it could be
integrated into the main agda. If you want to see the current state, you
can check it out at https://github.com/jespercockx/agda/tree/unification.
Currently, it is a bit of a mess of refactorings and changes at various
places, but maybe I could sort out some of the refactorings and push those
to the repository already. What would be the best thing to do?

Jesper



On Mon, Sep 28, 2015 at 10:34 AM, Ulf Norell <ulf.norell at gmail.com> wrote:

> Now that 2.4.2.4 is out the door I think we should start focusing on
> getting 2.4.4 released. For that we should think about things that cannot
> easily be done after the release (on maint-2.4.4), like language changes or
> larger code refactorings.
>
> I don't think we should worry about about bugs unless they are sever.
> Those we can always fix later.
>
> Looking at the issues tagged with 2.4.4 only #892 is about changing the
> language. I should probably also fix #1407 since impossibles are never good.
>
> If possible we should try to get the explicit substitution branch sorted
> out and merged, and I'll have a think about the state of the reflection api
> and where we'd want that to be for 2.4.4. What are other things we should
> consider?
>
> / Ulf
>
>
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda-dev/attachments/20150928/99630e85/attachment.html


More information about the Agda-dev mailing list