如何安装Coq

Question

我一直在使用https://coq.inria.fr/上的下载链接来安装Coq。但是，当我在终端或命令提示符上尝试coqc或coqtop时，我收到错误消息，指出找不到该命令。尽管如此，我仍然可以在Coq IDE上很好地运行Coq，但是当我编译buffer时，特别是来自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。