digest: backfill leanprover/lean4 for May 2026 (dailies, weeklies, monthly)

31 daily posts (2026-05-01..31), 5 weekly rollups (W18-W22), and the
2026-05 monthly rollup.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: kt3k

src/posts/2026-05-01_leanprover-lean4.md

@@ -0,0 +1,21 @@
+---
+date: 2026-05-01
+repo: leanprover/lean4
+size: M
+title: "Lean fixes docstring metavars and grind slowdown"
+excerpt: "Docstring elaboration now rejects leaked metavariables consistently, and `grind`-based tactics stop wasting time on theory combination."
+commits: 2
+authors: [david-christiansen, leodemoura]
+commit_authors: {"659249a": david-christiansen, "53db221": leodemoura}
+---
+
+### **Docstrings now fail on unresolved metavariables** (659249a)
+Lean now checks for leaked metavariables introduced while elaborating Verso docstrings and module docstrings, and reports them before the term state is rolled back. This makes `{given}` and `{givenInstance}` behave more consistently and improves the resulting error messages when a hole slips through.
+
+### **`grind` derived tactics stop enabling mbtc** (53db221)
+The `NoopConfig` used by `lia`, `linarith`, `cutsat`, `order`, and `ring` now disables model-based theory combination. That should make these tactics fail fast on problems outside their intended scope instead of burning time in expensive reasoning or hitting deterministic timeouts.
+
+### Other misc changes
+- Docstring/Verso test coverage added for leaked metavariable handling
+- Minor doc wording updates in range documentation
+- New regression test for the `grind` timeout issue

src/posts/2026-05-02_leanprover-lean4.md

@@ -0,0 +1,27 @@
+---
+date: 2026-05-02
+repo: leanprover/lean4
+size: M
+title: "Lean4 tightens instance and tactic diagnostics"
+excerpt: "Better universe matching, safer default-instance visibility, and new `.instances` type-check diagnostics landed alongside a few Sym fixes."
+commits: 7
+authors: [Kha, leodemoura]
+commit_authors: {"0303977": leodemoura, "75e37de": leodemoura, "508a113": Kha, "b7ca76a": Kha, "4b8e74b": Kha, "06ac472": Kha, "c53c4b4": Kha}
+---
+
+### **Public default instances no longer leak from private imports** (c53c4b4)
+Lean now filters default instances during export/public-scope elaboration so privately imported instances can’t accidentally influence public signatures. This fixes a class of hard-to-diagnose elaboration failures where an unseen default instance was chosen and later reported as an unknown constant.
+
+### **Tactics now warn when goals only type-check at `.instances` transparency** (508a113)
+Added a new diagnostic path that checks tactic goals at `.instances` transparency and appends a lazy note when `rw`, `simp`, `dsimp`, or `simp_all` would otherwise fail after an `unfold`-style change. This should make transparency-related tactic failures much easier to understand and debug.
+
+### **`wrapInstance` can now reuse nested sub-instances** (06ac472)
+`inferInstanceAs`/`deriving` wrapping was extended to keep recursing through the class graph even after finding a local instance, so already-wrapped subclass instances can be reused instead of needlessly rebuilding them. That improves instance synthesis behavior in more complex class hierarchies.
+
+### **`SymM` universe matching now handles the missing level case** (0303977)
+`processLevel` in `Sym.Pattern` now re-substitutes already-assigned universe uvars before continuing, fixing a missing case that could make otherwise valid matches fail. The added regression test shows this unblocks a `MonadStateOf.get` vs. `Spec.get_StateT` universe match.
+
+### Other misc changes
+- Removed an incorrect assertion in `Sym.simp` `have` simplification (75e37de)
+- Disabled one flaky interactive server test (4b8e74b)
+- Refined CLAUDE.md PR description guidance (b7ca76a)

src/posts/2026-05-03_leanprover-lean4.md

