[Agda-dev] New Agda Compiler/Backend

Ulf Norell ulf.norell at gmail.com
Wed Mar 25 14:54:33 CET 2015


It built and passed the test suite so I merged it. Philipp I invited you to
the agda group on github so you can commit directly to the main repo when
you make further developments on the backend.

As Nils Anders said some text should be added to
doc/release-notes/2-4-4.txt.

Also, it would be a good idea if you could take some of your test programs
and set
up a test/uhc directory that could be run as part of make test.

/ Ulf

On Tue, Mar 24, 2015 at 10:38 AM, Nils Anders Danielsson <nad at cse.gu.se>
wrote:

> On 2015-03-23 17:15, Philipp Hausmann wrote:
>
>> Our backend is not finished, there are some improvements we still want
>> to make, but we think it is sufficiently stable now for general usage.
>> Related to this, we would like to merge this into Agda; if that is
>> possible and you are interested in doing so.
>>
>
> Sounds OK to me (but I haven't looked at the code). As I see it an
> important potential problem with merging in a new backend or feature is
> that there is a risk that it might be abandoned by the original
> developers. However, in this case I guess that most of the code is
> fairly independent of the rest of the code base, so it should be easy to
> drop support for this backend if it starts to bit-rot.
>
>  It adds some new pragmas and command line options,
>>
>
> Please document these changes in the release notes.
>
> --
> /NAD
>
> _______________________________________________
> 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/20150325/a80d03e3/attachment.html


More information about the Agda-dev mailing list