學習Coq筆記（一）：Windows下安裝Coq
阿新 • • 發佈：2018-12-10
正在學習形式語義這門課，需要使用到Coq作為輔助語言進行描述。因此，需要在熟悉Coq語言。然而，直接百度Coq會出現很多奇奇怪怪的結果（Google更準確，但是我在載入自定義庫遇到的問題沒有直接找到答案），因此特別在這裡做個筆記，以備後來查驗。
Coq的核心下載地址：https://coq.inria.fr/download，我選擇的是Windows下的8.8.1版本。安裝之後，記得將安裝目錄下的bin資料夾（In my case, that is "C:\\Coq\\bin"）加入環境變數Path。Coq安裝中會自己攜帶IDE，通常情況下已經夠用了，如果有需要，可以考慮Emacs的外掛ProofGeneral（專案地址： https://github.com/ProofGeneral/PG），解壓之後記得在配置檔案.emacs中加入load-file指令載入PG的proof-site.el檔案；在VSCode中也有vscoq的外掛，安裝之後記得加入Coq的bin資料夾地址。
這個時候Coq已經安裝完畢，就可以進行相關的操作了。如果需要載入自定義庫，記得將.v檔案Compile buffer成.vo檔案等一系列檔案，否則可能出現`Unable to locate library XXX`等問題。