digest: backfill leanprover/lean4 2026-06-06..08

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

Author: kt3k

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

@@ -0,0 +1,16 @@
+---
+date: 2026-06-06
+repo: leanprover/lean4
+size: M
+title: "Lean switches to faster refcount cleanup"
+excerpt: "A small performance tweak replaces a heavier object destructor with a more precise free path in refcount teardown."
+commits: 1
+authors: [hargoniX]
+commit_authors: {"8391b96": hargoniX}
+---
+
+### **Faster refcount cleanup in `dec_ref_known`** (8391b96)
+`lean_dec_ref_known` now calls `lean_free_object` instead of `lean_del_object` when dropping a constructor with known children. This is a targeted performance improvement in the runtime’s reference-counting path, shaving overhead from object teardown.
+
+### Other misc changes
+- None

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

@@ -0,0 +1,20 @@
+---
+date: 2026-06-07
+repo: leanprover/lean4
+size: L
+title: "Std.Time gets a major DateTime overhaul"
+excerpt: "Lean4 overhauls its time API around the renamed DateTime type, while also exposing reflectBV for BVDecide users."
+commits: 2
+authors: [hargoniX, algebraic-dev]
+commit_authors: {"a806b5c": hargoniX, "b3b7d7a": algebraic-dev}
+---
+
+### **Std.Time replaces ZonedDateTime with a new DateTime API** (b3b7d7a)
+This is a broad refactor of the `Std.Time` stack: the old `DateTime (tz : TimeZone)`/`ZonedDateTime` split is collapsed into a redesigned `DateTime` centered on zone rules and timezone-aware helpers. It updates formatting, parsing, notation, HTTP date handling, server logging, and a large set of time tests, so downstream code will likely need API adjustments.
+
+### **`reflectBV` is now public** (a806b5c)
+`Lean.Meta.Tactic.BVDecide.Prover.Basic.reflectBV` is exported publicly, making the BVDecide reflection helper available to other code. This is a small API exposure but can unblock external metaprogramming uses.
+
+### Other misc changes
+- HTTP/time plumbing updated to use the renamed time types and helpers
+- Various time tests and formatting expectations adjusted

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

@@ -0,0 +1,30 @@
+---
+date: 2026-06-08
+repo: leanprover/lean4
+size: L
+title: "Lean adds do-notation and linting upgrades"
+excerpt: "Major do-notation semantics changed, env linters became option-driven, and the compiler gained USize constant folding."
+commits: 9
+authors: [hargoniX, Kha, Garmelon, wkrozowski, volodeyka, sgraf812]
+commit_authors: {"3696103": sgraf812, "6b63f7d": Garmelon, "b6682da": hargoniX, "5b6365d": wkrozowski, "50e5bb3": volodeyka, "d265d1c": Kha}
+---
+
+### **Do-notation now accepts arbitrary `doElem`s after `←`** (3696103)
+`nestedAction` now parses a full `doElem` after `←`, not just a term, and the new elaborator handles the richer syntax. This is a breaking change for code that relied on `return` inside nested actions to return from the inner block; the legacy elaborator still preserves the old restriction behind `set_option backward.do.legacy true`.
+
+### **Environment linters are now controlled by Lean options** (5b6365d)
+Builtin environment linters can now be toggled per declaration with `set_option linter.X false in ...` and at the CLI with `lake lint --linters=...`. The implementation also snapshots linter options into the environment so declaration-level lint behavior is tracked consistently across elaboration and lint runs.
+
+### **Compiler folds `USize` equality and ordering** (b6682da)
+The constant folder now evaluates `USize.decEq`, `USize.decLt`, and `USize.decLe` in both 32-bit and 64-bit interpretations and only folds when they agree. That makes platform-dependent `USize` comparisons more optimizable without risking incorrect cross-platform behavior.
+
+### **`@[spec]` gains a new internal WP-based path** (50e5bb3)
+`@[spec]` was refactored to support both legacy `Std.Do.Triple` specs and a new internal weakest-precondition-based spec database. This is a substantial preparatory change for `mvcgen`, preserving backward compatibility while adding a dispatcher that can register either spec style.
+
+### **Lean release scripts and CI were tightened up** (6b63f7d, d265d1c)
+Release tooling got more robust around toolchain lookup and workflow handling, and macOS aarch64 CI was demoted out of the PR path to save time. These changes reduce friction in release automation and shorten the feedback loop for contributors.
+
+### Other misc changes
+- Fixed an incorrect debug assertion in `lean.h`.
+- Updated stage0 artifacts.
+- Added a Claude skill note for retrying stage2 olean-related test failures.