初學 Coq 時看的是 Mathematical Components 這本書，它自帶了一個 Coq 的庫，這是它的安裝教程

這個庫的安裝要用到 OCaml Package Manager (OPAM) ，而它在本文所寫之時（2021/9/25）仍不支援 Windows

我採用作者推薦的方式安裝：採用 WSL 2

以下為步驟

1. 確認 Windows 版本為 1903 及以上

   可在終端內輸入winver，在開啟的視窗中檢視

2. 確認以下 Windows 功能均已啟動：

   • 適用於 Linux 的 Windows 子系統
   • 虛擬機器平臺

   可以在這裡檢視：控制面板 > 程式 > 程式和功能 > 啟用或關閉 Windows 功能

   或者直接在終端中輸入以下兩行指令以開啟：

   dism.exe /online /enable-feature /featurename:Microsoft-Windows-Subsystem-Linux /all /norestart
   dism.exe /online /enable-feature /featurename:VirtualMachinePlatform /all /norestart
   

   若未啟用功能，要在啟用後重啟電腦。

3. 升級 WSL

   • 下載並安裝 Linux 核心升級包：wsl_update_x64.msi

   • 在終端輸入wsl --set-default-version 2

4. 為 WSL 下載 GNU/Linux 發行版

   在 Microsoft Store 中選擇

   這裡我使用 Debian

   安裝完後執行，按提示設定好使用者名稱、密碼

   執行下列指令以安裝一些基礎應用

   • sudo apt update
   • sudo apt-get install emacs

5. 安裝 X.org 伺服器以便在 WSL 中使用圖形介面應用

   • 下載並安裝 VcXsrv Windows X Server

   • 開啟 XLaunch，依次選擇 Multiple windows、Start no client，勾上 Disable access control之後每次用 WSL 都需開啟並設定一次

   • 開啟控制面板 > 系統和安全 > Windows Defender 防火牆 > 高階設定 > 入站規則

   • 找到名稱為VcXsrv windows xserver的兩項，分別雙擊開啟並檢查：

     • 確認常規 > 操作 一欄中選擇了允許連線
     • 確認作用域中兩欄均選擇了任何 IP 地址

   • 在 WSL 終端內輸入emacs ~/.bashrc，在程式碼末尾新增一行：（這需要一點點的 Emacs 基礎知識）

     export DISPLAY=$(awk '/nameserver / {print $2; exit}' /etc/resolv.conf 2>/dev/null):0
     

   • 重啟 XLaunch，WSL 終端，這時啟動 Emacs 等圖形介面應用就應該會彈出一個獨立的視窗了

6. 依次在 WSL 終端中執行下列命令，其中的一些可能需要等待較長時間

   • sudo apt install opam libgmp3-dev libcairo2-dev libexpat1-dev libgtk-3-dev libgtksourceview-3.0-dev
     

   • opam init
     

   • opam switch create 4.11.2
     

   • opam repo add coq-released https://coq.inria.fr/opam/released
     

   • opam install coq
     

   • opam install coqide
     

   • opam install coq-mathcomp-ssreflect
     

   此時就已經安裝完了，輸入coqide便可進入 Coq 的整合開發環境

參考：Installation of MathComp on Windows 10