Agda 可以在批处理模式下更快地编译吗？答案

【问题标题】：Can Agda compile faster in batch mode?Agda 可以在批处理模式下更快地编译吗？
【发布时间】：2012-03-31 17:12:22
【问题描述】：

当我编译一个使用标准库的 Agda 程序时，编译器会花费很长时间打印出如下行：

Skipping Relation.Binary.Consequences (/home/owen/install/lib-0.6/src/Relation/Binary/Consequences.agdai).
Skipping Relation.Binary.Indexed.Core (/home/owen/install/lib-0.6/src/Relation/Binary/Indexed/Core.agdai).
Skipping Relation.Binary (/home/owen/install/lib-0.6/src/Relation/Binary.agdai).

我猜它安全“跳过”它们的原因是它们已经编译（目录中已经有 .agdai 文件）。但是跳过它们仍然会花费大量时间，并且编译需要一分钟以上。

有没有办法在每次编译时避免所有这些额外的工作？

【问题讨论】：

编译是指生成可执行文件还是只是类型检查？
@saizan 好问题。我想只是类型检查就足够了，因为它是最重复的任务。虽然生成可执行文件也很好。

标签： compilation incremental-build agda

【解决方案1】：

Agda 必须将这些 .agdai 文件中的至少一部分加载到内存中才能对您自己的代码进行类型检查，所以这可能就是即使跳过这些模块的检查仍需要一些时间的原因。

【讨论】：

【解决方案2】：

Agda 和其他类似的软件系统（如 coq）具有可用的交互界面，通常通过安装在 emacs 中的 Proof General。

模块化编译在其他情况下也有效，因为编程语言往往依赖于对外部符号的浅名称检查，如果他们检查的话。 Agda 是一个证明系统，因此如果要完成其工作，它必须每次都从头开始，并深入验证整个证明。

【讨论】：

hmmm.... 我想我并不是在寻找模块化编译，我只是喜欢从与编辑器分开的命令行运行编译器；即因为agda可以在emacs中快速重新输入check，如果它可以作为一个恶魔运行......你明白我的意思吗？