@@ -0,0 +1,36 @@
+---
+date: 2026-05-03
+repo: leanprover/lean4
+size: L
+title: "Lean4 tightens `grind` and Lake artifact handling"
+excerpt: "Lake now awaits extra deps before module headers and meta-import artifacts are fixed; `grind` gets several invariant and proof-hint fixes."
+commits: 7
+authors: [leodemoura, tydeu]
+commit_authors: {"dae3257": tydeu, "326f43a": tydeu, "316c39f": leodemoura, "ee8acc1": leodemoura, "1b23b05": leodemoura, "2d79ec2": leodemoura, "fe3c739": leodemoura}
+---
+
+### **Lake now waits for extra deps before header processing** (dae3257)
+Lake’s module setup build now awaits `extraDep` targets before fetching and processing module headers, so `needs`-style dependencies and cloud releases can actually influence header generation instead of racing it. This changes build ordering in a subtle but important way and closes a correctness gap in module setup construction.
+
+### **Lake includes transitive `meta import` artifacts** (326f43a)
+Lake now tracks when imports are reached through `meta import` and ensures their transitive IR artifacts are included in the setup passed to Lean. This fixes missing `.ir` data in artifact-cache setups, which could otherwise surface as “missing data file” errors.
+
+### **`grind` fixes a congruence-table invariant around lazy `ite` branches** (316c39f)
+When an `ite` branch is internalized lazily, `grind` now explicitly records the parent relation at the right moment so later equivalence-class merges don’t leave stale congruence-table entries behind. This prevents a panic-level invariant violation in a common propagation path.
+
+### **`grind` now internalizes casts before emitting heq propagation** (ee8acc1)
+A cast-related internal error was caused by `pushCastHEqs` running before the arguments it referenced had been internalized. The call moved later in `internalize`, avoiding heqs that point at unenoded terms.
+
+### **`grind` adds missing proof hints for injectivity and projections** (1b23b05)
+Projection and constructor injectivity propagators now wrap generated proofs with the expected proposition shape before pushing equalities. That makes the produced proofs robust enough for downstream checking and fixes proof-construction failures in these propagators.
+
+### **`grind` tightens AC invariant checks for basis vs queue state** (fe3c739)
+The AC invariant checker now distinguishes fully simplified basis entries from partially simplified queue entries, only enforcing the stricter neutral/idempotent checks where they actually apply. This aligns the invariant checker with how AC equations are staged internally and avoids false failures.
+
+### **`grind` fixes another AC invariant edge case** (2d79ec2)
+A follow-up AC invariant fix further narrows when neutral-element checks are enforced during invariant validation. It addresses another checker failure in the AC machinery, reinforcing the same queue-vs-basis distinction.
+
+### Other misc changes
+- New regression tests for the Lake module-setup cases and several `grind` fixes
+- Small internal refactors in `grind` AC/congruence code
+- Test updates for proof term shapes and module import behavior

src/posts/2026-05-04_leanprover-lean4.md

@@ -0,0 +1,21 @@
+---
+date: 2026-05-04
+repo: leanprover/lean4
+size: M
+title: "Lean4 renames clamped ints and reshapes exports"
+excerpt: "UInt8 gets a clearer clamp API, scoped env exports are overhauled, and release tooling/CI are updated alongside benchmark script moves."
+commits: 5
+authors: [Garmelon, Kha, TwoFX]
+commit_authors: {"c8191c5": Kha, "ba502f7": TwoFX}
+---
+
+### **Clamp-style integer constructors renamed** (ba502f7)
+`UInt8.ofNatTruncate` is renamed to `UInt8.ofNatClamp`, matching the newer naming used elsewhere in the library. The old name remains as a deprecated wrapper, so existing code keeps working while users get a clearer API and a consistent migration path.
+
+### **Scoped environment export handling was generalized** (c8191c5)
+`ScopedEnvExtension.exportEntry?` now works with the new `OLeanEntries` export format, and the built-in simp/cbv/grind/instance extensions were updated to use it. This is an internal refactor, but it unblocks more precise export behavior for private vs. public declarations and keeps these extensions aligned with the new persistence API.
+
+### Other misc changes
+- Release tooling and documentation overhaul, including a large rewrite of the release scripts
+- CI workflow updated to use a self-hosted runner when available, with fallback handling
+- Radar benchmark helper scripts moved into this repo for more control over benchmark execution

