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
execname is the name of the executable file. This will generate
A shell script
build/exec/execnamewhich invokes the program
build/exec/execname_appwhich 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.
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
expr must have type
IO (). This will generate a temporary
_tmpchez in the
build/exec directory, and execute
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
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-toolby running the configuration script and then make:$ scheme --script gen-config.ss --bootpath <bootpath>
<bootpathis the path to where the Chez Scheme bootfiles (
scheme.hare. More configuration is described in the chez-exe installation instructions.
compile-chez-program:$ compile-chez-program --optimize-level 3 build/exec/my_idris_prog_app/my_idris_prog.ss
Note 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
The finished executable still requires the libidris_support shared library. It’s possible to also eliminate that dependency by linking with it statically.