Lean4: Version 4.28.0 release/update and 4.29.0-rc1

rc1 無くなってますね。

リリースノート

前記事

変更点（ざっくり）

🐺賢狼に調べてもらいました。

Lean 4.28.0（2026-02-17）の release note から、「開発者が体感しやすい主な変更点」を要点だけ抜き出してまとめるぞい。

言語・エラボレータ周り（Language）

• `match` の一般化（generalization）が賢くなり、これまで落ちていた例が通るようになった。挙動を戻したい場合は `match ... (generalizing := false)` を付けて旧挙動にできる。

• Mathlib 由来の依存関係管理コマンドが本体へ取り込まれた：
  `#import_path Foo`（import の鎖を表示）、`assert_not_exists Foo`、`assert_not_imported Module`、`#check_assertions` など。

• `mvcgen with tac` が `tac` 失敗時に失敗するようになり、挙動がより直感的に（旧挙動は `mvcgen with try tac`）。

• モジュール/可視性・回帰の修正（public inductive を mutual 内で宣言したときの問題、`declare_syntax_cat` のローカル宣言が import エラーを誘発する問題、など）や、`where` 節での Verso docstring 対応が入った。

タクティク（Tactics）

• `simp`/`simp_all`/`dsimp` に `+locals` オプション：そのファイル内定義を自動で unfold 対象へ（同様に `grind` にも `+locals`）。

• 並列に走らせて最初に成功したものを採用する `first_par` コンビネータが追加。

• `Sym.simp`（構造的 simplifier 系）で `have` telescope の扱い・性能改善、`simpForall`/`simpArrow` 実装など、高速化と機能強化がまとまって入っている。

標準ライブラリ（Library）

• `BitVec.cpop`（popcount）追加など、BitVec 周りが強化。

• キャンセル（cancellation）のための `Context` 型が追加。

• `Int` の range 補題が増えて `Nat` 側との対称性が改善、Iterator API は `IteratorCollect` 型クラス削除で簡素化。

• get-elem tactic が range の subarray を扱えるようになるなど、配列/ループ周りの使い勝手も改善。

コンパイラ・ランタイム（Compiler）

• 特殊化（specializer）の強化、`Quot.lift` の LCNF 変換での panic 回避、`getLine` 最適化など、正しさ＋性能の改善が複数。

• 線形性（linear/owned 変数）を壊しうる最適化の修正：`floatLetIn` が parser の `ParserState` を非線形化してしまうケースを防ぐ。

• SCC 分割や Decidable の定数畳み込み前倒し、サブ項抽出の superlinear 修正、ASAN 下の `IO.Process.spawn` でのデッドロック回避など。

ドキュメント（Documentation）

• `ffi.md` をマニュアル参照リンクへ置換、iterator 文書の docstring 補完。

• tactic docs の「先頭トークン自動検出」が頑丈に、`let rec` tactic の補完/ドキュメントも有効化。

LSP/サーバ（Server）

• `lakefile.toml` の JSON Schema 修正（`require.git` の table 形式許可）、補完/あいまい検索の高速化。

• async theorem が絡む go-to-definition の修正、NeoVim の code action 修正など、IDE 体験の地味に痛い不具合が改善。

Lake（ビルド/パッケージ管理）

• `meta import` の推移閉包の扱いを Lean 本体の期待に合わせて修正。

• `lakefile.lean` の数値オプションで `.ofNat` が不要に。

• `lake shake` が組み込みコマンド化、artifact cache のデフォルト挙動改善、`lake build --no-build` の終了コード修正、`lake query` の出力修正、依存での `+mod` 復活など。

そのほか & FFI

• Lean の挙動変更を追跡するための bisect 支援 Python スクリプト、CI artifact ダウンロード用スクリプト、`lean4checker` を elan 既知の `leanchecker` として提供、などツール面が強化。

• FFI：Lean ヘッダに対してビルドするライブラリで `-fwrapv` 必須を撤廃。

全体としては、「言語コアの挙動改善（特に `match`）」「依存管理コマンドの本体取り込み」「simp/grind 周りの UX 改善」「Lake/LSP の実務的な不具合修正＋体感速度改善」が柱じゃな。

DkMath

現在、活用中のソースコードでの影響はありませんでした。

リポジトリ

2026/02/18 15:34

D.

#Lean #Lean4 #Mathlib #Mathlib4 #release #リリース

Appendix

DkMath リポジトリ

こちらも、main / nightly 共に Lean 4.28.0 + Mathlib4 に対応。
main においては、非推奨 補題名 警告 が出てしまっていますが nightly では、出なくなって使わなくなったのでしょう。合流すれば問題ないです。