src/posts/2026-05-05_leanprover-lean4.md

@@ -0,0 +1,41 @@
+---
+date: 2026-05-05
+repo: leanprover/lean4
+size: L
+title: "Lean adds extra linters, plugin init control"
+excerpt: "Renames `--clippy` to `--extra`, lets plugins declare init functions, and includes several fixes for termination errors, I/O, and crashes."
+commits: 16
+authors: [eric-wieser, nomeata, hargoniX, wkrozowski, tydeu, Kha, Garmelon, sgraf812, leodemoura]
+commit_authors: {"ea6e767": wkrozowski, "ad5ec0e": tydeu, "03bd884": nomeata, "e4c0a5a": eric-wieser, "70098e4": eric-wieser, "c9855f5": eric-wieser, "8ebd294": leodemoura}
+---
+
+### **Rename `--clippy` to `--extra` and broaden its scope** (ea6e767)
+`lake lint --clippy` is now `lake lint --extra`, and it no longer means only “non-default” linters: it runs the default builtin linters together with the extra ones. That changes the linter selection model and also renames the underlying option/namespace/attribute plumbing, so existing scripts and custom linters need to follow the new naming.
+
+### **Plugin loading can now specify an explicit init function** (ad5ec0e)
+`Lean.loadPlugin` now accepts an optional init-function name, and the CLI/JSON setup formats can pass `path:initFn` or `{path, initFn}`. This makes plugin loading more flexible for nonstandard shared-library names and aligns the frontend, setup, and import paths around a richer plugin descriptor.
+
+### **Termination errors now point at the correct recursive call site** (03bd884)
+Recursive applications now carry source byte position metadata in addition to syntax, preventing identical calls at different locations from being merged by hashconsing/simplification. That fixes misleading termination diagnostics where the reported failing call could come from the wrong branch.
+
+### **`Sym.simp` no longer chokes on kernel projections in matches** (8ebd294)
+The symbolic simplifier now folds kernel `Expr.proj` terms back into projection applications before continuing simplification. This avoids a panic triggered by struct-eta/iota combinations and makes `Sym.simp` more robust on `match`/`do`-heavy code.
+
+### **Module loading handles interrupted reads and clearer I/O failures** (70098e4)
+`readModuleDataParts` now retries `EINTR` and distinguishes interrupted reads, unexpected EOF, and other read failures with better errors. This fixes import loading on filesystems or runtimes where `read()` can return short or interrupted reads.
+
+### **Severity overrides now affect the exit code before counting errors** (e4c0a5a)
+Promoted diagnostics are now applied before Lean increments its error counter, so `lean --error=tag` correctly exits nonzero when a warning is upgraded to an error. This restores the intended behavior of the feature and closes a regression.
+
+### **`mpz` allocation failures now abort instead of corrupting memory** (c9855f5)
+When Lean is built without GMP, `mpz_alloc` now checks for `malloc`/`mi_malloc` failure and panics on OOM rather than continuing with a null pointer. That closes a memory-safety hole that could otherwise turn allocation failure into corruption.
+
+### Other misc changes
+- Updated stage0 snapshot.
+- Benchmark/build tooling now uses lean-llvm and supports it in lake.
+- CI workflow adjusted for external PRs.
+- `wrapInstance` shake dependency tracking fixed.
+- `grind` no longer uses `grind` in HTTP lowercasing.
+- Added `trace.Meta.Tactic.simp.backwardDefEq`.
+- `readModuleDataParts` now guards the empty-file case without `LEAN_MMAP`.
+- Sym-based `mvcgen'` was expanded to match `mvcgen` more closely, with benchmark/test updates.

