增量代码生成（Incremental Code Generation）
默认情况下，Idris 2 是一个整体程序编译器——即在构建可执行文件时才查找所有必要的函数定义并进行编译。这为优化提供了大量机会，但在重新构建时可能较慢。然而，如果后端支持，也可以*增量*构建模块和可执行文件。为此，你可以：
在命令行中为每个希望增量使用的后端设置
--inc <backend>标志。设置
IDRIS2_INC_CGS环境变量，并用逗号分隔要增量使用的后端列表。
目前，仅 Chez 后端支持增量构建。
增量构建模块（Building modules incrementally）
如果设置了上述任一项，构建模块时会为模块中的所有定义生成已编译的二进制代码，以及常规的已检查 TTC 文件。例如：
$ idris2 --inc chez Foo.idr
$ IDRIS2_INC_CGS=chez idris2 Foo.idr
类型检查成功后，每个模块会在与 Foo.ttc 相同的构建目录下生成 Chez Scheme 文件（Foo.ss）、其已编译代码（Foo.so）以及常规的 Foo.ttc。
在增量模式下，若模块中存在空洞（hole），即使这些空洞会在其他模块中定义，也会收到警告。
增量构建可执行文件（Building executables incrementally）
如果使用了 --inc 或设置了 IDRIS2_INC_CGS，编译可执行文件时会尝试将所有已编译模块链接在一起，而不是一次性为所有函数生成代码。为实现此功能，所有被导入的模块*必须*已为当前后端以增量方式构建（若有缺失，Idris 会回退到整体程序编译，并发出警告）。
因此，可执行文件所用的所有包也必须为当前后端以增量方式构建。prelude、base、contrib、network 和 test 这些包默认都已为 Chez 后端启用增量编译支持。
在增量编译与整体程序编译之间切换时，建议先删除 build 目录。切换到增量编译时尤为重要，因为可能存在 Idris 当前无法检测到的过时目标文件！
覆盖增量编译（Overriding incremental compilation）
在构建可执行文件时，--whole-program 标志会覆盖所有增量编译设置。
性能说明（Performance note）
增量编译意味着可执行文件生成速度更快，尤其是在只有少量模块发生变化时。但这也意味着优化机会减少，生成的可执行文件性能可能不如整体编译。部署时建议使用 --whole-program 编译。