Chez Scheme Code Generator
The Chez Scheme code generator is the default, or it can be accessed via a REPL command:
Main> :set cg chez
By default, therefore, to run Idris programs you will need to install Chez Scheme. Chez Scheme is open source, and available via most OS package managers.
You can compile an expression expr
of type IO ()
to an executable as
follows, at the REPL:
Main> :c execname expr
…where execname
is the name of the executable file. This will generate
the following:
A shell script
build/exec/execname
which invokes the programA subdirectory
build/exec/execname_app
which contains all the data necessary to run the program. This includes the Chez Scheme source (execname.ss
), the compiled Chez Scheme code (execname.so
) and any shared libraries needed for foreign function definitions.
The executable execname
is relocatable to any subdirectory, provided that
execname_app
is also in the same subdirectory.
You can also execute an expression directly:
Main> :exec expr
Again, expr
must have type IO ()
. This will generate a temporary
executable script _tmpchez
in the build/exec
directory, and execute
that.
Chez Scheme is the default code generator, so if you invoke idris2
with the
-o execname
flag, it will generate an executable script
build/exec/execname
, again with support files in build/exec/execname_app
.
Chez Directives
--directive extraRuntime=<path>
Embed Scheme source from
<path>
directly into generated output. Can be specified more than once, in which case all given files will be included in the order specified.; extensions.scm (define (my-mul a b) (* a b))
-- Main.idr %foreign "scheme:my-mul" myMul : Int -> Int -> Int
$ idris2 --codegen chez --directive extraRuntime=/path/to/extensions.scm -o main Main.idr
Making a freestanding executable
It’s possible to embed the Chez Scheme system and the built Idris2 program into a freestanding executable with chez-exe.
Build and install the
compile-chez-program-tool
by running the configuration script and then make:$ scheme --script gen-config.ss --bootpath <bootpath>where
<bootpath
is the path to where the Chez Scheme bootfiles (petite.boot
andscheme.boot
) andscheme.h
are. More configuration is described in the chez-exe installation instructions.Invoke
compile-chez-program
:$ compile-chez-program --optimize-level 3 build/exec/my_idris_prog_app/my_idris_prog.ssNote that it can only use the
.ss
-file and not the.so
-file. To embed the full Chez Scheme system including the compiler add the--full-chez
option.The finished executable still requires the libidris_support shared library. It’s possible to also eliminate that dependency by linking with it statically.