形式化验证编程语言【免费下载链接】coqThe Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.项目地址https://gitcode.com/gh_mirrors/co/coq点击查看免费下载rocq doc是 Rocq ProverCoq 的继任者自带的文档生成工具功能定位类似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 TextAFT工具主体是普通的 ASCII 文本辅以少量“轻量级”的控制语法下文逐一介绍。官方文档特别强调rocq doc是健壮的robust——无论输入什么它都不应崩溃但同时也提醒“garbage in, garbage out”输入垃圾注释产出的文档自然也是垃圾。从源码看这个“文档状态”与“代码状态”的切换由 tools/coqdoc/cpretty.mll 中的词法规则完成扫描器在行首遇到space* (** (space_nl as s)时调用Output.start_doc ()进入文档模式遇到注释结束再切回代码模式见coq_bol规则第 537542 行。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-printingprinting与remove printingrocq doc对标识符和关键字使用不同的字体face渲染。针对某个 Rocq 词法记号token标识符或符号可以通过以下命令定制其 LaTeX 与 HTML 输出(** printing *token* %...LATEX...% #...html...# *)或数学模式版本(** printing *token* $...LATEX math...$ #...html...# *)其中 LaTeX 规则与 HTML 规则可以省略其一省略的那个输出位置将退回默认排版。删除某个记号的定制规则则用(** remove printing *token* *)默认的排版表中包含如下符号映射LaTeX/HTML 双向Rocq 记号输出Rocq 记号输出-→-←*×≤≥⇒≠-↔|-⊢\/∨/\∧~¬这些默认映射都可以用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统计星号层级第 6876 行。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函数中实现第 2634 行制表符按每 8 列推进。5. 水平分隔线行首超过 4 个破折号----及以上产生一条水平分隔线horizontal rule。6. 强调斜体用下划线_包围文本可将其渲染为斜体。为了避免与标识符中的下划线混淆前导下划线之前、后随下划线之后都必须是非标识符字符通常是空格或标点。示例This sentence contains some _emphasized text_.7. 直接转义到 LaTeX 与 HTML注释中可以插入纯 LaTeX 或纯 HTML 素材使用以下三种转义序列转义序列含义$...LATEX stuff...$插入 LaTeX 数学模式素材在 HTML 输出中被直接丢弃%...LATEX stuff...%插入 LaTeX 素材在 HTML 输出中被直接丢弃#...HTML stuff...#插入 HTML 素材在 LaTeX 输出中被直接丢弃注意如果只是想原样输出字符$、%、#本身而不要其转义语义必须将它们写成双份$$、%%、##。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”信息先用rocq c file.v编译它会自动把定位信息导出到file.glob或者用选项--dump-glob file将信息追加到指定文件。注意开始整批编译前应删除已存在的 glob 文件避免新旧信息混杂。然后调用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” 警告并放弃链接第 4657 行——这正是“记得重新编译生成 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 第 1435 行的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 中有完整的词法定义第 518523 行的begin_hide、end_hide、begin_show、end_show、begin_details、end_details并在coq_bol规则第 549561 行中处理HTML 后端将其渲染为detailssummary结构见 tools/coqdoc/output.ml 第 764768 行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 第 5966 行校验只接受.v、.g、.tex其余后缀直接报错 “Expected a .v, .g, or .tex file”。rocq doc支持五种目标输出格式输出格式说明HTML 输出默认命令行给出的每个 Rocq 文件各生成一个 HTML 文件另生成index.html除非指定--no-index。HTML 页面使用名为style.css的样式表该文件随rocq doc一起分发仓库中即 tools/coqdoc/style.cssLaTeX 输出生成单个 LaTeX 文件输出到标准输出可用-o重定向到文件。命令行中文件的顺序会保留在最终文档中命令行给出的.tex文件会“原样”拷入最终文档。可直接用-dvi与-ps选项生成 DVI 与 PostScriptAlectryon 输出生成单个可被 Alectryon 理解的 Markdown 文件标准输出用-o重定向到文件TeXmacs 输出将输入文件翻译为 TeXmacs 格式供 TeXmacs 的 Rocq 界面使用从源码看输出分发逻辑在 tools/coqdoc/rocqdoc_main.ml 的produce_document中HTML 模式下自动拷贝coqdoc.css、LaTeX 模式下自动拷贝coqdoc.sty第 116118 行并根据out_to是StdOut、File还是MultFiles选择单文件或多文件生成策略第 124133 行。另外命令会先在 stderr 打印版本横幅This is rocq doc version ...因此重定向标准输出时横幅不会混入文档除非同时重定向了 stderr。--dvi、--ps还会触发 tools/coqdoc/latexCompiler.ml 中封装的latex/dvips等外部编译流程。四、命令行选项全表以下选项均为rocq doc实际支持的选项与源码 tools/coqdoc/cmdArgs.ml 中的注册表逐一对应按类别组织。总体选项选项作用--HTML选择 HTML 输出默认格式--latex选择 LaTeX 输出--dvi选择 DVI 输出LaTeX 编译产物--ps选择 PostScript 输出--alectryon选择面向 Alectryon 的 Markdown 输出--texmacs选择 TeXmacs 输出--stdout将输出写到标准输出-o file, --output file将输出重定向到文件file对 HTML 模式无意义因为 HTML 是多文件输出-d dir, --directory dir将输出文件放入目录dir而非当前目录-d不会改变-o指定的文件名--body-only抑制最终文档的头header与尾trailer便于把结果嵌入更大的文档-p string, --preamble string在 LaTeX 导言区\begin{document}之前插入素材对 HTML 模式无意义--vernac-file file/--tex-file file强制将file分别视为.v或.g文件 /.tex文件--files-from file从文件file读取待处理的文件名等价于把它们直接写在命令行上。对源码分散在多个目录的项目很有用-q, --quiet安静模式除错误外不打印任何内容注意--quiet在实现中其实是默认值可用--verbose取消-h, --help打印选项摘要后退出-v, --version打印版本后退出索引选项默认行为是仅对 HTML 输出在index.html中构建索引。选项作用--no-index不输出索引--binder-index把变量 binder 也纳入索引。不推荐用于大型源文件因为 binder 信息可能淹没索引主体--multi-index为索引中每个类别、每个字母各生成一个页面外加顶层页面index.html--index string将索引文件名改为string.html而非index.html后者对 Web 服务器有特殊含义目录Table of Contents选项选项作用-toc, --table-of-contents插入目录。LaTeX 输出时在文档开头插入\tableofcontentsHTML 输出时构建到toc.html--toc-depth int目录只包含不超过int层级的标题超链接选项选项作用--glob-from file使用文件file中的 Rocq 全局化信息该信息由 Rocq 的-dump-glob选项生成来解析引用--no-externals不向 Rocq 标准库插入链接--external url coqdir为名字以coqdir前缀开头的引用使用给定的 URL 作为链接目标--coqlib_url url设置 Rocq 标准库的基础 URL默认值由Coq_config.wwwcorelib给出。等价于--external url Stdlib。注意实现中还保留了别名--corelib_url且--coqlib_url在源码中标注为 deprecated建议使用--corelib_url见 tools/coqdoc/cmdArgs.ml 第 189192 行-R dir coqdir递归地将物理目录dir映射到 Rocq 逻辑目录coqdir与 Rocq 编译器的-R类似-Q dir coqdir将物理目录dir映射到 Rocq 逻辑目录coqdir与-Q类似注意-R与-Q只对命令行中位于它们之后的文件生效所以通常需要把它们放在命令行最前面。这两个选项不仅决定超链接的解析还决定每个文件在文档与索引中的模块名从 tools/coqdoc/cmdArgs.ml 的coq_module函数第 4357 行可以看到若文件处于某个-R/-Q映射的目录范围内模块名会使用逻辑目录名替换物理前缀否则只保留基础文件名。标题选项选项作用-s, --short不为各文件插入标题。默认行为是为每个文件插入类似 “Library Foo” 的标题--lib-name string将标题中的 “Library Foo” 改为 “string Foo”例如 “Chapter”“Module” 都是合理取值--no-lib-name标题只打印 “Foo”去掉 “Library” 前缀--lib-subtitles查找库副标题。启用后每个文件的第一行会被检查是否存在如下形式的注释(** * ModuleName : text *)其中ModuleName必须是文件名若存在则text会作为该模块的副标题出现在合适的位置。对应实现是 tools/coqdoc/rocqdoc_main.ml 中的Cpretty.detect_subtitle第 40、54 行-t string, --title string设置整篇文档的标题内容选项选项作用-g, --gallina不打印证明只保留 Gallina 定义与陈述-l, --light轻量模式除与-g一样抑制证明外还抑制以下命令[Recursive] Tactic Definition、Hint / Hints、Require、Transparent / Opaque、Implicit Argument / Implicits、Section / Variable / Hypothesis / End-g与-l的行为可以被局部的(* begin show *) … (* end show *)环境覆盖见上文。从源码看-l的实现就是gallinatrue加上lighttruetools/coqdoc/cmdArgs.ml 第 133136 行而 light 模式要隐藏的命令列表在 tools/coqdoc/cpretty.mll 第 482511 行的gallina_kw_to_hide正则中给出——包括Implicit Arguments、Arguments、Ltac、Ltac2、From、Require、Import/Export/Load、Hint …、Transparent/Opaque、Section等。此外还有几个控制注释解析的选项选项作用--parse-comments把由(*与*)分隔的普通注释也当作文档解析并内联排版--plain-comments不解释注释直接把它们作为纯文本复制--interpolate利用全局化信息把注释内 Rocq 转义片段中出现的标识符按定义排版即对注释内代码进行交叉引用式渲染语言选项默认假定输入文件是 7 位 ASCII。其余编码相关选项选项作用-latin1, --latin1选择 ISO-8859-1 输入文件等价于--inputenc latin1 --charset iso-8859-1-utf8, --utf8对 LaTeX 输出设置--inputenc utf8x、对 HTML 输出设置--charset utf-8同时把若干标准纯 ASCII 记号替换为 Unicode 符号例如-替换为 →、forall替换为 ∀。注意LaTeX 要正确解释 Unicode 字符可能需要额外安装rocq doc默认不提供的宏包如希腊字母的textgreek、数学符号的stmaryrd若某个 Unicode 字符在 utf8x 输入编码下缺失解释可用\DeclareUnicodeCharacter{code}{LATEX-interpretation}补上。宏包与声明都可以用-p选项加入--inputenc string为 LaTeX 的inputenc宏包指定输入编码--charset string指定写入 HTML 头部的字符集在 tools/coqdoc/cmdArgs.ml 中--utf8会设置charset utf-8与inputenc utf8x--latin1设置charset iso-8859-1与inputenc latin1第 201210 行默认配置的 charset 是iso-8859-1、inputenc 为空tools/coqdoc/common.ml 第 8893 行。五、自定义 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等第 4366 行这些基础宏再由\coqdoclibrary、\coqdocinductive、\coqdocdefinition、\coqdocvariable、\coqdoclemma、\coqdocclass等“真实宏”按类别调用第 7180 行。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 第 765776 行。其中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工作流是在源码中按本文第二节的语法书写(** ... *)特殊注释章节、列表、强调、代码引用、逐字块等用rocq c编译源码生成或更新file.glob确保链接信息与源码一致运行文档生成。例如生成 HTML 并放入doc/目录rocq doc -utf8 -d doc -R . MyLib -t My Library file1.v file2.v其中-R . MyLib需放在文件参数之前只影响其后文件-t设置文档标题-utf8启用 Unicode 符号替换。需要定制输出时组合使用--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——注释写得越规范产出越专业。赞分享形式化验证编程语言【免费下载链接】coqThe Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.项目地址https://gitcode.com/gh_mirrors/co/coq点击查看免费下载相关推荐Nixpkgs 中的 Rocq原 Coq打包与使用完全指南rocq-core、rocqPackages 与 mkRocqDerivationNixpkgs 中的 Rocq原 Coq打包与使用完全指南 rocq core 、 rocqPackages 与 mkRocqDerivation 导读包管理器操作系统CoqRocq Prover官方文档体系解析从 reST 源码到 HTML/PDF/JSON 索引的完整构建指南CoqRocq Prover官方文档体系解析从 reST 源码到 HTML/PDF/JSON 索引的完整构建指南 本指南围绕当前仓库 doc/README形式化验证编程语言姿态估计模型对比为什么rtmw-l-256x192是实时应用的最佳选择姿态估计模型对比为什么rtmw l 256x192是实时应用的最佳选择 在计算机视觉领域姿态估计技术正迅速改变着我们与数字世界的交互方式。 rtmw l创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考