Skip to content

Releases: idris-lang/Idris2

[v0.8.0] 2025 Hallowe'en Release

31 Oct 17:22

Choose a tag to compare

It has been nearly 2 years since the previous release, so it was high time for a new one and here it is!

Highlights include:

  • Autobind and Typebind modifier on operators allow the user to customise the syntax of operator to look more like a binder.
  • Totality checking will now look under data constructors, so Just xs will be considered smaller than Just (x :: xs).
  • Typst files can be compiled as Literate Idris.
  • Constructors with certain tags (CONS, NIL, JUST, NOTHING) are replaced with _builtin.<TAG> (eg _builtin.CONS). This allows the identity optimisation to optimise conversions between list-shaped things.
  • Refactored Uninhabited implementation for Data.List.Elem, Data.List1.Elem, Data.SnocList.Elem, and Data.Vect.Elem so it can be used for homogeneous (===) and heterogeneous (~=~) equality.
  • The RefC backend compiler can emit precise reference counting instructions where a reference is dropped as soon as possible. This allows you to reuse unique variables and optimize memory consumption.
  • Fix memory leaks of IORef in RefC backend. Now that IORef holds values by itself, global_IORef_Storage is no longer needed.
  • The NodeJS executable output to build/exec/ now has its executable bit set. That file already had a NodeJS shebang at the top, so now it is fully ready to go after compilation.

For a detailed list of changes, please see the CHANGELOG.

As always, thanks to the many people who have contributed, both old and new, whether by adding features, fixing code, reporting issues, or anything else. You can find a list of names in CONTRIBUTORS.

Happy Hallowe'en! Have fun!

Version 0.7.0 (2023 release)

22 Dec 13:55

Choose a tag to compare

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

See the CHANGELOG for full details.

Version 0.6.0

27 Oct 15:42
102d7eb

Choose a tag to compare

v0.6.0

Update version number in CHANGELOG (#2734)

v0.5.1

20 Sep 06:54
bf0a157

Choose a tag to compare

This is to solve a couple of build issues. It requires either Idris v0.4.0, or the bootstrap code, to build.

Chez Scheme 9.5 (possibly earlier versions too, I haven't checked) is now sufficient for the bootstrap build, like previous versions of Idris. Also removed the dependency on sha256sum since this is not portable.

v0.5.0

18 Sep 15:09
ada3eb4

Choose a tag to compare

Version 0.5.0 (#1931)

* Update version numbers and bootstrap scheme

* Use wall clock time for search timeouts

That was always the intention in any case, rather than the process time.

v0.4.0

23 Jun 18:40
ea1ad16

Choose a tag to compare

Merge pull request #1599 from edwinb/prepare-040

Changes for next release, 0.4.0