Chez Scheme 代码生成器

Chez Scheme 代码生成器是默认的，或者可以通过 REPL 命令访问：

Main> :set cg chez

因此，默认情况下，要运行 Idris 程序，您需要安装 Chez Scheme 。 Chez Scheme 是开源的，可通过大多数操作系统包管理器获得。

您可以在 REPL 中将类型为 IO () 的表达式 expr 编译为可执行文件，如下所示：

Main> :c execname expr

...其中 execname 是可执行文件的名称。这将生成以下内容：

调用程序的 shell 脚本 build/exec/execname
子目录 build/exec/execname_app 中包含运行程序所需的所有数据。这包括 Chez Scheme 源代码（ execname.ss ），已编译的 Chez Scheme 代码（ execname.so ）和外部函数定义所需的任何共享库。

可执行的 execname 可以重新定位到任何子目录，前提是 execname_app 也在同一个子目录中。

你也可以直接执行表达式：

Main> :exec expr

同样， expr 必须具有 IO () 类型。这将在 build/exec 目录中生成一个临时可执行脚本 _tmpchez ，并执行它。

Chez Scheme 是默认的代码生成器，因此如果您使用 -o execname 标志调用 idris2 ，它将生成一个可执行脚本 build/exec/execname ，和支持文件 build/exec/execname_app 。

Chez 指令

--directive extraRuntime=<path>

将来自 <path> 的 Scheme 源代码直接嵌入到生成的输出中。可以多次指定，在这种情况下，所有给定的文件都将按指定的顺序包含。

; 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

--directive lazy=weakMemo

使所有非顶层 Lazy 和 Inf 值被*弱*记忆化。也就是说，一旦这个表达式在运行时被求值，它允许在后续访问时不再重新计算，直到记忆化的值被垃圾收集器清除。垃圾收集器可以自行决定收集弱记忆化的值，因此当没有可用内存时，弱记忆化的值可以被清除。这就是为什么它比完全记忆化更安全。

构建独立的可执行文件

可以使用 chez-exe 将 Chez Scheme 系统和内置的 Idris2 程序嵌入到独立的可执行文件中。

通过运行配置脚本构建并安装 compile-chez-program-tool ，然后执行：
$ scheme --script gen-config.ss --bootpath <bootpath>
其中 <bootpath 是 Chez Scheme 引导文件（ petite.boot 和 scheme.boot ）和 scheme.h 所在的路径。更多配置在 chez-exe 安装说明中描述。
调用 compile-chez-program ：
$ compile-chez-program --optimize-level 3 build/exec/my_idris_prog_app/my_idris_prog.ss
请注意，它只能使用 .ss 文件而不是 .so 文件。要嵌入包括编译器在内的完整 Chez Scheme 系统，请添加 --full-chez 选项。
完成的可执行文件仍然需要 libidris_support 共享库。也可以通过静态链接来消除这种依赖关系。