如何安装Coq

Question

我一直在使用 https://coq.inria.fr/ 的下载链接安装 Coq，适用于 Windows 和 Mac。但是，当我在终端或命令提示符上尝试

coqc

或

coqtop

时，我收到错误消息，指出未找到该命令。尽管如此，我仍然可以在 Coq IDE 上几乎完美地运行 Coq，但是当我编译缓冲区时，特别是来自 Software Foundations 的练习，我收到以下消息。

Running: coqc -I '/Users/zhangsheng/Desktop/G/repos/Coqy/cis500' '/Users/zhangsheng/Desktop/G/repos/Coqy/cis500/Basics.v' 2>&1

据我了解，

2>&1

似乎是某种形式的误导，我觉得这就是

coqc

和

coqtop

似乎无法在我的终端/命令提示符上工作的原因。

有人可以建议在 Mac 或 Windows 或两者上安装 Coq 的“最佳”方法，这样我就不会遇到上面提到的问题吗？

Answer 1

虽然我不是 Windows 或 OSX 用户，但我想您遇到这个问题是因为 Coq 安装程序不会更新系统的

PATH

变量。该变量是终端使用的目录列表，用于查找与您键入的命令相对应的程序。如果您不想通过其他方法安装 Coq，您可能应该找到

coqc

和

coqtop

二进制文件的安装位置，并将这些目录添加到您的

PATH

。以下是有关如何执行此操作的一些参考：OSX、Windows。

Answer 2

使用Mac时，只需运行

brew install coq