编译为可执行文件

备注

Idris 的文档已在知识共享 CC0 许可下发布。因此，在法律允许的范围内，Idris 社区 已经放弃了 Idris 文档的所有版权和相关或邻近的权利。

关于CC0的更多信息，可以在网上找到：http://creativecommons.org/publicdomain/zero/1.0/

Idris 2（语言）被设计为不依赖于任何特定的代码生成器。不过，由于编写程序的重点是能够运行它，所以知道如何运行是很重要的,默认情况下，Idris通过 Chez Scheme 编译为可执行文件。

你可以在 REPL 中按如下方式编译到可执行文件：

Main> :c execname expr

…其中 execname 是要生成的可执行文件的名称， expr 是将被执行的 Idris 表达式。 expr 必须拥有 IO () 的类型。这将产生一个可执行文件 execname ，在相对于当前工作目录的 build/exec 目录下。

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

Main> :exec expr

同样， expr 也必须要有类型 IO () 。

最后，你可以通过添加 -o <output file> 选项从命令行编译为可执行文件：

$ idris2 hello.idr -o hello

将编译表达式 Main.main ，在 build/exec 目录下生成一个可执行的 hello （根据代码生成器的不同，可能会有一个文件扩展名）。

默认情况下，Idris 2 是一个完整的程序编译器 - 也就是说，它找到所有必要的函数定义，并在你构建可执行文件时才编译它们。这提供了大量的优化机会，但对于重新构建来说可能会很慢。然而，如果后端支持的话，你可以 增量 构建模块和可执行文件：

如果后端支持，你可以通过设置 profile 标志来生成配置数据，或者用 --profile 启动 Idris，或者在 REPL 运行 :set profile 。生成的配置数据将取决于你所使用的后端。目前， Chez 和 Racket 后端支持生成配置数据。

Idris 2 中提供了五个代码生成器，并且有一个系统可以为各种目标语言插入新的代码生成器。默认是通过 Chez Scheme 编译，还有一个选择是通过 Racket 或 Gambit 编译。你可以在REPL中用 :set codegen 命令设置代码生成器，或者通过 IDRIS2_CG 环境变量进行设置。

还有一些其它的代码生成器，它们不是Idris 2 主资源库的一部分，你可以在 Idris 2 维基上找到：

其它后端

目前正在进行的工作是支持从 idris2 代码生成其他语言的库。