在 MacOS 上安装 Coq

Created: November-22, 2018

你可以从此处下载 dmg 软件包来安装整个软件包。

该软件包包含可用于编写校样的 CoqIDE，或者你可以使用 coqtop 命令在终端上运行解释程序

使用自制软件在 MacOS 上安装 Coq 也很容易

brew install coq

或者如果你使用 MacPorts

sudo port install coq

对 Coq 没有好的 vi 支持。你可以在具有良好可用性的 emacs 中使用 Proof General。

要安装 Proof General，请删除旧版本的 Proof General，从 GitHub 克隆新版本

git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
cd ~/.emacs.d/lisp/PG
make

然后将以下内容添加到 .emacs 中：

;; Open .v files with Proof General's Coq mode
(load "~/.emacs.d/lisp/PG/generic/proof-site")

确保你运行的 emacs 是实际的 Emacs。如果遇到版本不匹配问题，可能必须再次运行 makefile，明确指定 Emacs 路径

make clean; make EMACS=/Applications/Emacs.app/Contents/MacOS/Emacs