• 形式化验证
• 编程语言

rocq doc是 Rocq Prover（Coq 的继任者）自带的文档生成工具，功能定位类似javadoc与ocamldoc：它从.v/.g源码文件中提取以(**开头的特殊注释，生成面向人类读者而非仅面向证明助手的精美 HTML 或 LaTeX 文档，同时帮助用户快速浏览自己或第三方源码。读完本文，你将掌握rocq doc的注释语法（AFT 风格的轻量标记）、命令行选项全表，以及如何利用.glob全局化信息把源码中的标识符自动链接到其定义处。

本文内容以仓库文档 doc/sphinx/using/tools/coqdoc.rst 为核心骨架，并结合 tools/coqdoc 目录下的源码实现与 test-suite/coqdoc 测试用例进行深化，确保每个语法与选项都有可验证的依据。

一、原理：文档就是特殊注释

rocq doc与许多代码文档工具的关键区别在于：文档以“特殊注释”的形式直接内嵌在 Rocq 源文件中。因此你的文件无论是否使用rocq doc，都能照常编译；rocq doc只要求给定的 Rocq 文件至少是词法上良构的（well-formed）。

特殊注释的起止规则是：

• 以(**开头，其后必须紧跟一个空格；
• 以*)结束。

注释的标记语法借鉴了 Todd A. Coram 的Almost Free Text（AFT）工具：主体是普通的 ASCII 文本，辅以少量“轻量级”的控制语法（下文逐一介绍）。官方文档特别强调rocq doc是健壮的（robust）——无论输入什么它都不应崩溃，但同时也提醒“garbage in, garbage out”：输入垃圾注释，产出的文档自然也是垃圾。

从源码看，这个“文档状态”与“代码状态”的切换由 tools/coqdoc/cpretty.mll 中的词法规则完成：扫描器在行首遇到space* "(**" (space_nl as s)时调用Output.start_doc ()进入文档模式，遇到注释结束再切回代码模式（见coq_bol规则，第 537～542 行）。rocq doc对源码本身的词法分析基于 OCaml 的 lex 自动机，因此识别规则（如最长匹配）也继承自经典 lex 语义。

二、注释内的标记语法

1. 引用 Rocq 代码：[...]与[[...]]

在文档注释内，Rocq 代码片段用方括号[与]括起来引用。方括号可以嵌套，内层的方括号会被理解为被引用代码的一部分，例如要引用一个包含显式类型参数的项：

[let id := fun [T : Type] (x : t) => x in id 0]

这里[T : Type]中的内层方括号不会被误解为引用结束。被引用的代码在输出时会像普通代码部分一样进行 pretty-printing（语法高亮与换行缩进）。

如果需要引用整段的预格式化（preformatted）白话（vernacular）代码，则使用[[与]]包裹：

• [[之后必须紧跟一个换行；
• ]]之前必须是一个换行。

2. 控制 pretty-printing：printing与remove printing

rocq doc对标识符和关键字使用不同的字体（face）渲染。针对某个 Rocq 词法记号（token，标识符或符号），可以通过以下命令定制其 LaTeX 与 HTML 输出：

(** printing *token* %...LATEX...% #...html...# *)

或数学模式版本：

(** printing *token* $...LATEX math...$ #...html...# *)

其中 LaTeX 规则与 HTML 规则可以省略其一，省略的那个输出位置将退回默认排版。删除某个记号的定制规则则用：

(** remove printing *token* *)

默认的排版表中包含如下符号映射（LaTeX/HTML 双向）：

这些默认映射都可以用printing命令覆盖，或用remove printing抑制。

注意（最长匹配规则）：记号的识别由一个 OCaml lex 自动机完成，遵循最长匹配（longest-match）原则。例如输入->~会被整体识别为一个记号，而 Rocq 编译器会将其视为->与~两个记号。因此用户要么自己负责在记号间插入空格，要么为这类组合显式给出排版规则，例如：

(** printing ->~ %\ensuremath{\rightarrow\lnot}% *)

3. 章节标题

用 1 到 4 个星号加一个空格、再加标题文字，置于行首即可生成章节标题。一个星号是一级标题（section），两个是二级（subsection），依此类推。示例：

(** * Well-founded relations In this section, we introduce... *)

在源码中，这一语法由 tools/coqdoc/cpretty.mll 的正则let section = "*" | "**" | "***" | "****"识别（第 514 行），并调用sec_title统计星号层级（第 68～76 行）。

4. 列表

列表项以行首的破折号（dash，-）引入。rocq doc依靠空白（缩进）来判断列表项的层级以及哪些文本属于哪个列表项：

• 当一行文本起始列位于或早于列表破折号的缩进层级时，该列表结束；
• 列表项的破折号必须是所在行的第一个非空格字符；
• 特别地，列表不能从注释的第一行开始——请从注释的第二行开始写列表。

示例（注意缩进决定了两层列表与段落归属）：

We go by induction on [n]: - If [n] is 0... - If [n] is [S n'] we require... two paragraphs of reasoning, and two subcases: - In the first case... - In the second case... So the theorem holds.

这里的缩进计算在 tools/coqdoc/cpretty.mll 的count_spaces函数中实现（第 26～34 行），制表符按每 8 列推进。

5. 水平分隔线

行首超过 4 个破折号（----及以上）产生一条水平分隔线（horizontal rule）。

6. 强调（斜体）

用下划线_包围文本可将其渲染为斜体。为了避免与标识符中的下划线混淆，前导下划线之前、后随下划线之后都必须是非标识符字符（通常是空格或标点）。示例：

This sentence contains some _emphasized text_.

7. 直接转义到 LaTeX 与 HTML

注释中可以插入纯 LaTeX 或纯 HTML 素材，使用以下三种转义序列：

注意：如果只是想原样输出字符$、%、#本身而不要其转义语义，必须将它们写成双份（$$、%%、##）。

8. 逐字文本（Verbatim）

逐字文本（不做任何解释、原样呈现）由行首的<<引入、由行首的>>结束：

Here is the corresponding caml code: << let rec fact n = if n <= 1 then 1 else n * fact (n-1) >>

单行逐字文本也是允许的（只要该行文本中不包含>>）：

Here is the corresponding caml expression: << fact (n-1) >>

测试用例 test-suite/coqdoc/verbatim.v 覆盖了多行、单行、以及逐字块与列表、[[...]]白话块混排等边界情形。

9. 超链接与.glob全局化文件

HTML 输出可以自动插入超链接，使任何一个标识符都链接到它被定义的位置。这依赖“全局化（globalization）”信息：

1. 先用rocq c file.v编译，它会自动把定位信息导出到file.glob；或者用选项--dump-glob file将信息追加到指定文件。注意：开始整批编译前，应删除已存在的 glob 文件，避免新旧信息混杂。
2. 然后调用rocq doc（或rocq doc --glob-from file）告诉工具从指定文件读取名称解析信息；默认情况下它会自动查找file.glob。

从实现看，rocq doc默认的 glob 来源是DotGlob（自动为每个输入.v文件读取同名.glob），这一定义在 tools/coqdoc/common.ml 第 16 行与第 82 行（glob_source = DotGlob）。读取逻辑在 tools/coqdoc/glob_file.ml 中：它还会校验.glob文件头部的DIGEST摘要与对应.v文件是否一致，不一致时给出 “not consistent with corresponding .v file” 警告并放弃链接（第 46～57 行）——这正是“记得重新编译生成 glob”的底层原因。

标准库中的标识符默认链接到 Rocq 标准库在线文档（默认基地址由Coq_config.wwwcorelib给出），该行为可通过--no-externals与--coqlib_url等命令行选项改变（详见下文“超链接选项”）。需要注意的是，.glob中定义的多种对象类型（def、thm、ind、constr、not、mod、binder等）会在索引中被分类为Definition、Lemma、Inductive、Constructor、Notation、Module、Binder等条目（见 tools/coqdoc/glob_file.ml 第 14～35 行的type_of_string映射）。

10. 隐藏 / 显示源码的指定部分

rocq doc支持用命令行选项-g与-l整体隐藏证明（详见下文“内容选项”），也支持在源码中用注释对局部区域进行更精细的控制：

隐藏一段源码（配合-g/-l之外也可以单独使用）：

(* begin hide *) *some Rocq material* (* end hide *)

反之，显示默认会被隐藏的内容（例如在-g或-l模式下强制展示某段）：

(* begin show *) *some Rocq material* (* end show *)

后者不能用于某个证明的内部（证明中间），但可以包围整个证明。

折叠（details）：当目标输出为 HTML 时，还有一种折中方案——某段 Rocq 素材默认隐藏，但用户可以通过交互展开：

(* begin details *) *some Rocq material* (* end details *)

还支持带摘要的替代语法（摘要会显示在折叠区标题处）：

(* begin details : Some summary describing the snippet *) *some Rocq material* (* end details *)

这些指令在 tools/coqdoc/cpretty.mll 中有完整的词法定义（第 518～523 行的begin_hide、end_hide、begin_show、end_show、begin_details、end_details），并在coq_bol规则（第 549～561 行）中处理；HTML 后端将其渲染为<details><summary>结构（见 tools/coqdoc/output.ml 第 764～768 行），LaTeX 等其他后端则将其视为无操作。测试用例 test-suite/coqdoc/details.v 及对应期望输出 test-suite/coqdoc/details.html.out 验证了带/不带摘要两种形式的行为。

三、命令行用法与输出格式

rocq doc在 shell 中这样调用：

rocq doc <options and files>

规则要点：

• 任何不是选项的命令行参数都被视为文件名（即使它以-开头）；
• .v与.g后缀的文件被识别为 Rocq 文件，.tex后缀被识别为 LaTeX 文件；
• 非选项参数会被what_file（见 tools/coqdoc/cmdArgs.ml 第 59～66 行）校验：只接受.v、.g、.tex，其余后缀直接报错 “Expected a .v, .g, or .tex file”。

rocq doc支持五种目标输出格式：

从源码看，输出分发逻辑在 tools/coqdoc/rocqdoc_main.ml 的produce_document中：HTML 模式下自动拷贝coqdoc.css、LaTeX 模式下自动拷贝coqdoc.sty（第 116～118 行），并根据out_to是StdOut、File还是MultFiles选择单文件或多文件生成策略（第 124～133 行）。另外，命令会先在 stderr 打印版本横幅（This is rocq doc version ...），因此重定向标准输出时横幅不会混入文档（除非同时重定向了 stderr）。--dvi、--ps还会触发 tools/coqdoc/latexCompiler.ml 中封装的latex/dvips等外部编译流程。

四、命令行选项全表

以下选项均为rocq doc实际支持的选项（与源码 tools/coqdoc/cmdArgs.ml 中的注册表逐一对应），按类别组织。

总体选项

索引选项

默认行为是：仅对 HTML 输出在index.html中构建索引。

目录（Table of Contents）选项

超链接选项

注意：-R与-Q只对命令行中位于它们之后的文件生效，所以通常需要把它们放在命令行最前面。这两个选项不仅决定超链接的解析，还决定每个文件在文档与索引中的模块名：从 tools/coqdoc/cmdArgs.ml 的coq_module函数（第 43～57 行）可以看到，若文件处于某个-R/-Q映射的目录范围内，模块名会使用逻辑目录名替换物理前缀，否则只保留基础文件名。

标题选项

内容选项

-g与-l的行为可以被局部的(* begin show *) … (* end show *)环境覆盖（见上文）。从源码看，-l的实现就是gallina=true加上light=true（tools/coqdoc/cmdArgs.ml 第 133～136 行），而 light 模式要隐藏的命令列表在 tools/coqdoc/cpretty.mll 第 482～511 行的gallina_kw_to_hide正则中给出——包括Implicit Arguments、Arguments、Ltac、Ltac2、From、Require、Import/Export/Load、Hint …、Transparent/Opaque、Section等。此外还有几个控制注释解析的选项：

语言选项

默认假定输入文件是 7 位 ASCII。其余编码相关选项：

在 tools/coqdoc/cmdArgs.ml 中，--utf8会设置charset = "utf-8"与inputenc = "utf8x"，--latin1设置charset = "iso-8859-1"与inputenc = "latin1"（第 201～210 行）；默认配置的 charset 是iso-8859-1、inputenc 为空（tools/coqdoc/common.ml 第 88～93 行）。

五、自定义 HTML 头与尾

在 HTML 模式下，可以用--with-header与--with-footer分别让rocq doc在文件开头包含一个头文件、在文件末尾包含一个尾文件。此外，头文件中出现的字符串@@TITLE@@会被替换为页面标题。

六、rocq doc的 LaTeX 样式文件：coqdoc.sty

如果你选择不使用默认 LaTeX 导言区（选项--no-preamble）来生成文档，则必须在自己的导言区中手工插入：

\usepackage{coqdoc}

该宏包可选参数[color]：启用后标识符将以彩色排版（需要xcolor宏包）。仓库中随rocq doc分发的样式文件正是 tools/coqdoc/coqdoc.sty。

随后你可以通过重定义若干宏来调整文档渲染效果：

• coqdockw、coqdocid等单参数宏：用于排版本关键字与标识符。默认关键字为无衬线字体、标识符为斜体。例如想让关键字使用倾斜字体，在\usepackage{coqdoc}与\begin{document}之间任意位置插入：

  \renewcommand{\coqdockw}[1]{\textsl{#1}}

  从 tools/coqdoc/coqdoc.sty 可以看到，默认定义按对象类型细分：关键字\coqdockw用\texttt、变量\coqdocvar用\textit、常量\coqdoccst用\textsf、归纳类型\coqdocind用\textbf{\textsf}、构造子用\textsf、tactic 用\texttt等（第 43～66 行），这些基础宏再由\coqdoclibrary、\coqdocinductive、\coqdocdefinition、\coqdocvariable、\coqdoclemma、\coqdocclass等“真实宏”按类别调用（第 71～80 行）。

• coqdocmodule：用于排版.v文件标题的单参数宏，默认定义为：

  \newcommand{\coqdocmodule}[1]{\section*{Module #1}}

  可用\renewcommand重定义。

七、测试与集成佐证

rocq doc在仓库中有完整的回归测试，位于 test-suite/coqdoc 目录（包含Context.v、Record.v、binder.v、details.v、links.v、verbatim.v等用例），并通过 test-suite/Makefile 中的coqdoc目标批量验证：先以-R coqdoc Coqdoc编译生成.glob，再分别用--html、--latex、--alectryon三种后端输出并与期望文件比对（见 test-suite/Makefile 第 765～776 行）。其中：

• test-suite/coqdoc/details.v 验证begin details/end details（含: summary形式）的折叠渲染；
• test-suite/coqdoc/links.v 验证不同符号记号的链接解析、-utf8下forall的 Unicode 替换以及字符串中符号不被错误替换等细节；
• test-suite/coqdoc/Context.v 验证Section/Context/End这类轻量模式应隐藏命令的处理。

对于使用coq_makefile构建的项目，rocqdoc目标会自动调用文档生成并把样式表拷入输出目录（参见 tools/CoqMakefile.in 与 test-suite/coq-makefile/coqdoc1/run.sh、test-suite/coq-makefile/coqdoc2/run.sh 中检查test/html/coqdoc.css的断言）。

八、一个完整的实战流程

综合以上内容，一个典型的rocq doc工作流是：

1. 在源码中按本文第二节的语法书写(** ... *)特殊注释（章节、列表、强调、代码引用、逐字块等）；

2. 用rocq c编译源码生成（或更新）file.glob，确保链接信息与源码一致；

3. 运行文档生成。例如生成 HTML 并放入doc/目录：

   rocq doc -utf8 -d doc -R . MyLib -t "My Library" file1.v file2.v

   其中-R . MyLib需放在文件参数之前（只影响其后文件），-t设置文档标题，-utf8启用 Unicode 符号替换。

4. 需要定制输出时组合使用：--no-index/--multi-index/--index控制索引形态，-toc/--toc-depth控制目录，--body-only嵌入更大的文档，--with-header/--with-footer定制 HTML 页面外壳，-p注入 LaTeX 导言区素材，--lib-subtitles启用模块副标题，-g/-l控制证明与辅助命令的显隐，局部再辅以begin hide/show/details注释做精细调节。

至此，你可以用rocq doc把 Rocq 源码变成一套自带交叉索引、可在线阅读、也可嵌入论文与书籍的正式文档；garbage in, garbage out——注释写得越规范，产出越专业。

• 形式化验证
• 编程语言