「形式化方法」系列的 14 篇文章建立了 Curry-Howard 同构、依值类型、归纳类型与 Lean 4 入门的理论底座。本系列从工具链入手，目标是让读者能独立用 Coq 完成 200 行以内的证明项目。本篇处理的问题只有一个：从零搭建一套可重复、可在 CI 上运行的 Coq 开发环境。

opam switch 管理

Coq 的工具链通过 opam 管理，opam 是 OCaml 生态的包管理器。Coq 8.20 要求 OCaml ≥ 4.09（coq-core.opam 里写的是 "ocaml" {>= "4.09.0"}），4.x 系列官方测试到 4.14.1，OCaml 5.x 支持仍标注为实验性——所以下面固定用 4.14.2。不同项目可能需要不同的 Coq 版本，因此每个项目建议使用独立的 opam switch。

本系列锚定 Coq 8.20，因为它是存量项目的公共分母。但要先说清一件事：Coq 在 8.20 之后更名为 Rocq，现在 opam install coq 装到的可能是 9.x 的兼容层。9.0 起标准库命名空间从 Coq 改成 Stdlib，继续写 Require Import Coq.X 会开始告警（正确写法是 From Stdlib Require Import X），coq_makefile 也改叫 rocq makefile，opam 侧的 ported 包改名为 rocq-core / rocq-stdlib，面向用户的元包是 rocq-prover。本篇后面的所有命令都按 8.20 写，装 9.x 的读者需要自行做这层名字翻译。

安装 opam（macOS）：

1
2
brew install opam
opam init --no-setup   # 初始化 ~/.opam，--no-setup 不修改 shell rc 文件

安装 opam（Linux）：

1
2
bash -c "sh <(curl -fsSL https://opam.ocaml.org/install.sh)"
opam init

创建并激活专用 switch：

1
2
opam switch create coq-dev 4.14.2
eval $(opam env)

opam switch create 会下载并编译对应版本的 OCaml，时间约 5–15 分钟。eval $(opam env) 将新 switch 的 PATH、OCAMLPATH 等变量导入当前 shell，每次打开新终端都需要执行一次，或者把 eval $(opam env) 加入 .zshrc / .bashrc。

验证 switch 激活：

1
2
opam switch show      # 应输出 coq-dev
ocaml --version       # 应输出 4.14.x

安装 Coq 与 vscoq2 的语言服务器：

1
opam install coq.8.20.1 vscoq-language-server

这里要区分两套互相竞争的 LSP 实现，它们不是上下游关系：

  • vscoq2 的后端是 opam 包 vscoq-language-server，可执行文件叫 vscoqtop，配套 VS Code 扩展 maximedenes.vscoq。
  • coq-lsp 是另一套独立实现（ejgallego 维护），opam 包 coq-lsp，配套扩展 ejgallego.coq-lsp。

两者选一个装即可，混装会让编辑器不知道该连哪个。本篇后面用 vscoq2。安装完成后验证：

1
2
coqc --version        # The Coq Proof Assistant, version 8.20.1
vscoqtop --version
包名 作用 备注
coq 核心编译器与标准库 coqc / coqtop / coqdep 均包含其中；8.18 起拆为 coq-core + coq-stdlib，coq 是元包
vscoq-language-server vscoq2 的 LSP 服务端 提供 vscoqtop，配 maximedenes.vscoq 扩展
coq-lsp 另一套 LSP 服务端 配 ejgallego.coq-lsp 扩展，与 vscoq2 二选一

_CoqProject 文件

Coq 的 coqc 本身不知道项目边界，_CoqProject 文件承担这个职责：它告诉 coqc（以及 IDE）如何从源文件路径映射到逻辑模块名。

最小示例，假设目录结构为：

1
2
3
4
5
MyProject/
├── _CoqProject
├── Basics.v
└── Logic/
    └── Props.v

_CoqProject 内容：

1
-R . MyProject

-R . MyProject 表示：把当前目录（.）下所有 .v 文件递归映射到 MyProject.* 命名空间。Basics.v 对应模块 MyProject.Basics，Logic/Props.v 对应 MyProject.Logic.Props。

另一个选项 -Q 与 -R 的区别不在「是否递归」，两者都递归；区别在 Require 允许写多短：

