4

当我编译一个使用标准库的 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 文件）。但它仍然会花费大量时间跳过它们，并且编译需要一分钟以上。

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

4

2 回答 2

1

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

于 2012-10-21T01:18:58.837 回答
0

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

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

于 2012-09-16T21:41:46.017 回答