lakeの再帰的なビルドと手作業でのビルド

Lean ハマリ所 tips

lakeはnpmほどには洗練されてないみたいだ。現状では完全な自動ビルドは無理な気がする。原因不明な失敗をすることがある。

ビルドの手順は、原理的には次のようなことだと思う。

  1. ./lean-toolcahin を見て、ツールチェーンがインストールされてなければ、elan toolchain install でツールチェーンをインストールする。
  2. lakefile.lean の require を見て、依存関係〈dependency〉を知る。現パッケージが依存しているパッケージを ./lake-packages/ の直下に git clone する。原始的だが、grep require で依存しているパッケージは分かる。
  3. クローンしたパッケージの lakefile.lean の require を見て、依存しているパッケージを ./lake-packages/ の直下にクローンする。現状、入れ子の構造は作らないようだ。./lake-packages/ の下にすべてのパッケージがフラットに並ぶ。
  4. 再帰的な検索とクローンにより、依存しているパッケージは ./lake-package/ の下を探せばある（揃っている）状態を作る。
  5. すべてのパッケージの lakefile.lean を読んで依存関係グラフを作る。サイクルがあったらどうする？
  6. 依存関係グラフの末端から順にパッケージ単位でビルドする。
  7. ビルド時に、既にビルド済みのパッケージのディレクトリ ./lake-packages/pkg/build/, ./lake-packages/pkg/build/lib/ などを、ツールに指定して、依存関係を解決してあげる。
  8. 各パッケージごとに必要とするツールチェーンもlakeバージョンも違うので、各パッケージごとにOSのプロセスとして別なlakeを起動する必要がある。
lakeの実行

コマンドラインで：

> lake build -v | tee "$(date +%Y-%m-%d_%H-%M-%S)_build.log"

これは、Git BashでもPowershellでもOK。Powershellのteeは Tee-Object の別名だが特に問題ない。

Gig Bash：

  • alias 名前
  • alias 名前=文字列
  • unalias 名前
  • alias lean-build="lake build -v | tee \$(date +%Y-%m-%d_%H-%M-%S).lake-build.log"

Powershell：

  • alias 名前 または get-alias 名前
  • set-alias 名前 文字列
  • remove-item alias:名前
  • 下のスクリプトファイル
# lean-build.ps1
lake build -v | tee "$(date +%Y-%m-%d_%H-%M-%S).lake-build.log"

Powershellでは、lakeからの出力がないとルグファイルが作られないが、Git Bashではサイズ0のファイルが作られる。

パッケージバージョンの確認

信用できるのは、gitコミットのハッシュ値だけ。./laka-manifest.json に正確なバージョン（ハッシュ値）が書いてある。

{"git":
  {"url": "https://github.com/mhuisi/lean4-cli",
    "subDir?": null,
    "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e",
    "name": "Cli",
    "inputRev?": "nightly"
  }
}

この例で：

  • url: gitリポジトリのURLは "https://github.com/mhuisi/lean4-cli"
  • subDir?: サブディレクトリ指定はなし。リポジトリ全体（コミットのルートから下全部）がパッケージの内容物となる。
  • rev: パッケージのgitコミットのハッシュ値
  • name: パッケージ名、この名前でサブディレクトリが作られる。コンフリクトする可能性あり。
  • inputRev?: パッケージのブランチやリリースの名前

git cloneしたコミットのハッシュ値は次のようにして求める。

$ git branch
* master

$ git rev-parse master
ecad15071973627f08ce7af018100fdbee566654

lakeがダウンロードして ./lake-packages/ の下にいれたパッケージでは、HEADがデタッチされている。

$ git branch
* (HEAD detached at 5a858c3)
  main

$ cat .git/HEAD
5a858c32963b6b19be0d477a30a1f4b6c120be7e

HEADが指しているコミットは、たいてはタグが付いている。最後〈最新〉のタグがパッケージのリリースバージョンになっていることが多いが、いつでもそうとは限らない。タグよりハッシュ値ベースで確認する。

$ git tag | tail -1
v2.1.0-lnightly-2022-11-20

$ git rev-parse $(git tag | tail -1)
5a858c32963b6b19be0d477a30a1f4b6c120be7e