1
2
-Q . MyProject      # Require Import MyProject.Basics.  或  From MyProject Require Import Basics.
-R . MyProject      # 上面两种都行，额外允许部分限定名 Require Import Basics.

也就是说 -R 是 -Q 的放宽版，多出来的能力只有「省略前缀」这一项。库项目建议用 -Q，强制调用方写全限定名或 From 子句，避免和其他库撞名；-R 在教材和遗留项目里更常见，图的是少敲几个字。第 17 篇讲项目组织时用的是 -Q，口径与此一致。

_CoqProject 里还能放两类东西：具体的 .v 文件列表，以及编译选项。要注意直接转发给 coqc 的只有 -Q、-I、-R、-native-compiler 四个，其余 coqc 选项必须用 -arg 逐个包起来：

1
2
3
4
5
6
-R . MyProject
-Q /Users/you/.opam/coq-dev/lib/coq/user-contrib/mathcomp mathcomp
-arg -w -arg -notation-overridden

Basics.v
Logic/Props.v

MathComp 的路径不用手写，opam var lib 能问出来。另外它不在默认 opam 仓库里，装之前要先加源：

1
2
opam repo add coq-released https://rocq-prover.github.io/opam/released
opam install coq-mathcomp-ssreflect

验证 _CoqProject 是否被识别：

1
2
coq_makefile -f _CoqProject -o CoqMakefile
make -f CoqMakefile

coq_makefile 读取 _CoqProject 生成适合 make 的构建规则，是 Coq 项目的经典构建方式。

失败尝试 → 正确做法对照

直接在 MyProject/ 外运行 coqc Logic/Props.v 时，如果 Props.v 含有 Require Import MyProject.Basics.，会报错：

1
Error: Cannot find library MyProject.Basics in loadpath.

原因是 coqc 没有收到 -R 参数，不知道 MyProject.Basics 在哪里。正确做法有两种：

1
2
3
4
5
# 方案 A：手动传参
coqc -R . MyProject Logic/Props.v

# 方案 B：使用 coq_makefile 生成的 Makefile（推荐）
make -f CoqMakefile

在项目目录内启动 IDE 时，vscoq2 自动检测 _CoqProject 并注入正确的 -R 参数，手动写 coqc 调用只在命令行临时验证时需要。

dune-coq 集成

dune 是 OCaml 生态的现代构建系统，通过 coq.theory stanza 原生支持 Coq 项目。

先说版本红线：dune 的 Coq 支持已经跟着更名走完了一轮生命周期。dune 3.21 引入 (using rocq <版本>) 与 rocq.theory，把旧的 coq.* 兼容层剥掉；dune 3.24.0（2026-06）直接删掉了 (lang coq)，此后声明 (using coq ...) 不再是告警而是硬报错，dune 会给出一条指向 Rocq 的错误信息。dune 官方文档里的 coq.html 也随之下线，现在只有 rocq.html。

所以下面这套 coq.* 写法只在 dune 3.16 – 3.23 区间有效。要照着跑，把 dune 钉在这个区间：

1
opam pin add dune 3.23.0

对应关系见本节末尾的迁移表。

dune-project 文件：

1
2
(lang dune 3.16)
(using coq 0.9)

(using coq 0.9) 激活 Coq 支持扩展。这里的 0.9 是 dune 侧 Coq 语言扩展自己的版本号，跟 Coq 的版本无关——它标记的是 dune 支持哪些 coq.theory 字段。每个扩展版本有对应的 dune 最低要求：0.8 需要 (lang dune 3.8)，0.9 需要 3.16，0.10 需要 3.17。写 (lang dune 3.0) 配 (using coq 0.8) 会被 dune 直接拒绝，这是个容易踩的组合。

dune 文件（放在 MyProject/ 目录下）：

1
2
3
4
(coq.theory
 (name MyProject)
 (stdlib no)
 (theories Coq))

(name MyProject) 声明逻辑命名空间，等价于 _CoqProject 里的 -R . MyProject。标准库在 dune 里有特殊待遇：COQLIB/theories 会自动获得理论名 Coq 并被隐式加进依赖列表。dune 文档推荐的做法是关掉这个隐式行为再显式声明，也就是上面的 (stdlib no) + (theories Coq)——依赖关系写在纸面上，比隐式注入好维护。依赖外部库时，例如 MathComp：

