我一直在使用来自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 的“最佳”方法,这样我就不会遇到上面提到的问题吗?