Lambda the Ultimate

Edwin Brady has been working on the next version of the dependently-typed, eager, general-purpose Idris. It is now self-hosting.

tl;dr (twitter)

Edwin's press release (from the Idris mailing list):

Hi all,

I decided a couple of days ago, it was finally to time to have a go at
seriously porting Idris 2 to compile itself. To my surprise, it actually
worked (barring a couple of bits and pieces such as some details of the
IDE mode, and a couple of language issues that I'll resolve shortly.)

You can see the results here: https://github.com/edwinb/Idris2-SH

At some point in the next couple of weeks, I'll probably move to this as
the main development version - once I've ironed out the issues, and
worked out what a good process is for building and developing.

[..]

This also enables some other things that I've been holding back on for
the moment: plugin code generators, and better metaprogramming, among
other things.

Much more on this later. For now, I thought it would be nice to let
other people have a go with it.

My favourite new feature is that building the whole thing from scratch,
in the fully self hosted version, now takes about 1m45 on my machine,
which is about as long as the code generation along for the Idris 1
version :).

A shout-out to Chez Scheme, which Edwin uses for bootstrapping.