1
2
3
4
(coq.theory
 (name MyProject)
 (stdlib no)
 (theories Coq mathcomp.ssreflect))

构建整个项目：

1
dune build

dune 会自动计算文件间依赖（通过 coqdep），并行编译无依赖关系的 .v 文件，比手写 Makefile 快。

迁移到 rocq.*

dune ≥ 3.24 上面的写法会直接报错，对应的新写法是：

1
2
3
; dune-project
(lang dune 3.24)
(using rocq 0.14)
1
2
3
4
5
; dune
(rocq.theory
 (name MyProject)
 (no_corelib)
 (theories Stdlib))

三处字面替换：using coq → using rocq、coq.theory → rocq.theory、(stdlib no) → (no_corelib)。(stdlib yes) 在 rocq 语言 0.14 里被删掉了，不用再写。理论名也跟着标准库改名走：8.x 的 Coq 变成 9.x 的 Stdlib。

dune 与 coq_makefile 的选择：

维度 coq_makefile dune
成熟度 Coq 内置，长期稳定 版本敏感：(using coq 0.9) 只在 dune 3.16–3.23 有效，3.24 起要换 (using rocq 0.14)
多语言项目 只管 Coq 可同时构建 OCaml + Coq
增量构建 有，但手动管理依赖 自动依赖图，增量准确
程序提取集成 需要额外 rules dune 可直接编译提取出的 OCaml
社区存量 大多数现有项目使用，CompCert 至今仍是 configure + Makefile 带 OCaml 插件的项目普遍在用，例如 coq-lsp、coq-elpi

纯 Coq 项目选 coq_makefile 没有问题；若项目涉及 OCaml 提取、多包发布或多仓构建，建议迁移到 dune。

VS Code vscoq2 配置

vscoq2（扩展 ID：maximedenes.vscoq）是目前 Coq 在 VS Code 上的主力扩展，取代 Legacy 版 coq-community.vscoq1。它通过前面装的 vscoqtop 提供实时证明状态，可以在编辑器右侧面板看到当前光标处的证明目标（Hypotheses / Goal）。

安装方式：在 VS Code 扩展面板搜索 VsCoq 或执行：

1
code --install-extension maximedenes.vscoq

settings.json 配置（工作区级别 .vscode/settings.json）：

1
2
3
4
5
{
  "vscoq.path": "/Users/user/.opam/coq-dev/bin/vscoqtop",
  "vscoq.proof.mode": 1,
  "vscoq.goals.diff.mode": "on"
}

vscoq.path 指向 vscoqtop 二进制——不是 coq-lsp，指错会让 LSP 初始化失败。路径取决于 opam switch 的安装位置，查找方式：

1
2
3
which vscoqtop
# 或
opam var bin

vscoq.proof.mode 控制证明检查时机：0 = 手动触发，1 = 连续检查（光标移动时自动更新目标窗口）。

Legacy 版 vscoq（coq-community.vscoq1）走的是 coqtop -ideslave 协议，与 vscoq2 的 LSP 服务端不兼容。两者不能同时激活，切换前需禁用旧扩展。

打开一个 .v 文件后，右键菜单可以选择 Coq: Step Forward 执行下一步，或直接用 Alt+Down / Alt+Up 前进后退证明步骤，目标窗口随光标实时刷新。

项目目录约定

一个典型 Coq 证明项目的目录布局：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
MyProject/
├── _CoqProject             # 编译参数与模块映射（或用 dune-project）
├── dune-project            # dune 构建根
├── dune                    # coq.theory stanza
├── theories/               # Coq 源文件，按主题分子目录
│   ├── Defs.v              # 基础定义
│   ├── Lemmas.v            # 辅助引理
│   └── Main.v              # 主定理
├── extraction/             # Extraction 输出与 OCaml 包装代码
│   └── Main.ml
├── tests/                  # 命令行测试脚本（可选）
└── .github/
    └── workflows/
        └── coq.yml

theories/ 与 extraction/ 分开是因为 Coq 的 Extraction 命令会输出 .ml 文件，把它们与 .v 文件混放容易污染模块命名空间。

