This release mostly contains bug fixes and minor improvements, aiming towards releasing version 1.0 around the same time as the publication of Type Driven Development with Idris which will be very soon. There is also a new experimental feature, working towards support for linear types, but don’t expect this to work properly yet :). The changes since version 0.99 are detailed below.
Thanks as always to everyone who has contributed, either with code, documentation or by testing and reporting issues. You can find the names of all contributors in the CONTRIBUTORS file in the source repository.
- Language pragmas are now required for the less stable existing features, in addition to the existing
ElabReflection, which must be enabled to use
UniquenessTypes, which must be enabled to use
DSLNotation, which must be enabled to define a
FirstClassReflection, which must be enabled to define a
- New language extension
- This allows adding a /multiplicity/ to a binder which says how often it is allowed to be used; either 0 or 1 (if unstated, multiplicity is “many”)
- The typing rules follow Conor McBride’s paper “I Got Plenty o’ Nuttin'”
- This is highly experimental, unfinished, not at all polished. and there are still lots of details to sort out. Some features don’t quite work properly yet. But it is there to play with for the brave!
- Terminating programs has been improved with more appropriate functions (
exitSuccess) and a data structure (
ExitCode) to capture a program’s return code.
- Casting a
Doublenow ignores leading and trailing whitespace. Previously only leading whitespace was ignored.
- RTS functions
ARGVare now properly encoded using UTF-8 on Windows.
- New module
contribfor implementing and combining state transition systems
- Idris’ output has been updated to more accurately reflect its progress through the compiler i.e. Type Checking; Totality Checking; IBC Generation; Compiling; and Code Generation. To control the loudness of the reporting three verbosity levels are introduced:
--V2. The old aliases of
- New REPL command
:!that runs an external shell command.
- The REPL now colourises output on MinTTY consoles (e.g., Cygwin and MSYS) on Windows, which previously did not occur due to a bug.
- Idris now runs in a UTF-8-compatible codepage on Windows. This fixes many Unicode-rendering issues on Windows (e.g., error messages stating
commitBuffer: invalid argument (invalid character)).
- Idris now has a
--warnipkgflag to enable auditing of Idris packages during build time. Currently auditing check’s the list of modules specified in the
iPKGfile with those presented in the package directory.