Skip to content

v4.27.0 - #155

Merged
pandaman64 merged 1 commit into
mainfrom
v4.27.0
Jan 25, 2026
Merged

v4.27.0#155
pandaman64 merged 1 commit into
mainfrom
v4.27.0

Conversation

@pandaman64

@pandaman64 pandaman64 commented Jan 25, 2026

Copy link
Copy Markdown
Owner

Note

Upgrade to Lean v4.27.0

  • Updates lean-toolchain to v4.27.0 for correctness, docbuild, and regex
  • Refreshes lake-manifest.json and lakefile.toml pins: mathlib to v4.27.0 and newer SHAs for proofwidgets, aesop, Qq, batteries, plausible, LeanSearchClient, importGraph, Cli, doc-gen4, etc.

Minor proof maintenance

  • In RegexCorrectness/Backtracker/Basic.lean, add rfl after rw! [pushNext, ...] in several pushNext case lemmas (done, fail, epsilon, split, saveFin, save) to close equalities.

Written by Cursor Bugbot for commit 427bf4c. This will update automatically on new commits. Configure here.

@pandaman64
pandaman64 enabled auto-merge (squash) January 25, 2026 11:09
@pandaman64
pandaman64 merged commit 6756b62 into main Jan 25, 2026
3 checks passed
@pandaman64
pandaman64 deleted the v4.27.0 branch January 25, 2026 11:19
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant