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

当我编译使用标准库的阿格达程序，编译器花费很长的时间打印出线路如：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文件）。但它仍然花费大量时间跳过它们，编译花费的时间不止一分钟。

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

来源

2012-03-15 Owen

通过编译你的意思是生产一个可执行文件或只是typechecking？ – Saizan 2012-10-21 01:15:56

@saizan好问题。我认为只需进行类型检查就足够了，因为它是最重复的任务。虽然生成一个可执行文件也很好。 – Owen 2012-10-21 04:42:00

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

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

来源

2012-09-16 21:41:46 NovaDenizen

嗯....我想我并不是在寻找模块化编译，我只是喜欢在编辑器之外的命令行中运行编译器;即因为Agda可以在emacs中快速重新检查类型，如果它可能作为恶魔运行......你明白我的意思了吗？ – Owen 2012-10-21 04:45:02

Agda必须将至少一些.agdai文件加载到内存中，以便能够检查自己的代码，这可能是为什么即使跳过检查这些模块仍需要一些时间。

来源

2012-10-21 01:18:58 Saizan

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

回答

相关问题