Leanのパッケージ

Leanにも、NPMパッケージと同様な仕掛けがあるらしい。

• ディレクトリがパッケージ
• メタデータが leanpkg.toml
• 一部のメタデータは leanpkg.path にある。

ツールの情報がメタデータに書いてあって、パッケージをダウンロードした先で環境を再現できるようになっている。今はツールはグローバルだが、node_modules/ のように、ローカルにインストールとなるのかも知れない。

パッケージ構造に関しては、

• https://leanprover.github.io/reference/using_lean.html