論理資源管理
ざっと調べたが、雑でイイカゲンで未完成である。
一般的な概念
- モジュールとパッケージ：モジュールを集めてパッケージ
- パッケージマネージャ
- グローバルインストールとローカルインストール
- プロジェクト： 作業をするための環境
- パッケージのメタ情報
- パッケージのパブリッシュまたはアドバタイズ：公開する／投稿する
- パッケージのバージョニング
- ユーザー＝オーサーのメタ情報
Mizar
- 基本単位は Mizar article
- ローカルでの場所は $MIZAR_HOME/mml/
- 「.mizファイル＝article＝記事」で、すべての記事がフラットに配置される。
- 記事名はなんと8文字まで。アホか！
- 依存関係は、記事のenvironとbeginの間に書く。
- environ部の記述は異常に分かりにくい。超難解。クソ。
- article構文は http://www.mizar.org/language/mizar-grammar.xml#Article
- コンパイルされた記事は $MIZAR_HOME/prel/ の下に独自形式で格納。
- 記事の管理は中央集権方式
- 野良記事は認めない。
- articleの内容：definition, theorem, scheme, notation, ...
- .mizソースコードから自動的にPDFが生成されるようだが、ツールは非公開。
- 雑誌"Formalized Mathematics"は年4回出版。Volumeが単位で、Volumeは記事の集合。
- 過去に"Formalized Mathematics"に載った記事はすべてMMLに入るので、中央集権的に単調にMMLは膨張する。
- MMLは、特定時点（特定バージョン）では唯一の存在で、その信頼性や有意義性は委員会方式で担保される。
- ある意味、単純明快であるが、メカニズムは最悪。
Isabelle
- ライブラリのトップレベルの文書的単位はチャプター、物理的にはディレクトリ。
- チャプターディレクトリは $ISABELLE_HOME/src/ の直下に全て大文字の名前。ただし、$ISABELLE_HOME/src/ には、プログラムソースも一緒くたになっている。
- チャプターのメタデータは $chapter/ROOT というテキストファイル
- チャプターの下にファイルやディレクトリを作れる。
- チャプターやそのサブディレクトリの文書テンプレートと参考文献データは ./document/ に置く。ROOTを持つのはchapterだけ。
- 「.thyファイル＝セオリー」は、ライブラリルート（$ISABELLE_HOME/src/）からの相対パスで識別する。
- 文書構造としては、チャプターの下はセクション
- 物理的なディレクトリを論理構造としてはセッションと呼ぶ。
- セッションにオーナーシップがある。この意味でセッションはパッケージ。
- セッションの階層構造を許す。セッションの子はセッションでもセオリーでもよい。
- セッションはセオリーを含む。
- セオリーごとにタイトルと著者と著作権を持ってもよい。
- セオリーは依存関係を持つ。importsで依存関係を示す。
- セッション／セオリー構造はファイルシステムと同じで、ファイルシステムにそのままマップされる。セッション→ディレクトリ、セオリー→.thyファイル。
Coq
また後日。
