.olean と .ilean

モジュールをビルドすると，Lean は処理済みの環境情報を .olean ファイルに保存します． import されたモジュールを毎回ソースからエラボレートし直すのではなく，.olean を読み込むことで高速に再利用します． この保存が，上のパイプラインでいう serialization です． 保存されるのはソースコードのコピーではなく，カーネル検査済みの宣言，module の環境情報，import に必要な情報などです．

このプロジェクトの Lean 4.30.0 では，言語サーバー用の索引として .ilean も生成されます． これは補完，ジャンプ，情報表示などのためのデータです． 一方，Reference 最新版の module system の説明では，環境は public，private，server 情報に分けて .olean として保存される，と説明されています． つまり，正確なファイル名や分割方法は Lean のバージョンや module system の利用状況に依存します． 授業では「.olean は import される検査済み環境，language server 用の情報は対話機能のための補助データ」と押さえれば十分です． .ilean などの中身は実装詳細なので，通常の開発では直接読む対象ではありません．

このプロジェクトで lake build を実行すると，典型的には次のようなファイルができます．

.lake/build/lib/lean/LeanMathNote.olean
.lake/build/lib/lean/LeanMathNote.ilean
.lake/build/lib/lean/LeanMathNote/basic/chapter06.olean
.lake/build/lib/lean/LeanMathNote/basic/chapter06.ilean
.lake/build/lib/lean/LeanMathNote/practice/chapter01.olean
.lake/build/lib/lean/LeanMathNote/practice/chapter01.ilean

この章のように LeanMathNote/basic/chapter06.lean を単体で lake env lean した場合は， チェックは行われますが，Lake の通常ビルド対象に入っていなければ .olean は残らないことがあります．