src/posts/2026-05-06_leanprover-lean4.md

@@ -0,0 +1,35 @@
+---
+date: 2026-05-06
+repo: leanprover/lean4
+size: L
+title: "Lean 4 tightens docstrings, attrs, and runtime safety"
+excerpt: "Blockquotes now render in Verso docstrings, attribute loading gets stricter, LLVM 22 lands, and the runtime hardens OOM handling."
+commits: 14
+authors: [sgraf812, Kha, hargoniX, david-christiansen, nomeata, kim-em, eric-wieser, wkrozowski]
+commit_authors: {"5d56421": david-christiansen, "036bd4f": kim-em, "56fe75e": eric-wieser, "8d2b5d0": hargoniX, "e6dfdfd": Kha, "0e2088f": wkrozowski}
+---
+
+### **Verso docstrings now support blockquotes and render more robustly** (5d56421)
+Lean’s docstring pipeline now handles blockquotes end-to-end, and the Markdown renderer was reworked to combine blocks and inlines more reliably. This should fix previously missing output and reduce formatting glitches around quoted, indented docstring content.
+
+### **Attribute elaboration now rejects IR-only modules** (e6dfdfd)
+The elaborator now errors if `@[attr]` comes from a module that is reachable only through IR and not visibly imported. That closes a server-vs-command-line inconsistency and avoids `lake shake --fix` flip-flopping on repeated runs.
+
+### **Runtime allocator now panics safely on OOM instead of corrupting state** (56fe75e)
+When segment allocation fails, the runtime now treats that as fatal instead of propagating `std::bad_alloc` after leaving the small allocator inconsistent. This prevents later memory corruption in code that tries to recover from allocation failure.
+
+### **Lean upgrades LLVM to 22** (8d2b5d0)
+The LLVM toolchain was bumped from 19.1.2 to 22.1.4 across CI and benchmark scripts. This brings the repo onto the newer backend and is expected to yield modest performance gains.
+
+### **Diagnostics and simp reporting now avoid exporting-mode crashes** (036bd4f)
+Diagnostic reporting is wrapped in `withoutExporting`, so private helper names referenced in unfold summaries no longer trigger “Unknown constant” errors in module mode. This fixes a real crash path when `diagnostics` is enabled under a `public section`.
+
+### **Core linter for unreachable tactics is now upstreamed** (0e2088f)
+The `unreachableTactic` linter has been moved into core and wired into `Lean.Linter.Extra`. That gives Lean a built-in warning for dead tactics after constructs like `tac1 <;> tac2`.
+
+### Other misc changes
+- `mvcgen'` prototype tweaks and test fixes across several commits
+- Cancellation test infrastructure simplified
+- `CLAUDE.md` test note updated
+- `reldebug` preset renamed to `relwithassert`
+- LLVM upgrade docs added

src/posts/2026-05-07_leanprover-lean4.md

