This is the bootstrapping version of Idris 2, the successor to Idris. Its sole purpose is to build Idris 2 proper. Most likely, you will want to install that directly, unless you're following the bootstrapping path from scratch.
Please note: To build, this requires Idris version 1.3.2
Idris 2 is mostly backwards compatible with Idris 1, with some minor exceptions. The most notable user visible differences, which might cause Idris 1 programs to fail to type check, are:
private
, export
,
and public export
, which now refer to visibility of names from other
namespaces rather than visibility from other files.%language
pragma in Idris 1 is likely to be different.
Notably, elaborator reflection will exist, but most likely in a slightly
different form because the internal details of the elaborator are different.Prelude
is much smaller (and easier to replace with an alternative).let x = val in e
no longer computes with x
in e
, instead being
essentially equivalent to (\x => e) val
. This is to make the
behaviour of let
consistent in the presence of case
and with
(where
it is hard to push the computation inside the case
/with
efficiently).
Instead, you can define functions locally with let
, which do have
computational force, as follows:
let x : ? x = val in e
Watch this space for more details and the rationale for the changes, as I get around to writing it...
Summary of new features:
let
bindings are now more expressive, and can be used to define pattern
matching functions locally.case
expressions, and means fewer annotations are needed in interface
declarations.A significant change in the implementation is that there is an intermediate
language TTImp
, which is essentially a desugared Idris, and is cleanly
separated from the high level language which means it is potentially usable
as a core language for other high level syntaxes.
To build and install what exists of it so far:
PREFIX
in Makefile
make idris2
make install
You'll need to set your PATH
to $PREFIX/bin
You may also want to set IDRIS_CC
to clang
, since this seems to build
the generated C significantly faster.
Note: If you edit idris2.ipkg
to use the opts
with optimisation set
(--cg-opt -O2
) you'll find it runs about twice as fast, at the cost of
taking a couple of minutes to generate the idris2
executable.
You can check that building succeeded by running
make test
I make no promises how well this works yet, but you are welcome to have a play. Good luck :).
Information about external dependencies are presented in INSTALL.md.