コードのガバナンス
- ステータス：active
- 対象読者：コントリビューター、メンテナー
- 権威：リポジトリのコード構成方針。QED 形式仕様、現在のコード／テスト、ドキュメントのガバナンスに従属する
- 範囲：パッケージの階層化、alias エントリーポイント、ソースの責務、コード変更時のドキュメント更新義務
- 最終レビュー: 2026-10-08
本書は QED リポジトリのコードガバナンス規則を定める。新たな意味論的仕様の層は追加せず、パッケージ境界、エイリアスのエントリポイント、ドキュメントへの書き戻し義務のみを固定することで、コード構造が時間とともに逸脱しないようにする。
階層構造
既定の依存方向は次のように固定される。
kernel -> logic/elab -> parser -> tactics -> prover -> cmd
ガバナンス要件:
kernelは定理構築の唯一の境界である。logicが提供してよいのは、検査済みヘルパー、定義/展開、リプレイヘルパー、定理カタログの整理のみであり、新たな基本権限を追加してはならない。parserが担うのはテキスト構文、正規化、解決、ローワリングのみであり、タクティクの実行オブジェクトに直接依存してはならない。tacticsが担うのはゴール状態の変換とリプレイの編成のみであり、parser の意味論へ書き戻してはならない。proverは parser/tactics/kernel の編成と構造化診断の生成のみを行い、新たな論理的権限になってはならない。cmdは最も薄い最外層にとどまり、安定したファサードを利用するだけで、低レベルの知識を追加しない。
research_rewrite はこの連鎖の外にある。研究専用のプロトタイプであり、依存先は kernel と logic のみで、出荷対象のパッケージはこれに依存しない。cmd は実行可能パッケージ(moon.pkg 内の pkgtype(kind: "executable"))であるため、他のパッケージからインポートすることはできない。
変更によって逆方向の依存が必要になる場合は、既定で設計上の問題として扱う。層をまたぐ直接参照よりも、中立的なデータ構造や明示的なブリッジの導入を優先する。
alias エントリーポイント
各パッケージには、公式のエイリアスエントリポイントがちょうど 2 種類ある。
alias.mbt本番ソースのエントリポイント。alias_test.mbtブラックボックステストのエントリポイント。
制約は次のとおり。
alias.mbtが公開するのは、パッケージの本番ソースが実際に必要とする安定したシンボルのみである。alias_test.mbtは、まずalias.mbtの本番エクスポートを写し、その後にテスト専用のインポートを加えなければならない。alias_test.mbtは第二の公開 API ではなく、本番エントリポイントと異なるエクスポート方針に従ってはならない。- エイリアスファイルのヘッダコメントには、エントリポイントの適用範囲と保守規則を明記しなければならない。
- エイリアスファイルを、下位層のシンボルを無制限に再エクスポートする表として使ってはならない。
- ブラックボックステストが自パッケージのシンボルを参照する場合、
alias_test.mbtでusing @<package> {...}により明示的にインポートしなければならない(MoonBit のtest_unqualified_package規則)。テストは暗黙のインポートに依存してはならない。 kernelは他の QED パッケージに依存しないためalias.mbtを持たず、テストが使うパッケージのシンボルを列挙するalias_test.mbtのみを持つ。
ソースの責務
単一のファイルまたはモジュールは、可能な限り一つの主要な責務のみを担うべきである。
- 純粋なデータオブジェクトとアクセサ
- 純粋なローワリング / 正規化 / レンダリング
- リプレイ / 編成
- コーパス / マッピング / フィクスチャ
次の場合は優先的に分割すべきである。
- 編成ロジックとエラーのレンダリングが長期にわたって同一ファイルに混在している
- parser 側のローワリングがタクティクオブジェクトを直接構築している
- ファサード層のファイルが、層をまたぐ何でも屋のエントリポイントへと次第に変質している
現在このリポジトリに導入されている最初のガバナンスパターンには、次のものがある。
- parser は parser 所有の
ParsedGoalを出力し、上位層がそれをtactics.Goalへ明示的にブリッジする - prover は編成の役割を保ちつつ、診断のレンダリングとコーパスデータを主実行経路から分離し続ける
ドキュメントの義務
コードの変更が次のいずれかに影響する場合は、ドキュメントも同時に更新しなければならない。
- 公開されている機能の主張
- パッケージの責務または階層の境界
- エイリアスエントリポイントの意味論
- 失敗の意味論または構造化診断のフィールド
既定の保守順序:
- コードとテスト
- ユーザーマニュアル
- 影響を受けるパッケージのパッケージページ(
api/、design/、tutorial/) - 仕様適合性
README.mdとCHANGELOG.md- ワークスペース監査(2026-04-18)(特定時点の結論が変わる場合のみ)
レビューチェックリスト
提出およびレビューの際には、少なくとも次を確認する。
- 新たな依存が確立された階層構造に従っているか
alias.mbt/alias_test.mbtが引き続き唯一の公式エントリポイントであるか- parser/tactics/prover の責務が再び結合されていないか
.mbtiの変更が意図した公開境界と一致しているか- ドキュメントが新たな出荷状態を同時に反映しているか