@@ -0,0 +1,30 @@
+---
+date: 2026-05-07
+repo: leanprover/lean4
+size: L
+title: "Lean4 adds verifiable loops and mvcgen'"
+excerpt: "Major proof-engine upgrades landed: verifiable while/repeat loops, a new SymM-based mvcgen' tactic, plus deprecation-warning cleanup and runtime speedups."
+commits: 8
+authors: [wkrozowski, sgraf812, TwoFX, nomeata, Kha, hargoniX]
+commit_authors: {"9151360": nomeata, "a416b90": wkrozowski, "422920f": sgraf812, "049b7eb": sgraf812, "355dca6": hargoniX}
+---
+
+### **Verifiable `repeat`/`while` loops land** (049b7eb)
+Lean now models `forIn` via a new `whileM` API with unfolding and specification theorems, making these loops amenable to verification without changing user syntax. This is a substantial step for `mvcgen`-style reasoning about control flow and loop invariants.
+
+### **Experimental `mvcgen'` introduces a much faster SymM-based VC generator** (422920f)
+A new `mvcgen'` tactic is added as a drop-in experimental replacement for `mvcgen`, built on the newer `SymM` symbolic-evaluation framework. The implementation is promoted into the main source tree, suggesting the old benchmark-only prototype is becoming a supported part of the tactic stack.
+
+### **Deprecation warnings are now suppressed inside deprecated definitions** (a416b90)
+Lean no longer emits redundant `Linter.deprecated` warnings for references that appear inside code already marked `@[deprecated]`. This cleans up noisy diagnostics and matches the rule that those references are going away with the declaration itself.
+
+### **Runtime reference-count teardown gets a cold-path optimization** (355dca6)
+`lean_dec_ref_cold` was tightened by splitting out the cold path and using a smaller header write on 64-bit builds. This is low-level performance work that can reduce overhead in reference-counted object destruction.
+
+### **Hover now preserves the target symbol for `fun_induction`** (9151360)
+`fun_induction` now resolves the function target with info preserved, so editor hover shows the actual function name instead of losing symbol context. That improves interactive ergonomics for proof development.
+
+### Other misc changes
+- Reduced `String.length` usage across the codebase, including a new dedicated string-length module and some API reshuffling.
+- Refactored `cbv` to use `SymM` primitives in a few congruence-heavy paths.
+- Removed an old `printDecls` test.

src/posts/2026-05-08_leanprover-lean4.md

@@ -0,0 +1,20 @@
+---
+date: 2026-05-08
+repo: leanprover/lean4
+size: M
+title: "Lake config hoisted; CI unblocked"
+excerpt: "Lake now stores compiled configs in workspace-local paths, while CI pins a broken action tag to restore builds."
+commits: 3
+authors: [tydeu, TwoFX, kim-em]
+commit_authors: {"41eccce": tydeu, "819f454": TwoFX, "85d46c3": kim-em}
+---
+
+### **Lake hoists compiled configs to the workspace** (41eccce)
+Lake now writes compiled configuration artifacts into the workspace’s `.lake/config/<pkgIdx>` instead of each package’s own `.lake/config`. This avoids contention when multiple workspaces share a dependency and makes config caching less collision-prone.
+
+### **CI pins test-summary to a stable SHA** (85d46c3)
+The build template stops using the broken floating `test-summary/action@v2` tag and pins the action to the immutable v2.4 commit SHA. This unblocks the shared CI template after upstream retagging removed the expected `index.js` from the `v2` target.
+
+### Other misc changes
+- Replaced several remaining `String.length` calls with string-position/byte-size aware checks and emptiness tests for correctness on UTF-8 text (819f454)
+- Misc internal string-handling cleanups across pretty-printing, docstrings, matching, semantic highlighting, and time formatting (1 commit)

src/posts/2026-05-09_leanprover-lean4.md

@@ -0,0 +1,19 @@
+---
+date: 2026-05-09
+repo: leanprover/lean4
+size: M
+title: "Public Glob parser and PR rebasing guidance"
+excerpt: "Lean4 made `Glob.ofString?` public and added CLAUDE guidance to avoid changing a PR’s GitHub base when rebasing locally."
+commits: 2
+authors: [kim-em]
+commit_authors: {"1e367b5": kim-em, "68764f5": kim-em}
+---
+
+### **Public `Glob.ofString?` for Lake TOML parsing** (1e367b5)
+`Glob.ofString?` is now public, which lets downstream code reuse the parser instead of relying on `open private` access. The commit is small, but it removes an access restriction that was blocking Mathlib cleanup.
+
+### **Clarify Claude guidance on rebasing vs PR base** (68764f5)
+Added a short note to `.claude/CLAUDE.md` explaining that “rebase onto X” should change only the local branch base, not the PR’s GitHub `--base` target. This helps preserve the Lean4 workflow where `nightly-with-mathlib` is used as a CI rebase target while the PR still targets `master`.
+
+### Other misc changes
+- None.