lake のパッケージの置き方

Lean4 では lake コマンドを使用してプロジェクトを作成する、作成したプロジェクトでパッケージの整理をする際に、少し詰まったのでメモしておく。結論はプロジェクト名のディレクトリを作成してそこにファイルを作るとインポートできる。

lake init を使用して作成したプロジェクトの Main.lean から、適当に作った Hoge/Fuga.lean を import Hoge.Fuga でインポートしようとしたがうまくいかなかった。

そこで自分のプロジェクト名 (ここでは Playground) のディレクトリを作成し、その中に Hoge/Fuga.lean を移動し import Playground.Hoge.Fuga でインポートするとうまくいった。

いちいちプロジェクト名のディレクトリを作成しないといけないのだろうか？そういえば既存のライブラリとかは src ディレクトリを置いているのを見たことがある、ということで調べると lakefile.lean に srcDir という設定をかけることがわかった。しかしこれもあまり意味がなかった、単に src/Playground/Hoge/Fuga.lean が import Playground.Hoge.Fuga でインポートできるようになるだった。

この辺りのコード を見てみても import する場所の指定はなさそうだった。名前が衝突するなどの理由から無理なのだろうか？

感想

• ドキュメントの不足