cmd の設計

cmd パッケージは QED の最も外側の層であり、prover の上に載ったファースト・ファイルのコマンドラインツールである。このページでは、なぜ意図的に薄くしているのか、prover の結果をどのようにテキストと終了コードに対応づけるのか、そして何を決してしてはならないのかを説明する。

設計目標

一つのコマンドで定理スクリプトのファイルを検査し、すべての定理を報告する。
人が対処でき、スクリプトが解析できる診断を出力する。定理ごとに固定された先頭行と、ラベル付きのコンテキスト行を出す。
ビルドシステムが利用できる状態で終了し、開発中は未完了の証明を許容する手段を備える。
prover が報告する以上の、論理、項、タクティクに関する知識を加えない。

数学的背景

このツールは、ファイルから結果のリストと状態への関数を計算する。ファイルの各定理の結果を $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 を返す。

設計判断

ファイルファースト

問題。 定理証明器の CLI は、REPL にも、単一ゴールの検査器にも、ファイル検査器にもなりうる。

選択。 qed-cmd はちょうど一つのファイルを受け取る。定理は qed 行で区切られ、プレリュードをインストールした空のカーネル状態から、それぞれ独立に検査される。

理由。 ユーザーが編集し、バージョン管理し、CI に渡すのはファイルである。各定理を同じ初期状態から検査することで、結果は順序に依存せず、ファイル内の定理が互いを引用できないという prover の規則とも合致する。

規則による薄さ

問題。 CLI は論理を蓄積しがちである。特殊なケース、ゴールの独自のパース、独自の成功の概念などである。

選択。 このツールは、引数をパースし、ファイルを読み、prove_theorem_file_results_detailed を呼び、結果を文字列に変換し、終了状態を計算するだけである。コードガバナンスはこれを規則としている。cmd は最も薄い層であり、安定した prover ファサードのみを利用する。

理由。 ツールが出力する主張はすべて prover に由来する。そのため prover のテストとコーパスがそれらをカバーし、ツールが意味論の異なる第二の証明エンジンになることはない。

安定したテキスト、構造化が先

問題。 出力は人にもツールにも役立たなければならない。

選択。 各定理は、ok …、error[kind] …、warning[unfinished] … のいずれかの一行で始まる。コンテキストはラベル付きの行（step:、branch:、goal:、locals:、hole:、message:）で続き、値がない場合は固定のマーカー <none> と <root> を使う。結果は構造化された値（CmdRunResult）として構築され、一つの関数で描画される。

理由。 固定された先頭行は grep しやすい。ラベル付きの行は読みやすく解析しやすい。描画の前に値を構築することで、テストは構造とテキストを別々に検査できる。ゴールとローカルはカーネルの構造プリンタで描画されるため、冗長にはなるが、カーネルが見たとおりの項がそのままテキストに現れる。

警告は成功ではない

未完了の証明は警告であり、ok ではない。既定では実行が失敗となるため、CI は hole を含むファイルを受け入れない。--no-warn は作業途中のために存在する。これは終了状態だけを変え、出力は決して変えないので、hole は見えたままである。

正しさと不変条件

権限を持たない。 このパッケージは定理を構築せず、カーネル規則も呼ばない。ok はカーネル定理を伴う ProverItemProved 項目に対してのみ出力される。
報告の完全性。 パース可能なファイルのすべての定理は、ファイル順にちょうど一つのブロックを生成する。
終了状態 は上記の式に従う。cmd_exit_code がその実装であり、cmd_wbtest.mbt でカバーされている。
位置。 ステップ番号と分岐パスは prover のものであり、ソースやライブラリ利用と一致する。

却下した代替案

最初のエラーで停止する。 速くはなるが、ユーザーはエラーごとに修正と再実行を一回ずつ行わなければならなくなる。
--no-warn で警告を隠す。 出力を消すフラグでは、hole が見過ごされかねない。
項を表面構文で整形表示する。 ∧ や -> を再導入するプリンタは、エンコーディングの第二の解釈となり、パーサとずれうる。構造プリンタにはそのような危険がない。

境界

一回の実行につきファイルは一つ。ディレクトリ、ファイル間のインポート、ウォッチモードはない。
REPL もエディタプロトコルもない。
-d と --no-warn 以外のオプションはない。プレリュードは常にインストールされる。
ライブラリとしての利用はできない。このパッケージは実行ファイルであり、インポートできない。ライブラリ利用者は prover を直接呼ぶ。