[Agda-dev] 2.4.4 roadmap

[Ulf Norell]

It would probably make your life easier to push as much as you can. Your
changes to the unifier is precisely the kind of thing I had in mind that we
should get sorted out before releasing.

/ Ulf

On Mon, Sep 28, 2015 at 2:37 PM, Jesper Cockx <Jesper at sikanda.be> wrote:

> 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/26eb6525/attachment.html