[Agda-dev] New Agda Compiler/Backend

[Nils Anders Danielsson]

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