cmd API
cmd 包（Luna-Flow/QED/cmd）是命令行工具 qed-cmd。它读取一个定理脚本文件，用 prover 包检查其中的每个定理，为每个定理打印一份报告，并以状态码退出。它是可执行包（其 moon.pkg 中为 pkgtype(kind: "executable")），因此其他包无法导入它；它的公开函数是该工具的受测接口，在此列出供维护者参考。
cmd 教程逐步介绍该工具；cmd 设计说明解释其输出约定。完整的输出约定也见用户手册。
命令行
qed-cmd
qed-cmd 检查一个定理脚本文件。
qed-cmd [-d] [--no-warn] <file>| 参数 | 含义 |
|---|---|
<file> | 定理脚本文件。定理之间以包含 qed 的行分隔；只含一个定理的文件可以省略它。 |
-d | 在每个已证明定理的名称之后打印其结论。 |
--no-warn | 存在未完成证明但没有错误时以 0 退出。警告仍会打印。 |
在仓库中通过 moon run 运行；工具的参数跟在 -- 之后：
moon run src/cmd examples/truth_file.qed
moon run src/cmd -- -d --no-warn examples/multi_with_hole.qed未知选项、缺少文件参数或多出第二个文件参数时，会打印用法行并以 1 退出。
输出
每个定理按文件顺序产生一个输出块。
| 结果 | 输出 |
|---|---|
| 已证明 | ok <name>，使用 -d 时为 ok <name>: <conclusion> |
| 失败 | error[<kind>] <file> (<name>): <detail>，当失败带有证明上下文时，其后跟 step:、branch:、goal: 和 locals: 行 |
| 未完成 | warning[unfinished] <file> (<name>): <detail>，其后跟 theorem:、step:、branch:、goal:、locals:、hole: 和 message: 行 |
<kind> 为 usage、io、parse、bridge、tactic、sig、logic 之一。分支路径打印为 1.1，空路径打印为 <root>，缺失的值打印为 <none>。目标和局部变量使用内核的结构化项打印器输出。
退出状态
| 状态 | 条件 |
|---|---|
| 0 | 所有定理均已证明，或只有未完成证明且给出了 --no-warn。 |
| 1 | 用法或 I/O 错误、文件无法解析、任何定理失败，或存在未完成证明且未给出 --no-warn。 |
选项
CmdOptions
CmdOptions 保存一次运行的设置：是否安装命题 prelude、是否打印结论，以及仅有警告时是否仍以 0 退出。
pub struct CmdOptions {
auto_install_prelude : Bool
detailed_success : Bool
no_warn : Bool
}default_cmd_options、cmd_options、cmd_options_with_detail 和 cmd_options_full
这些函数用于构造选项。default_cmd_options() 安装 prelude 并关闭两个标志；其余函数分别设置一个、两个或三个字段。
pub fn default_cmd_options() -> CmdOptions
pub fn cmd_options(Bool) -> CmdOptions
pub fn cmd_options_with_detail(Bool, Bool) -> CmdOptions
pub fn cmd_options_full(Bool, Bool, Bool) -> CmdOptions运行
cmd_run_argv
cmd_run_argv(args, opts) 解析命令行（其中 args[0] 是程序名），读取文件并检查。命令行上的标志会覆盖 opts 中对应的字段。
pub fn cmd_run_argv(Array[String], CmdOptions) -> CmdRunResultcmd_run_script
cmd_run_script(path, src, opts) 把源文本 src 当作从 path 读取的内容进行检查，从空的内核状态开始。
pub fn cmd_run_script(String, String, CmdOptions) -> CmdRunResultcmd_render_result 和 cmd_exit_code
cmd_render_result 生成工具打印的文本，cmd_exit_code 生成退出状态，如上所述。
pub fn cmd_render_result(CmdRunResult) -> String
pub fn cmd_exit_code(CmdRunResult) -> Int结果
CmdRunResult
CmdRunResult 是一个结果：对可检查的文件是逐定理的报告，对整个运行则是单个失败（用法、I/O、解析）或未完成结果。
pub enum CmdRunResult {
FileReport(CmdFileReport)
Failure(CmdFailure)
Unfinished(CmdUnfinished)
}CmdFileReport 和 CmdFileItem
文件报告为每个定理列出一项，并记住两个输出标志。
pub struct CmdFileReport {
path : String
items : Array[CmdFileItem]
detailed_success : Bool
no_warn : Bool
}
pub enum CmdFileItem {
CmdItemSuccess(CmdSuccess)
CmdItemFailure(CmdFailure)
CmdItemWarning(CmdUnfinished)
}CmdSuccess
CmdSuccess 是已证明的定理：包含其名称、结论以及渲染后的结论。
pub struct CmdSuccess {
path : String
theorem_name : String
conclusion : @kernel.Term
conclusion_summary : String
}CmdFailure 和 CmdFailureKind
CmdFailure 是失败，其位置和上下文以字符串形式渲染；CmdFailureKind 指明其来源。
pub struct CmdFailure {
path : String
theorem_name : String?
kind : CmdFailureKind
step_index : Int?
branch_path : Array[Int]
current_goal_summary : String?
local_hyps : Array[CmdLocalHypSummary]
detail : String
}
pub enum CmdFailureKind {
Usage
Io
Parse
Bridge
Tactic
Sig
Logic
}cmd_failure_kind_to_string
cmd_failure_kind_to_string 返回打印在 error[...] 内的小写类别名。
pub fn cmd_failure_kind_to_string(CmdFailureKind) -> StringCmdUnfinished、cmd_unfinished 和 cmd_unfinished_from_prover
CmdUnfinished 是未完成证明，其上下文以字符串形式渲染。cmd_unfinished 把它构造成运行结果；cmd_unfinished_from_prover 转换 prover 的报告。
pub struct CmdUnfinished {
path : String
theorem_name : String
step_index : Int?
branch_path : Array[Int]
current_goal_summary : String
local_hyps : Array[CmdLocalHypSummary]
hole_name : String?
detail : String
}
pub fn cmd_unfinished(String, String, Int?, Array[Int], String, Array[CmdLocalHypSummary], String?, String) -> CmdRunResult
pub fn cmd_unfinished_from_prover(String, @prover.ProverUnfinished) -> CmdRunResultCmdLocalHypSummary
CmdLocalHypSummary 是为输出渲染的局部假设，打印为 name: term。
pub struct CmdLocalHypSummary {
name : String
term_summary : String
}