在 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