2

我一直在使用来自https://coq.inria.fr/的下载链接为 Windows 和 Mac 安装 Coq。但是,当我尝试coqccoqtop在终端或命令提示符上时,我收到错误消息,提示找不到该命令。尽管话虽如此,但我仍然可以在 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,您可能应该找到安装coqccoqtop二进制文件的位置,并将这些目录添加到您的PATH. 以下是有关如何执行此操作的一些参考:OSXWindows

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