cmd 设计说明

cmd 包是 QED 的最外层：一个基于 prover 的、以文件为先的命令行工具。本页解释它为何刻意保持精简、如何把 prover 的结果映射为文本和退出码，以及它绝不能做什么。

设计目标

用一条命令检查一个定理脚本文件，并报告每个定理。
打印人可据以行动、脚本可解析的诊断：每个定理有固定的第一行，以及带标签的上下文行。
以构建系统可用的状态退出，并提供在开发期间容忍未完成证明的方式。
除 prover 所报告的内容外，不增加任何关于逻辑、项或策略（tactic）的知识。

数学背景

该工具计算一个从文件到结果列表和状态的函数。把文件中各定理的结果记为 $o_1, \dots, o_n$ ，每个都属于 $\{\mathsf{ok}, \mathsf{err}, \mathsf{warn}\}$ ，则退出状态为

\mathsf{exit}(o_1, \dots, o_n) = \begin{cases} 1 & \text{if some } o_i = \mathsf{err} \\ 1 & \text{if some } o_i = \mathsf{warn} \text{ and } \texttt{--no-warn} \text{ is not given} \\ 0 & \text{otherwise.} \end{cases}

该状态是单调的：向文件中添加失败的定理只会使其升高，而 --no-warn 只会降低由警告引起的状态。用法错误、不可读的文件或无法解析的文件给出 1，且没有任何逐定理的结果。

设计决策

以文件为先

问题。 定理证明器的命令行可以是 REPL、单目标检查器或文件检查器。

选择。 qed-cmd 恰好接受一个文件。各定理由 qed 行分隔，并从安装了 prelude 的空内核状态开始独立检查。

原因。 文件是用户编辑、做版本管理并交给 CI 的对象。每个定理都从同一初始状态开始检查，使结果与顺序无关，这与 prover 的规则一致：同一文件中的定理不能互相引用。

规则上保持精简

问题。 命令行工具往往会积累逻辑：特例、自己对目标的解析、自己对成功的理解。

选择。 该工具只解析参数、读取文件、调用 prove_theorem_file_results_detailed、把结果转换为字符串并计算退出状态。代码治理把这定为规则：cmd 是最薄的一层，只使用稳定的 prover 门面。

原因。 工具打印的每一项断言都来自 prover，因此 prover 的测试和语料（corpus）覆盖了它，工具也不会变成语义不同的第二个证明引擎。

稳定的文本，结构化优先

问题。 输出必须同时服务于人和工具。

选择。 每个定理以一行 ok …、error[kind] … 或 warning[unfinished] … 开头。上下文随后以带标签的行给出（step:、branch:、goal:、locals:、hole:、message:），缺失的值使用固定标记 <none> 和 <root>。结果先构建为结构化的值（CmdRunResult），再在一个函数中渲染。

原因。 固定的第一行便于 grep；带标签的行便于阅读和解析；先构建值再渲染，使测试可以分别检查结构和文本。目标和局部假设用内核的结构化打印器渲染，因此文本恰好显示内核所见的项，代价是比较冗长。

警告不是成功

未完成的证明是警告，不是 ok。默认情况下它会使运行失败，因此 CI 不会接受含有 hole 的文件。--no-warn 用于开发中的工作：它只改变退出状态，从不改变输出，所以 hole 仍然可见。

正确性与不变量

无权威性。 该包不构造定理，也不调用内核规则；只有对携带内核定理的 ProverItemProved 项才会打印 ok。
报告的完整性。 可解析文件中的每个定理恰好产生一个块，并按文件顺序排列。
退出状态遵循上述公式；cmd_exit_code 是其实现，并由 cmd_wbtest.mbt 覆盖。
位置。 步骤编号和分支路径来自 prover，因此与源文件及库的使用方式一致。

被否决的替代方案

在第一个错误处停止。 更快，但用户每个错误都得修复并重新运行一次。
用 --no-warn 隐藏警告。 会删除输出的标志会让 hole 被忽略。
用表面语法美化打印项。 重新引入 ∧ 和 -> 的打印器会成为对编码的第二种解释，可能与解析器出现偏差；结构化打印器没有这种风险。

边界

每次运行一个文件；不支持目录，不支持文件间导入，没有监视模式。
没有 REPL，也没有编辑器协议。
除 -d 和 --no-warn 外没有其他选项；prelude 始终被安装。
不支持作为库使用：该包是可执行文件，不能被导入。库的使用者应直接调用 prover。