Print Assumptions. 用于验证主定理不依赖任何非预期的公理：

1
2
3
4
5
6
7
8
9
10
11
(* theories/Main.v *)
Theorem and_comm' : forall P Q : Prop, P /\ Q -> Q /\ P.
Proof.
  intros P Q [HP HQ].
  split.
  - exact HQ.
  - exact HP.
Qed.

Print Assumptions and_comm'.
(* 输出：Closed under the global context *)

Closed under the global context 表示 and_comm' 不依赖任何额外公理，仅依赖 CIC（归纳构造演算）的内置规则。如果输出中出现 Axioms: 条目，说明证明用到了 Classical.classic 或 FunctionalExtensionality.functional_extensionality 等外加公理。

Show Proof. 在交互式证明中间使用，显示当前已构造的证明项：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
Goal forall P Q : Prop, P /\ Q -> Q /\ P.
Proof.
  intros P Q [HP HQ].
  Show Proof.
  (* 此时显示：
     (fun (P Q : Prop) (H : P /\ Q) =>
       match H with
       | conj HP HQ => ?Goal
       end)
     其中 ?Goal 是尚未填充的空洞 *)
  split.
  - exact HQ.
  - exact HP.
Qed.

Show Proof. 对理解 tactic 与 proof term 的对应关系有直接帮助——intros P Q [HP HQ] 对应的是模式匹配展开，split 对应的是 conj 构造子被拆成两个子目标。

CI 配置（GitHub Actions）

Coq 项目的 CI 核心步骤是：安装 opam → 创建 switch → 安装 Coq → 运行 coqc 或 dune build。

.github/workflows/coq.yml：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
name: CI

on:
  push:
    branches: [main]
  pull_request:

jobs:
  build:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - name: Set up opam
        uses: ocaml/setup-ocaml@v3
        with:
          ocaml-compiler: 4.14.2

      - name: Install Coq
        run: |
          opam install --yes coq.8.20.1 dune

      - name: Build
        run: |
          eval $(opam env)
          dune build

ocaml/setup-ocaml@v3 是 OCaml 社区维护的官方 action，内置 opam 缓存，重复构建时不需要重新编译 OCaml。注意它只装 opam 和 OCaml 编译器，dune 要自己 opam install。漏掉这一项，Build 步会以 dune: command not found 收场。完整运行一次约 8–12 分钟（首次含 OCaml 编译），后续缓存命中约 3–5 分钟。

这 8–12 分钟里绝大部分花在编译 OCaml 上，用预建镜像可以直接省掉。第 17 篇讲了 coq-community/docker-coq-action 的配法，本篇的 CI 配方只求最小可跑通，真要上生产以那篇为准。

若项目使用 coq_makefile 而非 dune，把 dune build 替换为：

1
2
coq_makefile -f _CoqProject -o CoqMakefile
make -f CoqMakefile

核心配置项汇总

文件 关键字段 作用
_CoqProject -R . Namespace 递归模块映射，coqc 和 IDE 共用
_CoqProject -Q . Namespace 仅 qualified 引用，适合库项目
dune-project (using coq 0.9) 激活 dune 的 Coq 支持扩展，需 (lang dune 3.16)；dune ≥ 3.24 已删除，改用 (using rocq 0.14)
dune (coq.theory (name ...) (stdlib no) (theories ...)) 声明 Coq 理论及依赖；新语言里是 rocq.theory + (no_corelib)
.vscode/settings.json vscoq.path 指向 vscoqtop 二进制
.github/workflows/coq.yml ocaml/setup-ocaml@v3 CI 上安装 opam + OCaml

练习

  1. 在 coq-dev switch 下执行 opam list | grep -E 'coq|vscoq'，确认 coq、vscoq-language-server 均已安装，记录各自版本号。

  2. 创建如下 _CoqProject，把 -R 改成 -Q，然后依次试 Require Import Basics.、Require Import MyProject.Basics.、From MyProject Require Import Basics. 三种写法，记录哪些在 -Q 下能过、哪些只在 -R 下能过。

    1
    -R . MyProject

  3. 在 theories/Main.v 末尾添加 Print Assumptions and_comm'.，在 VS Code 中把光标停在该行上，观察目标窗口输出，确认没有额外公理依赖。

参考资料