2

我一直在使用来自https://coq.inria.fr/的下载链接为 Windows 和 Mac 安装 Coq。但是，当我尝试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 的“最佳”方法，这样我就不会遇到上面提到的问题吗？

4

1 回答 1

3

虽然我不是 Windows 或 OSX 用户，但我想您会遇到这个问题，因为 Coq 安装程序不会更新系统PATH变量。该变量是终端用来查找与您键入的命令相对应的程序的目录列表。如果您不想通过其他方法安装 Coq，您可能应该找到安装coqc和coqtop二进制文件的位置，并将这些目录添加到您的PATH. 以下是有关如何执行此操作的一些参考：OSX，Windows。

于 2017-01-27T12:03:21.973 回答