A new version (0.7.0) of Idris 2 has been released. You can download the source (including generated Scheme and Racket files for bootstrapping) from the download page.

Highlights include:

• Size-change graphs are now matrices, faithfully implementing Lee, Jones, and Ben-Amram; 2001.
• Elaborator scripts can now access project files, allowing for type-providers and similar.
• Warnings on conflicting fixity declarations along with %hide support for these.
• Numerous doc and error message enhancements, bug fixes, performance improvements, and much more.

For a detailed list of changes, see the CHANGELOG.

Thanks to the many people who have contributed, whether by adding features, fixing code, reporting issues, or anything else. You can find a list of contributors in the GitHub repository.

Have fun!