付録E 実行・検証の手引き
「動かない」を一つの問題として扱わず、何を確認するコマンドなのかと、どの段階で失敗したのかを分けます。検査の緑色の表示だけで、目的の振る舞いまで保証されたとは判断しません。
E.1 目的からコマンドを選ぶ
| 目的 | 入口 | 成功しても別に残る確認 |
|---|---|---|
| 型・効果・所有権と証明を検査 | tauto check FILE | 実際の入出力、外部コード、対象バックエンドでの実行 |
| 残っている証明を知る | tauto goals FILE | 各穴を埋め、ファイル全体を再検査する |
| 穴に入れる候補を検査 | tauto try FILE --hole NAME --with 'TERM' | 候補以外の穴や宣言が完成したか |
| 検査した候補を書き込む | tauto fill FILE --hole NAME --with 'TERM' | 書き込み後の差分と再検査。fill はファイルを変更する |
| 実際の結果を確認 | tauto run --tote . | 他の入力やエラー経路の期待値 |
| テストを実行 | tauto test . | 未記載のケース、一般的な性質、別バックエンド |
| 名前や定理を調べる | tauto library FILE | 呼び出しに必要な型や仮定が満たされるか |
| コードを整形 | tauto fmt FILE | 型の正しさやプログラムの意味。整形は検証ではない |
各コマンドの詳細は第12章で説明します。実行やテストは外部コードを動かすことがあります。信頼できないソースを、安全なサンドボックスだと考えて実行しないでください。
E.2 失敗を切り分ける順序
- 構文と名前：最初の診断から確認します。後続の型エラーは、先行する構文エラーや名前解決の失敗による可能性があります。ファイル名と import を掲載例と照合します。
- 型・使用規則・効果：型の不一致、移動後の使用、借用、未処理の効果を区別します。診断を消すために公理や外部関数へ置き換えないでください。
- 証明：穴があれば goals を確認し、仮定と結論を書き出します。
Reflで通らなければ、両辺が計算で一致するか、それとも等式の証明が必要かを確認します。 - 実行：検査が通った最小例で、入力、期待する出力、実測した出力を分けます。
showに出た文字列だけではアサーションになりません。 - バックエンドとホスト：同じソースで実行対象を変えた場合は、それぞれのビルド・実行結果を記録します。一方の成功だけで他方を成功扱いしません。
E.3 最小再現に残すもの
- CLI のバージョンと、使ったコマンド全体。
- 単独で失敗するソース、必要な import、マニフェスト。秘密鍵や業務データは含めない。
- 期待した結果、実際の診断や出力、終了コード。
- バックエンドと実行ホスト、外部関数やホスト権限が必要か。
check・テスト・ビルド・実行のうち、成功した段階、失敗した段階、未実施の段階。
型名の解決失敗と、それに続く戻り値の不一致など、異なる段階の診断が同時に出ることがあります。後の診断を独立した不具合だと決めつけず、先の失敗を取り除いた例でも再現するかを確かめます。
E.4 検査記録と実測の違い
本の例にはビルド時の検査記録を付けます。本文・期待する診断・CLI と検査記録が一致しない場合、サイト生成では再検査が必要です。古い成功表示を新しいコードの検証結果として扱いません。
これは読者の環境での成功や全バックエンドの同等性を意味しません。また、axiom に依存する証明は、その仮定の下での証明です。何を信頼するかは第20章を参照してください。