Lean プロジェクトの依存関係を 自動更新する

Transcript

1. Lean プロジェクトの依存関係を 自動更新する 井上亜星 Proxima Technology 2026-01-12
2. はじめに
3. 自己紹介 はじめに • 趣味で Lean を勉強しています • Lean by Example という日本語リファレン スを書いています • 2025 年 9 月に Lean の入門書をラムダノー トから出版しました 井上亜星 Lean プロジェクトの依存関係を自動更新する 2026-01-12 2 / 21
4. 今回の目的 はじめに • そもそも Lean とは何かを紹介する • Lean プロジェクトの依存関係を自動更新する 方法について紹介する • 開発の裏話を聞いていただく 井上亜星 Lean プロジェクトの依存関係を自動更新する 2026-01-12 3 / 21
5. そもそも Lean とは何か
6. Lean は、証明支援系 そもそも Lean とは何か • 定理証明支援系の一種 ‣ Rocq(旧 Coq)や Isabelle などの仲間 ‣ 数学の定理やソフトウェアの仕様をコードで表現して、 証明できる • 間違いを犯しやすい人類に代わって、 ソフトウェアや証明の正しさをチェックしてくれる • ここでは詳しく説明しないが、 「依存型」という強力な型システムに基づいている 井上亜星 Lean プロジェクトの依存関係を自動更新する 2026-01-12 5 / 21
7. Lean は、プログラミング言語 そもそも Lean とは何か • Lean は汎用言語としても使えるように作られている • 公式サイトにも、programming language だと書かれている 井上亜星 Lean プロジェクトの依存関係を自動更新する 2026-01-12 6 / 21
8. Lean では証明とプログラムは地続き そもそも Lean とは何か プログラムと証明は全然違うものという印象があるかもしれ ないが、 Lean では証明とプログラムは地続き Lean でプログラムを書くと、証明が自然に現れる • 再帰関数を定義するとき、停止証明を要求される • 配列にインデックスアクセスするとき、 それが範囲内であることの証明を要求される • モナドを定義したら、 それがモナド則を満たしていることを証明できる 井上亜星 Lean プロジェクトの依存関係を自動更新する 2026-01-12 7 / 21
9. Lean では証明とプログラムは地続き そもそも Lean とは何か 逆に証明を書くときにプログラムが必要になることもある • 命題𝑃が成り立つかどうか判定するアルゴリズムがあるな ら、 それを実装すれば𝑃の証明に使えるようになる • Lean での自動証明のカスタマイズは手続き的に行えるので まさにプログラミングそのもの 井上亜星 Lean プロジェクトの依存関係を自動更新する 2026-01-12 8 / 21
10. Lean では証明とプログラムは地続き そもそも Lean とは何か 同じ関数を証明にもプログラムにも使うことには問題もある たとえば文字列 String は • 証明に使うことを考えると文字 Char のリストとして定義し たい • プログラムに使うことを考えるともっと効率的な表現にし たい 井上亜星 Lean プロジェクトの依存関係を自動更新する 2026-01-12 9 / 21
11. Lean では証明とプログラムは地続き そもそも Lean とは何か Lean では等しいことの証明があればコンパイラ上で実装を置 き換えるように指示できて、ある程度この問題を解決できる ようになっている 井上亜星 Lean プロジェクトの依存関係を自動更新する 2026-01-12 10 / 21
12. lean-update について
13. Lean はまだ開発中 lean-update について Lean 4 はだいぶ安定してきたとはいえ、月に一度のペースで 新しいリリース(候補)が出る (mathlib はもっと頻繁に更新される) • 開発元は最新版しか見ていないので、使う側も最新を使い たい • まとめて更新すると大変なので、ちまちま更新したい！ 井上亜星 Lean プロジェクトの依存関係を自動更新する 2026-01-12 12 / 21
14. lean-update とは lean-update について Lean の依存関係を更新して、ビルドが通るか自動で確かめて くれる GitHub Action が欲しい！ • lean-update が誕生 • 元々は Oliver Butterley さんのプロジェクト • Oliver さんのやる気がなくなったので 私がメンテナになった 井上亜星 Lean プロジェクトの依存関係を自動更新する 2026-01-12 13 / 21
15. lean-update の仕組み lean-update について • Lean の最新版のリリースを取得して • lake update コマンドを実行して • ビルド＆テストを試してみて ‣ テストが失敗したら issue 投稿したり ‣ ビルドが通ったら PR を出したり を行うだけ。シンプル。 井上亜星 Lean プロジェクトの依存関係を自動更新する 2026-01-12 14 / 21
16. lean-update のありがたみ lean-update について 「最新版だとビルドが通らなくなる」という事象を素早く キャッチしてくれるので、 特に mathlib に依存しているようなプロジェクトだとありが たいかも 井上亜星 Lean プロジェクトの依存関係を自動更新する 2026-01-12 15 / 21
17. 開発の裏話
18. 問題が山積み 開発の裏話 作ってみると、意外と難しいことが分かってきた • 要件が意外と複雑 • GitHub Action 自体の保守のしんどさ 井上亜星 Lean プロジェクトの依存関係を自動更新する 2026-01-12 17 / 21
19. 要件が意外と複雑 開発の裏話 • Lean のバージョン取得のやり方 ‣ 各リリースごと ‣ rc は無視して stable のみ ‣ nightly を追いかける • lake build 以外のチェック ‣ lake test も実行 ‣ lake lint も実行 • CLI ツールなら --version の出力も更新したい …etc 井上亜星 Lean プロジェクトの依存関係を自動更新する 2026-01-12 18 / 21
20. GitHub Action 自体の保守のしんどさ 開発の裏話 • action.yml ファイルにワークフローの処理を書いていく ‣ 状態管理も条件分岐も例外処理も全部 yml • テストもやりにくい ‣「自分自身を呼び出す」ことによってテストしている でもこれが良い方法なのかわからない… ‣ IO 系の操作が多くてそもそもテストが書きづらい 要件の複雑さをカバーしきれない（私の能力不足もあり） 井上亜星 Lean プロジェクトの依存関係を自動更新する 2026-01-12 19 / 21
21. GitHub Action 自体の保守のしんどさ 開発の裏話 私の前に着手された Oliver さん、類似の Action を管理してい る Anne さん、みなさん苦労されている様子 lean-update に限らず「自動更新 Action」が Lean 界隈で普及 しない原因はこの辺にありそう 良い方法があれば教えてください 井上亜星 Lean プロジェクトの依存関係を自動更新する 2026-01-12 20 / 21
22. ご清聴ありがとうござ いました