compilation - 在没有标准库的情况下编译 coq

Question

我经常编译 Coq 来测试一些变化，但是这个过程真的很慢，因为 theories/ 中的标准库编译需要时间。

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

Answer 1

为了避免这种情况，我通常会做的是 make bin/coqtop (或您使用的任何类型的二进制文件)而不是普通的 make .它只重新编译二进制文件。请注意，某些命令依赖于 std(主要是前奏，带有基本类型的定义)，因此如果您修改理论，您可能需要不时重新编译所有内容。

希望能帮助到你，

五、

(以防万一它改变了什么，我总是给 -local 标志来配置)。