我经常编译Coq来测试一些变化,但是这个过程非常慢,因为理论中的标准库/需要时间来编译.

是否有可能为实验生成“轻量级”Coq版本？

最佳答案 我通常做的是避免这种情况,即我使用bin / coqtop(或者你使用的任何二进制文件)而不是普通make.它只重新编译二进制文件.请注意,某些命令依赖于std(主要是前缀,基本类型的定义),因此如果修改理论,可能不得不重新编译所有内容.

希望能帮助到你,

V.

(为了防止它发生任何变化,我总是给出-local标志来配置).