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

opam switch 管理

Coq 的工具链通过 opam 管理，opam 是 OCaml 生态的包管理器。Coq 8.20 依赖 OCaml 4.14.x，不同项目可能需要不同的 Coq 版本，因此每个项目建议使用独立的 opam switch。

安装 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 与 coq-lsp：

1
opam install coq.8.20.1 coq-lsp

coq-lsp 是 Coq 的 Language Server Protocol 实现，VS Code 的 vscoq2 插件依赖它提供实时证明状态反馈。安装完成后验证：

1
2
coqc --version   # Coq 8.20.1
coq-lsp --version
包名 作用 备注
coq 核心编译器与标准库 coqc / coqtop / coqdep 均包含其中
coq-lsp LSP 服务端 vscoq2 的后端；也可用旧的 coq-serapi
coq-stdlib-compat 标准库跨版本兼容层 处理 8.18 → 8.19 → 8.20 的 API 变更

_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 的区别：

1
2
-Q . MyProject      # 仅映射 qualified 引用，短名称（Basics）不可见
-R . MyProject      # 同时允许不带前缀的短名称（Basics）和带前缀的（MyProject.Basics）

多数教学项目用 -R，库项目（避免命名冲突）用 -Q。_CoqProject 也可以列出额外的包含路径和编译选项，例如：

1
2
-R . MyProject
-Q /path/to/MathComp mathcomp

验证 _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 生态的现代构建系统，自 dune 3.x + Coq 8.17 起，通过 coq.theory stanza 原生支持 Coq 项目。

dune-project 文件：

1
2
(lang dune 3.0)
(using coq 0.8)

(using coq 0.8) 激活 Coq 支持扩展，版本 0.8 对应 Coq 8.17–8.20 的 dune 集成语义。

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

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

(name MyProject) 声明逻辑命名空间，等价于 _CoqProject 里的 -R . MyProject。(theories Coq) 表示依赖 Coq 标准库。依赖外部库时，例如 MathComp：

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

构建整个项目：

1
dune build

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

dune 与 coq_makefile 的选择：

维度 coq_makefile dune
成熟度 Coq 内置，长期稳定 需要 dune 3.x + Coq 8.17+
多语言项目 只管 Coq 可同时构建 OCaml + Coq
增量构建 有，但手动管理依赖 自动依赖图，增量准确
程序提取集成 需要额外 rules dune 可直接编译提取出的 OCaml
社区存量 大多数现有项目使用 新项目推荐；CompCert 8.x 已迁移

纯 Coq 项目选 coq_makefile 没有问题；若项目涉及 OCaml 提取、coq-lsp 配置或多仓构建，建议迁移到 dune。

VS Code vscoq2 配置

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

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

1
code --install-extension coq-community.vscoq2

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

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

vscoq.path 指向 coq-lsp 二进制，路径取决于 opam switch 的安装位置。查找当前 switch 下的路径：

1
2
3
which coq-lsp
# 或
opam var bin

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

旧版 vscoq（maximedenes.coq-vscode）使用 coqtop 协议，不兼容 coq-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

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

ocaml/setup-ocaml@v3 是 OCaml 社区维护的官方 action，内置 opam 缓存，重复构建时不需要重新编译 OCaml。完整运行一次约 8–12 分钟（首次含 OCaml 编译），后续缓存命中约 3–5 分钟。

若项目使用 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.8) 激活 dune 的 Coq 支持扩展
dune (coq.theory (name ...) (theories ...)) 声明 Coq 理论及依赖
.vscode/settings.json vscoq.path 指向 coq-lsp 二进制
.github/workflows/coq.yml ocaml/setup-ocaml@v3 CI 上安装 opam + OCaml

练习

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

  2. 创建如下 _CoqProject，尝试把 -R 改为 -Q，观察在 Basics.v 中写 Require Import Basics. 与 Require Import MyProject.Basics. 时哪个能通过编译，并解释原因。

    1
    -R . MyProject

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

参考资料