この論文、参考になる。
- https://kwarc.info/people/frabe/Research/KRW_isabelle_19.pdf
- Making Isabelle Content Accessible in Knowledge Representation Formats
- Michael Kohlhase, Florian Rabe, Makarius Wenzel
日付はハッキリしないが、2020以降なのは確か。FAIR (Findable, Accessible, Interoperable, and Reusable) knowledge exchange format という概念が出てくる。
- ライブラリという概念は直感的にはハッキリしている。ライブラリが膨大だと、ライブラリ検索〈library search〉が大問題になる。
- 証明系のタコツボ状態が、automated proving, library management, user interfaces の重複実装/再実装を招いている。
- ※檜山注釈：user interfaceは、LSPで少し改善されたが、まだまだ。
Isabelleの配布構造は、セッション、セオリー、コマンドから構成される。
- セッションはセオリー〈アーティクル〉の集合。物理的にはディレクトリだろう。PDF文書が含まれてもよい。
- セッションは、1個の親セッションと幾つかのインポート・セッションを持つ。
- セッションはだいたいパッケージかな。パッケージ依存性がインポートセッションか。親セッションという概念がイマイチわからん。
- セオリーが物理的なファイルで、モジュール相当。
- コマンドは、セオリーコンテキスト＝証明状態の状態遷移を引き起こすオペレーター。コマンド実装言語やコマンド・スクリプト言語がある。カートリッジ（カプセル化）により他言語のコマンドを組み込める。
- ロケールが指標相当。
編成・組織化と依存グラフ構造、それとコマンド〈スキルアイテム〉の構造がある。指標の概念がハッキリしてないのがちょっとイヤ。セオリーは指標の上に構築されるはずだから、ベース指標はハッキリすべき。
"the narrative structure addressed to humans" という概念が出てくる。パラグラフとそれが組織化されたセッションで構造化される。
