fix: make -DLEAN_VERSION_* CMake overrides actually work (#13226)

This PR updates `release_checklist.py` to handle the `CACHE STRING ""`
suffix on CMake version variables. The `CACHE STRING` format was
introduced in the `releases/v4.30.0` branch, but the script's parsing
wasn't updated to match, causing false failures.

🤖 Prepared with Claude Code

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

.claude/commands/release.md

@@ -157,6 +157,16 @@ Note: `gh pr checks --watch` exits as soon as ALL checks complete (pass or fail)
 fail while others are still running, `--watch` will continue until everything settles, then exit
 with a non-zero code. So a background `--watch` finishing = all checks done; check which failed.
 
+## Mathlib Bump Branches
+
+Mathlib `bump/v4.X.0` branches live on the **fork** `leanprover-community/mathlib4-nightly-testing`,
+NOT on `leanprover-community/mathlib4`.
+
+## Never Force-Update Remote Refs Without Confirmation
+
+Never force-update an existing remote branch or tag via `git push --force` or the GitHub API
+without explicit user confirmation.
+
 ## Error Handling
 
 **CRITICAL**: If something goes wrong or a command fails:

.github/workflows/ci.yml

@@ -143,7 +143,7 @@ jobs:
           CMAKE_MAJOR=$(grep -E "^set\(LEAN_VERSION_MAJOR " src/CMakeLists.txt | grep -oE '[0-9]+')
           CMAKE_MINOR=$(grep -E "^set\(LEAN_VERSION_MINOR " src/CMakeLists.txt | grep -oE '[0-9]+')
           CMAKE_PATCH=$(grep -E "^set\(LEAN_VERSION_PATCH " src/CMakeLists.txt | grep -oE '[0-9]+')
-          CMAKE_IS_RELEASE=$(grep -m 1 -E "^set\(LEAN_VERSION_IS_RELEASE " src/CMakeLists.txt | sed -nE 's/^set\(LEAN_VERSION_IS_RELEASE ([0-9]+)\).*/\1/p')
+          CMAKE_IS_RELEASE=$(grep -m 1 -E "^set\(LEAN_VERSION_IS_RELEASE " src/CMakeLists.txt | grep -oE '[0-9]+' | head -1)
 
           # Expected values from tag parsing
           TAG_MAJOR="${{ steps.set-release.outputs.LEAN_VERSION_MAJOR }}"

.gitpod.yml

@@ -6,6 +6,6 @@ vscode:
     - leanprover.lean4
 
 tasks:
-  - name: Release build
-    init: cmake --preset release
+  - name: Build
+    init: cmake --preset dev
     command: make -C build/release -j$(nproc || sysctl -n hw.logicalcpu)

CMakeLists.txt

@@ -1,4 +1,6 @@
 cmake_minimum_required(VERSION 3.21)
+include(ExternalProject)
+include(FetchContent)
 
 if(NOT CMAKE_GENERATOR MATCHES "Makefiles")
   message(FATAL_ERROR "Only makefile generators are supported")
@@ -34,7 +36,6 @@ foreach(var ${vars})
   endif()
 endforeach()
 
-include(ExternalProject)
 project(LEAN CXX C)
 
 if(NOT (DEFINED STAGE0_CMAKE_EXECUTABLE_SUFFIX))
@@ -119,17 +120,16 @@ if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
 endif()
 
 if(USE_MIMALLOC)
-  ExternalProject_Add(
+  FetchContent_Declare(
     mimalloc
-    PREFIX mimalloc
     GIT_REPOSITORY https://github.com/microsoft/mimalloc
     GIT_TAG v2.2.3
-    # just download, we compile it as part of each stage as it is small
-    CONFIGURE_COMMAND ""
-    BUILD_COMMAND ""
-    INSTALL_COMMAND ""
+    # Unnecessarily deep directory structure, but it saves us from a complicated
+    # stage0 update for now. If we ever update the other dependencies like
+    # cadical, it might be worth reorganizing the directory structure.
+    SOURCE_DIR "${CMAKE_BINARY_DIR}/mimalloc/src/mimalloc"
   )
-  list(APPEND EXTRA_DEPENDS mimalloc)
+  FetchContent_MakeAvailable(mimalloc)
 endif()
 
 if(NOT STAGE1_PREV_STAGE)

CMakePresets.json

@@ -8,16 +8,26 @@
   "configurePresets": [
     {
       "name": "release",
-      "displayName": "Default development optimized build config",
+      "displayName": "Release build config",
       "generator": "Unix Makefiles",
       "binaryDir": "${sourceDir}/build/release"
     },
+    {
+      "name": "dev",
+      "displayName": "Default development optimized build config",
+      "cacheVariables": {
+        "STRIP_BINARIES": "OFF"
+      },
+      "generator": "Unix Makefiles",
+      "binaryDir": "${sourceDir}/build/dev"
+    },
     {
       "name": "debug",
       "displayName": "Debug build config",
       "cacheVariables": {
+        "CMAKE_BUILD_TYPE": "Debug",
         "LEAN_EXTRA_CXX_FLAGS": "-DLEAN_DEFAULT_THREAD_STACK_SIZE=16*1024*1024",
-        "CMAKE_BUILD_TYPE": "Debug"
+        "STRIP_BINARIES": "OFF"
       },
       "generator": "Unix Makefiles",
       "binaryDir": "${sourceDir}/build/debug"
@@ -26,7 +36,8 @@
       "name": "reldebug",
       "displayName": "Release with assertions enabled",
       "cacheVariables": {
-        "CMAKE_BUILD_TYPE": "RelWithAssert"
+        "CMAKE_BUILD_TYPE": "RelWithAssert",
+        "STRIP_BINARIES": "OFF"
       },
       "generator": "Unix Makefiles",
       "binaryDir": "${sourceDir}/build/reldebug"
@@ -38,6 +49,7 @@
         "LEAN_EXTRA_CXX_FLAGS": "-fsanitize=address,undefined -DLEAN_DEFAULT_THREAD_STACK_SIZE=16*1024*1024",
         "LEANC_EXTRA_CC_FLAGS": "-fsanitize=address,undefined",
         "LEAN_EXTRA_LINKER_FLAGS": "-fsanitize=address,undefined -fsanitize-link-c++-runtime",
+        "STRIP_BINARIES": "OFF",
         "SMALL_ALLOCATOR": "OFF",
         "USE_MIMALLOC": "OFF",
         "BSYMBOLIC": "OFF",
@@ -58,6 +70,10 @@
       "name": "release",
       "configurePreset": "release"
     },
+    {
+      "name": "dev",
+      "configurePreset": "dev"
+    },
     {
       "name": "debug",
       "configurePreset": "debug"
@@ -81,6 +97,11 @@
       "configurePreset": "release",
       "output": {"outputOnFailure": true, "shortProgress": true}
     },
+    {
+      "name": "dev",
+      "configurePreset": "dev",
+      "output": {"outputOnFailure": true, "shortProgress": true}
+    },
     {
       "name": "debug",
       "configurePreset": "debug",

doc/make/index.md

@@ -30,6 +30,9 @@ cd lean4
 cmake --preset release
 make -C build/release -j$(nproc || sysctl -n hw.logicalcpu)
 ```
+
+For development, `cmake --preset dev` is recommended instead.
+
 You can replace `$(nproc || sysctl -n hw.logicalcpu)` with the desired parallelism amount.
 
 The above commands will compile the Lean library and binaries into the

script/release_checklist.py

@@ -311,16 +311,16 @@ def check_cmake_version(repo_url, branch, version_major, version_minor, github_t
         print(f"  ❌ Could not retrieve {cmake_file_path} from {branch}")
         return False
 
-    expected_lines = [
-        f"set(LEAN_VERSION_MAJOR {version_major})",
-        f"set(LEAN_VERSION_MINOR {version_minor})",
-        f"set(LEAN_VERSION_PATCH 0)",
-        f"set(LEAN_VERSION_IS_RELEASE 1)"
+    expected_patterns = [
+        (f"LEAN_VERSION_MAJOR", rf"^set\(LEAN_VERSION_MAJOR\s+{version_major}[\s)]", f"set(LEAN_VERSION_MAJOR {version_major} ...)"),
+        (f"LEAN_VERSION_MINOR", rf"^set\(LEAN_VERSION_MINOR\s+{version_minor}[\s)]", f"set(LEAN_VERSION_MINOR {version_minor} ...)"),
+        (f"LEAN_VERSION_PATCH", rf"^set\(LEAN_VERSION_PATCH\s+0[\s)]", f"set(LEAN_VERSION_PATCH 0 ...)"),
+        (f"LEAN_VERSION_IS_RELEASE", rf"^set\(LEAN_VERSION_IS_RELEASE\s+1[\s)]", f"set(LEAN_VERSION_IS_RELEASE 1 ...)"),
     ]
 
-    for line in expected_lines:
-        if not any(l.strip().startswith(line) for l in content.splitlines()):
-            print(f"  ❌ Missing or incorrect line in {cmake_file_path}: {line}")
+    for name, pattern, display in expected_patterns:
+        if not any(re.match(pattern, l.strip()) for l in content.splitlines()):
+            print(f"  ❌ Missing or incorrect line in {cmake_file_path}: {display}")
             return False
 
     print(f"  ✅ CMake version settings are correct in {cmake_file_path}")
@@ -343,11 +343,11 @@ def check_stage0_version(repo_url, branch, version_major, version_minor, github_
     for line in content.splitlines():
         stripped = line.strip()
         if stripped.startswith("set(LEAN_VERSION_MAJOR "):
-            actual = stripped.split()[-1].rstrip(")")
+            actual = stripped.split()[1].rstrip(")")
             if actual != str(version_major):
                 errors.append(f"LEAN_VERSION_MAJOR: expected {version_major}, found {actual}")
         elif stripped.startswith("set(LEAN_VERSION_MINOR "):
-            actual = stripped.split()[-1].rstrip(")")
+            actual = stripped.split()[1].rstrip(")")
             if actual != str(version_minor):
                 errors.append(f"LEAN_VERSION_MINOR: expected {version_minor}, found {actual}")
 

src/CMakeLists.txt

@@ -80,6 +80,7 @@ option(CCACHE "use ccache" ON)
 option(SPLIT_STACK "SPLIT_STACK" OFF)
 # When OFF we disable LLVM support
 option(LLVM "LLVM" OFF)
+option(STRIP_BINARIES "Strip produced binaries" ON)
 
 # When ON we include githash in the version string
 option(USE_GITHASH "GIT_HASH" ON)

src/Init/Data/Ord/String.lean

@@ -9,7 +9,7 @@ prelude
 public import Init.Data.Order.Ord
 public import Init.Data.String.Basic
 import Init.Data.Char.Lemmas
-import Init.Data.String.Lemmas
+import Init.Data.String.Lemmas.StringOrder
 
 public section
 

src/Init/Data/String/Iter/Intercalate.lean

@@ -17,6 +17,7 @@ namespace Std
 /--
 Appends all the elements in the iterator, in order.
 -/
+@[inline]
 public def Iter.joinString {α β : Type} [Iterator α Id β] [ToString β]
     (it : Std.Iter (α := α) β) : String :=
   (it.map toString).fold (init := "") (· ++ ·)

src/Init/Data/String/Lemmas.lean

@@ -20,49 +20,4 @@ public import Init.Data.String.Lemmas.Intercalate
 public import Init.Data.String.Lemmas.Iter
 public import Init.Data.String.Lemmas.Hashable
 public import Init.Data.String.Lemmas.TakeDrop
-import Init.Data.Order.Lemmas
-public import Init.Data.String.Basic
-import Init.Data.Char.Lemmas
-import Init.Data.Char.Order
-import Init.Data.List.Lex
-
-public section
-
-open Std
-
-namespace String
-
-@[deprecated toList_inj (since := "2025-10-30")]
-protected theorem data_eq_of_eq {a b : String} (h : a = b) : a.toList = b.toList :=
-  h ▸ rfl
-@[deprecated toList_inj (since := "2025-10-30")]
-protected theorem ne_of_data_ne {a b : String} (h : a.toList ≠ b.toList) : a ≠ b := by
-  simpa [← toList_inj]
-
-@[simp] protected theorem not_le {a b : String} : ¬ a ≤ b ↔ b < a := Decidable.not_not
-@[simp] protected theorem not_lt {a b : String} : ¬ a < b ↔ b ≤ a := Iff.rfl
-@[simp] protected theorem le_refl (a : String) : a ≤ a := List.le_refl _
-@[simp] protected theorem lt_irrefl (a : String) : ¬ a < a := List.lt_irrefl _
-
-attribute [local instance] Char.notLTTrans Char.ltTrichotomous Char.ltAsymm
-
-protected theorem le_trans {a b c : String} : a ≤ b → b ≤ c → a ≤ c := List.le_trans
-protected theorem lt_trans {a b c : String} : a < b → b < c → a < c := List.lt_trans
-protected theorem le_total (a b : String) : a ≤ b ∨ b ≤ a := List.le_total _ _
-protected theorem le_antisymm {a b : String} : a ≤ b → b ≤ a → a = b := fun h₁ h₂ => String.ext (List.le_antisymm (as := a.toList) (bs := b.toList) h₁ h₂)
-protected theorem lt_asymm {a b : String} (h : a < b) : ¬ b < a := List.lt_asymm h
-protected theorem ne_of_lt {a b : String} (h : a < b) : a ≠ b := by
-  have := String.lt_irrefl a
-  intro h; subst h; contradiction
-
-instance instIsLinearOrder : IsLinearOrder String := by
-  apply IsLinearOrder.of_le
-  case le_antisymm => constructor; apply String.le_antisymm
-  case le_trans => constructor; apply String.le_trans
-  case le_total => constructor; apply String.le_total
-
-instance : LawfulOrderLT String where
-  lt_iff a b := by
-    simp [← String.not_le, Decidable.imp_iff_not_or, Std.Total.total]
-
-end String
+public import Init.Data.String.Lemmas.StringOrder

src/Init/Data/String/Lemmas/Pattern/Basic.lean

@@ -40,7 +40,7 @@ framework.
 /--
 This data-carrying typeclass is used to give semantics to a pattern type that implements
 {name}`ForwardPattern` and/or {name}`ToForwardSearcher` by providing an abstract, not necessarily
-decidable {name}`PatternModel.Matches` predicate that implementates of {name}`ForwardPattern`
+decidable {name}`PatternModel.Matches` predicate that implementations of {name}`ForwardPattern`
 and {name}`ToForwardSearcher` can be validated against.
 
 Correctness results for generic functions relying on the pattern infrastructure, for example the
@@ -151,7 +151,7 @@ theorem IsLongestMatch.le_of_isMatch {pat : ρ} [PatternModel pat] {s : Slice} {
 
 /--
 Predicate stating that the region between the start of the slice {name}`s` and the position
-{name}`pos` matches the patten {name}`pat`, and that there is no longer match starting at the
+{name}`pos` matches the pattern {name}`pat`, and that there is no longer match starting at the
 beginning of the slice. This is what a correct matcher should match.
 
 In some cases, being a match and being a longest match will coincide, see
@@ -228,7 +228,7 @@ theorem isLongestRevMatch_iff_isRevMatch {ρ : Type} (pat : ρ) [PatternModel pa
   exact ht₅ (NoSuffixPatternModel.eq_empty _ _ ht₂ (ht₅'' ▸ ht₂'))
 
 /--
-Predicate stating that the slice formed by {name}`startPos` and {name}`endPos` contains is a match
+Predicate stating that the slice formed by {name}`startPos` and {name}`endPos` contains a match
 of {name}`pat` in {name}`s` and it is longest among matches starting at {name}`startPos`.
 -/
 structure IsLongestMatchAt (pat : ρ) [PatternModel pat] {s : Slice} (startPos endPos : s.Pos) : Prop where
@@ -411,7 +411,7 @@ theorem not_revMatchesAt_startPos {pat : ρ} [PatternModel pat] {s : Slice} :
   intro h
   simpa [← Pos.ofSliceTo_inj] using h.ne_endPos
 
-theorem revMatchesAt_iff_revMatchesAt_ofSliceto {pat : ρ} [PatternModel pat] {s : Slice} {base : s.Pos}
+theorem revMatchesAt_iff_revMatchesAt_ofSliceTo {pat : ρ} [PatternModel pat] {s : Slice} {base : s.Pos}
     {pos : (s.sliceTo base).Pos} : RevMatchesAt pat pos ↔ RevMatchesAt pat (Pos.ofSliceTo pos) := by
   simp only [revMatchesAt_iff_exists_isLongestRevMatchAt]
   constructor
@@ -505,8 +505,8 @@ theorem LawfulForwardPatternModel.skipPrefix?_eq_none_iff {ρ : Type} {pat : ρ}
 /--
 Predicate stating compatibility between {name}`PatternModel` and {name}`BackwardPattern`.
 
-This extends {name}`LawfulForwardPattern`, but it is much stronger because it forces the
-{name}`ForwardPattern` to match the longest prefix of the given slice that matches the property
+This extends {name}`LawfulBackwardPattern`, but it is much stronger because it forces the
+{name}`BackwardPattern` to match the longest prefix of the given slice that matches the property
 supplied by the {name}`PatternModel` instance.
 -/
 class LawfulBackwardPatternModel {ρ : Type} (pat : ρ) [BackwardPattern pat]

src/Init/Data/String/Lemmas/Pattern/TakeDrop/Pred.lean

@@ -65,7 +65,7 @@ theorem startsWith_prop_eq_head? {P : Char → Prop} [DecidablePred P] {s : Slic
     s.startsWith P = s.copy.toList.head?.any (decide <| P ·) := by
   simp [startsWith_prop_eq_startsWith_decide, startsWith_bool_eq_head?]
 
-theorem eq_append_of_dropPrefix_prop_eq_some {P : Char → Prop} [DecidablePred P] {s res : Slice} (h : s.dropPrefix? P = some res) :
+theorem eq_append_of_dropPrefix?_prop_eq_some {P : Char → Prop} [DecidablePred P] {s res : Slice} (h : s.dropPrefix? P = some res) :
     ∃ c, s.copy = singleton c ++ res.copy ∧ P c := by
   rw [dropPrefix?_prop_eq_dropPrefix?_decide] at h
   simpa using eq_append_of_dropPrefix?_bool_eq_some h
@@ -162,7 +162,7 @@ theorem startsWith_prop_eq_head? {P : Char → Prop} [DecidablePred P] {s : Stri
 theorem eq_append_of_dropPrefix?_prop_eq_some {P : Char → Prop} [DecidablePred P] {s : String} {res : Slice}
     (h : s.dropPrefix? P = some res) : ∃ c, s = singleton c ++ res.copy ∧ P c := by
   rw [dropPrefix?_eq_dropPrefix?_toSlice] at h
-  simpa using Slice.eq_append_of_dropPrefix_prop_eq_some h
+  simpa using Slice.eq_append_of_dropPrefix?_prop_eq_some h
 
 theorem skipSuffix?_bool_eq_some_iff {p : Char → Bool} {s : String} {pos : s.Pos} :
     s.skipSuffix? p = some pos ↔ ∃ h, pos = s.endPos.prev h ∧ p ((s.endPos.prev h).get (by simp)) = true := by

src/Init/Data/String/Lemmas/StringOrder.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+
+prelude
+public import Init.Data.String.Basic
+public import Init.Data.Order.Classes
+import Init.Data.List.Lex
+import Init.Data.Char.Lemmas
+import Init.Data.Char.Order
+import Init.Data.Order.Factories
+import Init.Data.Order.Lemmas
+
+public section
+
+open Std
+
+namespace String
+
+@[simp] protected theorem not_le {a b : String} : ¬ a ≤ b ↔ b < a := Decidable.not_not
+@[simp] protected theorem not_lt {a b : String} : ¬ a < b ↔ b ≤ a := Iff.rfl
+@[simp] protected theorem le_refl (a : String) : a ≤ a := List.le_refl _
+@[simp] protected theorem lt_irrefl (a : String) : ¬ a < a := List.lt_irrefl _
+
+attribute [local instance] Char.notLTTrans Char.ltTrichotomous Char.ltAsymm
+
+protected theorem le_trans {a b c : String} : a ≤ b → b ≤ c → a ≤ c := List.le_trans
+protected theorem lt_trans {a b c : String} : a < b → b < c → a < c := List.lt_trans
+protected theorem le_total (a b : String) : a ≤ b ∨ b ≤ a := List.le_total _ _
+protected theorem le_antisymm {a b : String} : a ≤ b → b ≤ a → a = b := fun h₁ h₂ => String.ext (List.le_antisymm (as := a.toList) (bs := b.toList) h₁ h₂)
+protected theorem lt_asymm {a b : String} (h : a < b) : ¬ b < a := List.lt_asymm h
+protected theorem ne_of_lt {a b : String} (h : a < b) : a ≠ b := by
+  have := String.lt_irrefl a
+  intro h; subst h; contradiction
+
+instance instIsLinearOrder : IsLinearOrder String := by
+  apply IsLinearOrder.of_le
+  case le_antisymm => constructor; apply String.le_antisymm
+  case le_trans => constructor; apply String.le_trans
+  case le_total => constructor; apply String.le_total
+
+instance : LawfulOrderLT String where
+  lt_iff a b := by
+    simp [← String.not_le, Decidable.imp_iff_not_or, Std.Total.total]
+
+end String

src/Init/Data/String/Slice.lean

@@ -706,14 +706,14 @@ Returns {name}`none` otherwise.
 This function is generic over all currently supported patterns.
 -/
 @[inline]
-def Pos.revSkip? {s : Slice} (pos : s.Pos) (pat : ρ) [ForwardPattern pat] : Option s.Pos :=
-  ((s.sliceFrom pos).skipPrefix? pat).map Pos.ofSliceFrom
+def Pos.revSkip? {s : Slice} (pos : s.Pos) (pat : ρ) [BackwardPattern pat] : Option s.Pos :=
+  ((s.sliceFrom pos).skipSuffix? pat).map Pos.ofSliceFrom
 
 /--
 If {name}`pat` matches a suffix of {name}`s`, returns the remainder. Returns {name}`none` otherwise.
 
 Use {name (scope := "Init.Data.String.Slice")}`String.Slice.dropSuffix` to return the slice
-unchanged when {name}`pat` does not match a prefix.
+unchanged when {name}`pat` does not match a suffix.
 
 This function is generic over all currently supported patterns.
 
@@ -775,7 +775,7 @@ def Pos.revSkipWhile {s : Slice} (pos : s.Pos) (pat : ρ) [BackwardPattern pat]
 termination_by pos.down
 
 /--
-Returns the position a the start of the longest suffix of {name}`s` for which {name}`pat` matches
+Returns the position at the start of the longest suffix of {name}`s` for which {name}`pat` matches
 (potentially repeatedly).
 -/
 @[inline]

src/Init/Data/String/TakeDrop.lean

@@ -314,7 +314,7 @@ Returns {name}`none` otherwise.
 This function is generic over all currently supported patterns.
 -/
 @[inline]
-def Pos.revSkip? {s : String} (pos : s.Pos) (pat : ρ) [ForwardPattern pat] : Option s.Pos :=
+def Pos.revSkip? {s : String} (pos : s.Pos) (pat : ρ) [BackwardPattern pat] : Option s.Pos :=
   (pos.toSlice.revSkip? pat).map Pos.ofToSlice
 
 /--
@@ -461,7 +461,7 @@ def dropPrefix? (s : String) (pat : ρ) [ForwardPattern pat] : Option String.Sli
 If {name}`pat` matches a suffix of {name}`s`, returns the remainder. Returns {name}`none` otherwise.
 
 Use {name (scope := "Init.Data.String.TakeDrop")}`String.dropSuffix` to return the slice
-unchanged when {name}`pat` does not match a prefix.
+unchanged when {name}`pat` does not match a suffix.
 
 This is a cheap operation because it does not allocate a new string to hold the result.
 To convert the result into a string, use {name}`String.Slice.copy`.

src/Init/Omega/LinearCombo.lean

@@ -36,9 +36,6 @@ private local instance : ToString Int where
 private local instance : Repr Int where
   reprPrec i prec := if i < 0 then Repr.addAppParen (toString i) prec else toString i
 
-private local instance : Append String where
-  append := String.Internal.append
-
 /-- Internal representation of a linear combination of atoms, and a constant term. -/
 structure LinearCombo where
   /-- Constant term. -/

src/Lean/Data/Trie.lean

@@ -60,7 +60,7 @@ instance : EmptyCollection (Trie α) :=
 instance : Inhabited (Trie α) where
   default := empty
 
-/-- Insert or update the value at a the given key `s`.  -/
+/-- Insert or update the value at the given key `s`.  -/
 partial def upsert (t : Trie α) (s : String) (f : Option α → α) : Trie α :=
   let rec insertEmpty (i : Nat) : Trie α :=
     if h : i < s.utf8ByteSize then
@@ -100,7 +100,7 @@ partial def upsert (t : Trie α) (s : String) (f : Option α → α) : Trie α :
         node (f v) cs ts
   loop 0 t
 
-/-- Inserts a value at a the given key `s`, overriding an existing value if present. -/
+/-- Inserts a value at the given key `s`, overriding an existing value if present. -/
 partial def insert (t : Trie α) (s : String) (val : α) : Trie α :=
   upsert t s (fun _ => val)
 

src/Lean/Meta.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Basic
+public import Lean.Meta.HasAssignableMVar
 public import Lean.Meta.LevelDefEq
 public import Lean.Meta.WHNF
 public import Lean.Meta.InferType

src/Lean/Meta/AppBuilder.lean

@@ -8,6 +8,7 @@ prelude
 public import Lean.Meta.SynthInstance
 public import Lean.Meta.DecLevel
 import Lean.Meta.CtorRecognizer
+public import Lean.Meta.HasAssignableMVar
 import Lean.Structure
 import Init.Omega
 public section

src/Lean/Meta/HasAssignableMVar.lean

@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+
+prelude
+public import Lean.Meta.Basic
+
+public section
+
+open Lean
+
+namespace Lean.Meta
+
+def isLevelMVarAssignable (mvarId : LMVarId) : MetaM Bool := do
+  let mctx ← getMCtx
+  match mctx.lDepth.find? mvarId with
+  | some d => return d >= mctx.levelAssignDepth
+  | _      => panic! s!"unknown universe metavariable {mvarId.name}"
+
+def hasAssignableLevelMVar : Level → MetaM Bool
+  | .succ lvl       => pure lvl.hasMVar <&&> hasAssignableLevelMVar lvl
+  | .max lvl₁ lvl₂  => (pure lvl₁.hasMVar <&&> hasAssignableLevelMVar lvl₁) <||> (pure lvl₂.hasMVar <&&> hasAssignableLevelMVar lvl₂)
+  | .imax lvl₁ lvl₂ => (pure lvl₁.hasMVar <&&> hasAssignableLevelMVar lvl₁) <||> (pure lvl₂.hasMVar <&&> hasAssignableLevelMVar lvl₂)
+  | .mvar mvarId    => isLevelMVarAssignable mvarId
+  | .zero           => return false
+  | .param _        => return false
+
+/-- Return `true` iff expression contains a metavariable that can be assigned. -/
+partial def hasAssignableMVar (e : Expr) : MetaM Bool :=
+  if !e.hasMVar then
+    return false
+  else
+    go e |>.run' {}
+where
+  go (e : Expr) : StateRefT ExprSet MetaM Bool :=
+    match e with
+    | .const _ lvls    => lvls.anyM (liftM <| hasAssignableLevelMVar ·)
+    | .sort lvl        => liftM <| hasAssignableLevelMVar lvl
+    | .app f a         => do checkSystem "hasAssignableMVar"; visit f <||> visit a
+    | .letE _ t v b _  => do checkSystem "hasAssignableMVar"; visit t <||> visit v <||> visit b
+    | .forallE _ d b _ => do checkSystem "hasAssignableMVar"; visit d <||> visit b
+    | .lam _ d b _     => do checkSystem "hasAssignableMVar"; visit d <||> visit b
+    | .fvar _          => return false
+    | .bvar _          => return false
+    | .lit _           => return false
+    | .mdata _ e       => visit e
+    | .proj _ _ e      => visit e
+    | .mvar mvarId     => mvarId.isAssignable
+  visit (e : Expr) : StateRefT ExprSet MetaM Bool := do
+    if !e.hasMVar then return false
+    if (← get).contains e then return false
+    modify fun s => s.insert e
+    go e
+
+end Lean.Meta
+
+end

src/Lean/Meta/LevelDefEq.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Lean.Util.CollectMVars
 public import Lean.Meta.DecLevel
+public import Lean.Meta.HasAssignableMVar
 
 public section
 

src/Lean/Meta/Sym/Pattern.lean

@@ -18,6 +18,7 @@ import Lean.Meta.Sym.AlphaShareBuilder
 import Lean.Meta.Sym.Offset
 import Lean.Meta.Sym.Eta
 import Lean.Meta.Sym.Util
+import Lean.Meta.HasAssignableMVar
 import Init.Data.List.MapIdx
 import Init.Data.Nat.Linear
 import Std.Do.Triple.Basic

src/Lean/Meta/Tactic/Grind/EMatch.lean

@@ -14,6 +14,7 @@ import Lean.Meta.Tactic.Grind.SynthInstance
 import Lean.Meta.Tactic.Grind.Simp
 import Init.Grind.Util
 import Init.Omega
+public import Lean.Meta.HasAssignableMVar
 public section
 namespace Lean.Meta.Grind
 namespace EMatch

src/Lean/Meta/Tactic/Simp/Rewrite.lean

@@ -12,6 +12,7 @@ public import Lean.Meta.Tactic.Simp.Arith
 public import Lean.Meta.Tactic.Simp.Attr
 public import Lean.Meta.BinderNameHint
 import Lean.Meta.WHNF
+public import Lean.Meta.HasAssignableMVar
 public section
 namespace Lean.Meta.Simp
 /--

src/Lean/MetavarContext.lean

@@ -444,12 +444,6 @@ def _root_.Lean.MVarId.isAssignedOrDelayedAssigned [Monad m] [MonadMCtx m] (mvar
   let mctx ← getMCtx
   return mctx.eAssignment.contains mvarId || mctx.dAssignment.contains mvarId
 
-def isLevelMVarAssignable [Monad m] [MonadMCtx m] (mvarId : LMVarId) : m Bool := do
-  let mctx ← getMCtx
-  match mctx.lDepth.find? mvarId with
-  | some d => return d >= mctx.levelAssignDepth
-  | _      => panic! s!"unknown universe metavariable {mvarId.name}"
-
 def MetavarContext.getDecl (mctx : MetavarContext) (mvarId : MVarId) : MetavarDecl :=
   match mctx.decls.find? mvarId with
   | some decl => decl
@@ -484,30 +478,6 @@ def hasAssignedMVar [Monad m] [MonadMCtx m] : Expr → m Bool
   | .proj _ _ e      => pure e.hasMVar <&&> hasAssignedMVar e
   | .mvar mvarId     => mvarId.isAssigned <||> mvarId.isDelayedAssigned
 
-/-- Return true iff the given level contains a metavariable that can be assigned. -/
-def hasAssignableLevelMVar [Monad m] [MonadMCtx m] : Level → m Bool
-  | .succ lvl       => pure lvl.hasMVar <&&> hasAssignableLevelMVar lvl
-  | .max lvl₁ lvl₂  => (pure lvl₁.hasMVar <&&> hasAssignableLevelMVar lvl₁) <||> (pure lvl₂.hasMVar <&&> hasAssignableLevelMVar lvl₂)
-  | .imax lvl₁ lvl₂ => (pure lvl₁.hasMVar <&&> hasAssignableLevelMVar lvl₁) <||> (pure lvl₂.hasMVar <&&> hasAssignableLevelMVar lvl₂)
-  | .mvar mvarId    => isLevelMVarAssignable mvarId
-  | .zero           => return false
-  | .param _        => return false
-
-/-- Return `true` iff expression contains a metavariable that can be assigned. -/
-def hasAssignableMVar [Monad m] [MonadMCtx m] : Expr → m Bool
-  | .const _ lvls    => lvls.anyM hasAssignableLevelMVar
-  | .sort lvl        => hasAssignableLevelMVar lvl
-  | .app f a         => (pure f.hasMVar <&&> hasAssignableMVar f) <||> (pure a.hasMVar <&&> hasAssignableMVar a)
-  | .letE _ t v b _  => (pure t.hasMVar <&&> hasAssignableMVar t) <||> (pure v.hasMVar <&&> hasAssignableMVar v) <||> (pure b.hasMVar <&&> hasAssignableMVar b)
-  | .forallE _ d b _ => (pure d.hasMVar <&&> hasAssignableMVar d) <||> (pure b.hasMVar <&&> hasAssignableMVar b)
-  | .lam _ d b _     => (pure d.hasMVar <&&> hasAssignableMVar d) <||> (pure b.hasMVar <&&> hasAssignableMVar b)
-  | .fvar _          => return false
-  | .bvar _          => return false
-  | .lit _           => return false
-  | .mdata _ e       => pure e.hasMVar <&&> hasAssignableMVar e
-  | .proj _ _ e      => pure e.hasMVar <&&> hasAssignableMVar e
-  | .mvar mvarId     => mvarId.isAssignable
-
 /--
   Add `mvarId := u` to the universe metavariable assignment.
   This method does not check whether `mvarId` is already assigned, nor does it check whether

src/Std/Data/String/ToInt.lean

@@ -183,7 +183,8 @@ public theorem toInt?_repr (a : Int) : a.repr.toInt? = some a := by
   rw [repr_eq_if]
   split <;> (simp; omega)
 
-public theorem isInt?_repr (a : Int) : a.repr.isInt = true := by
+@[simp]
+public theorem isInt_repr (a : Int) : a.repr.isInt = true := by
   simp [← String.isSome_toInt?]
 
 public theorem repr_injective {a b : Int} (h : Int.repr a = Int.repr b) : a = b := by

src/Std/Internal/UV/System.lean

@@ -174,19 +174,19 @@ opaque osEnviron : IO (Array (String × String))
 Gets the value of an environment variable.
 -/
 @[extern "lean_uv_os_getenv"]
-opaque osGetenv : String → IO (Option String)
+opaque osGetenv : @& String → IO (Option String)
 
 /--
 Sets the value of an environment variable.
 -/
 @[extern "lean_uv_os_setenv"]
-opaque osSetenv : String → String → IO Unit
+opaque osSetenv : @& String → @& String → IO Unit
 
 /--
 Unsets an environment variable.
 -/
 @[extern "lean_uv_os_unsetenv"]
-opaque osUnsetenv : String → IO Unit
+opaque osUnsetenv : @& String → IO Unit
 
 /--
 Gets the hostname of the machine.

src/Std/Time/Internal/Bounded.lean

@@ -239,7 +239,7 @@ def ofFin' {lo : Nat} (fin : Fin (Nat.succ hi)) (h : lo ≤ hi) : Bounded.LE lo
     else ofNat' lo (And.intro (Nat.le_refl lo) h)
 
 /--
-Creates a new `Bounded.LE` using a the modulus of a number.
+Creates a new `Bounded.LE` using the modulus of a number.
 -/
 @[inline]
 def byEmod (b : Int) (i : Int) (hi : i > 0) : Bounded.LE 0 (i - 1) := by
@@ -252,7 +252,7 @@ def byEmod (b : Int) (i : Int) (hi : i > 0) : Bounded.LE 0 (i - 1) := by
     exact Int.emod_lt_of_pos b hi
 
 /--
-Creates a new `Bounded.LE` using a the Truncating modulus of a number.
+Creates a new `Bounded.LE` using the Truncating modulus of a number.
 -/
 @[inline]
 def byMod (b : Int) (i : Int) (hi : 0 < i) : Bounded.LE (- (i - 1)) (i - 1) := by

src/lakefile.toml.in

@@ -77,7 +77,7 @@ globs = ["Lake.*"]
 defaultFacets = ["static", "static.export"]
 # Load the previous stage's lake native code into lake's build process in order to prevent ABI
 # breakages from affecting bootstrapping.
-moreLeanArgs = ["--plugin", "${PREV_STAGE}/lib/lean/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}"]
+moreLeanArgs = ["--plugin", "${PREV_STAGE}/${CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}"]
 
 [[lean_lib]]
 name = "LakeMain"

src/runtime/uv/system.cpp

@@ -31,7 +31,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_process_title() {
     return lean_io_result_mk_ok(lean_title);
 }
 
-// Std.Internal.UV.System.setProcessTitle : String → IO Unit
+// Std.Internal.UV.System.setProcessTitle : @& String → IO Unit
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_set_process_title(b_obj_arg title) {
     const char* title_str = lean_string_cstr(title);
     if (strlen(title_str) != lean_string_size(title) - 1) {
@@ -124,7 +124,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_cwd() {
     return lean_io_result_mk_ok(lean_cwd);
 }
 
-// Std.Internal.UV.System.chdir : String → IO Unit
+// Std.Internal.UV.System.chdir : @& String → IO Unit
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_chdir(b_obj_arg path) {
     const char* path_str = lean_string_cstr(path);
     if (strlen(path_str) != lean_string_size(path) - 1) {
@@ -271,7 +271,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_environ() {
     return lean_io_result_mk_ok(env_array);
 }
 
-// Std.Internal.UV.System.osGetenv : String → IO (Option String)
+// Std.Internal.UV.System.osGetenv : @& String → IO (Option String)
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getenv(b_obj_arg name) {
     const char* name_str = lean_string_cstr(name);
     if (strlen(name_str) != lean_string_size(name) - 1) {
@@ -313,7 +313,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getenv(b_obj_arg name) {
 }
 
 
-// Std.Internal.UV.System.osSetenv : String → String → IO Unit
+// Std.Internal.UV.System.osSetenv : @& String → @& String → IO Unit
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setenv(b_obj_arg name, b_obj_arg value) {
     const char* name_str = lean_string_cstr(name);
     const char* value_str = lean_string_cstr(value);
@@ -333,7 +333,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setenv(b_obj_arg name, b_obj_arg
     return lean_io_result_mk_ok(lean_box(0));
 }
 
-// Std.Internal.UV.System.osUnsetenv : String → IO Unit
+// Std.Internal.UV.System.osUnsetenv : @& String → IO Unit
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_unsetenv(b_obj_arg name) {
     const char* name_str = lean_string_cstr(name);
     if (strlen(name_str) != lean_string_size(name) - 1) {
@@ -641,21 +641,21 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_environ() {
     );
 }
 
-// Std.Internal.UV.System.osGetenv : String → IO (Option String)
+// Std.Internal.UV.System.osGetenv : @& String → IO (Option String)
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getenv(b_obj_arg name) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-// Std.Internal.UV.System.osSetenv : String → String → IO Unit
+// Std.Internal.UV.System.osSetenv : @& String → @& String → IO Unit
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setenv(b_obj_arg name, b_obj_arg value) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-// Std.Internal.UV.System.osUnsetenv : String → IO Unit
+// Std.Internal.UV.System.osUnsetenv : @& String → IO Unit
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_unsetenv(b_obj_arg name) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")

src/stdlib.make.in

@@ -162,7 +162,7 @@ else
 	  -Wl,--whole-archive ${LIB}/temp/Lean.*o.export ${LIB}/temp/libleanshell.a -Wl,--no-whole-archive -Wl,--start-group -lInit -lStd -lLean -lleancpp -Wl,--end-group ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS}
 endif
 endif
-ifeq "${CMAKE_BUILD_TYPE}" "Release"
+ifeq "${STRIP_BINARIES}" "ON"
 ifeq "${CMAKE_SYSTEM_NAME}" "Linux"
 # We only strip like this on Linux for now as our other platforms already seem to exclude the
 # unexported symbols by default

tests/bench/mvcgen/sym/cases/Cases.lean

@@ -3,6 +3,7 @@ import Cases.AddSubCancelDeep
 import Cases.AddSubCancelSimp
 import Cases.DiteSplit
 import Cases.GetThrowSet
+import Cases.LetBinding
 import Cases.MatchIota
 import Cases.MatchSplit
 import Cases.PurePrecond

tests/bench/mvcgen/sym/cases/Cases/LetBinding.lean

@@ -0,0 +1,37 @@
+import Lean
+import VCGen
+
+open Lean Meta Elab Tactic Sym Std Do SpecAttr
+
+namespace LetBinding
+
+set_option mvcgen.warning false
+
+-- Partially evaluated specs for best performance.
+
+@[spec high]
+theorem Spec.MonadState_get {m ps} [Monad m] [WPMonad m ps] {σ} {Q : PostCond σ (.arg σ ps)} :
+    ⦃fun s => Q.fst s s⦄ get (m := StateT σ m) ⦃Q⦄ := by
+  mvcgen'
+
+@[spec high]
+theorem Spec.MonadStateOf_set {m ps} [Monad m] [WPMonad m ps] {σ} {Q : PostCond PUnit (.arg σ ps)} {s : σ} :
+    ⦃fun _ => Q.fst ⟨⟩ s⦄ set (m := StateT σ m) s ⦃Q⦄ := by
+  mvcgen'
+
+def step (v : Nat) : StateM Nat Unit := do
+  let s ← get
+  -- Pure let binding: `let offset := ...` produces a letE node in the elaborated term
+  let offset := v + 1
+  set (s + offset)
+  let s ← get
+  set (s - offset)
+
+def loop (n : Nat) : StateM Nat Unit := do
+  match n with
+  | 0 => pure ()
+  | n+1 => step n; loop n
+
+def Goal (n : Nat) : Prop := ∀ post, ⦃post⦄ loop n ⦃⇓_ => post⦄
+
+end LetBinding

tests/bench/mvcgen/sym/lib/VCGen.lean

@@ -720,12 +720,22 @@ The function performs the following steps in order:
 5. **Proj/beta reduction**: Reduce `Prod.fst`/`Prod.snd` projections and beta redexes in
    both `H` and `T` (e.g., `(fun _ => T, Q.snd).fst s` → `T`).
 6. **Syntactic rfl**: If `T` is not a `PredTrans.apply`, try closing by `SPred.entails.refl`.
-7. **Let-zeta**: Zeta-reduce let-expressions in the program head.
+7. **Let-hoisting**: Hoist let-expressions from the program head to the goal target.
+7a. **Let-zeta/intro**: If the target starts with `let`, zeta immediately if duplicable, else
+    introduce into the local context via `introsSimp`.
+7b. **Fvar zeta**: Unfold local let-bound fvars on demand when they appear as the program head.
 8. **Iota reduction**: Reduce matchers/recursors with concrete discriminants.
 9. **ite/dite/match splitting**: Apply the appropriate split backward rule.
 10. **Spec application**: Look up a registered `@[spec]` theorem (triple or simp) and apply
     its cached backward rule.
 -/
+
+private meta def isDuplicable (e : Expr) : Bool := match e with
+  | .bvar .. | .mvar .. | .fvar .. | .const .. | .lit .. | .sort .. => true
+  | .mdata _ e | .proj _ _ e => isDuplicable e
+  | .lam .. | .forallE .. | .letE .. => false
+  | .app .. => e.isAppOf ``OfNat.ofNat
+
 meta def solve (goal : MVarId) : VCGenM SolveResult := goal.withContext do
   let target ← goal.getType
   trace[Elab.Tactic.Do.vcgen] "target: {target}"
@@ -738,6 +748,19 @@ meta def solve (goal : MVarId) : VCGenM SolveResult := goal.withContext do
     let IntrosResult.goal _ goal ← introsSimp goal | throwError "Failed to introduce binders for {target}"
     return .goals [goal]
 
+  if target.isLet then
+    if isDuplicable target.letValue! then
+      trace[Elab.Tactic.Do.vcgen] "let-zeta-dup: {target.letName!}"
+      -- Zeta right away: substitute value into body with sharing
+      let target' ← Sym.instantiateRevBetaS target.letBody! #[target.letValue!]
+      return .goals [← goal.replaceTargetDefEq target']
+    else
+      trace[Elab.Tactic.Do.vcgen] "let-intro: {target.letName!}"
+      -- Introduce let binding into the local context with proper sharing
+      let IntrosResult.goal _ goal ← introsSimp goal
+        | throwError "Failed to introduce let binding"
+      return .goals [goal]
+
   let f := target.getAppFn
   if f.isConstOf ``Triple then
     let goal ← tripleOfWP goal
@@ -807,11 +830,15 @@ meta def solve (goal : MVarId) : VCGenM SolveResult := goal.withContext do
     let target ← mkAppS₃ ent σs H T
     goal.replaceTargetDefEq target
 
-  -- Zeta let-expressions
-  if let .letE _x _ty val body _nonDep := f then
-    let body' ← Sym.instantiateRevBetaS body #[val]
-    let e' ← mkAppRevS body' e.getAppRevArgs
-    return .goals [← replaceProgDefEq e']
+  -- Let-expressions: hoist to top of goal
+  if let .letE x ty val body nonDep := f then
+    trace[Elab.Tactic.Do.vcgen] "let-hoist: {x}"
+    let e' ← mkAppRevS body e.getAppRevArgs  -- body still has #0 for the let-bound var
+    let wp' ← Sym.Internal.mkAppS₅ wpConst m ps instWP α e'
+    let T' ← mkAppNS head (args.set! 2 wp')
+    let target' ← mkAppS₃ ent σs H T'
+    let hoisted := Expr.letE x ty val target' nonDep
+    return .goals [← goal.replaceTargetDefEq hoisted]
 
   -- Split ite/dite/match
   if let some info ← liftMetaM <| Lean.Elab.Tactic.Do.getSplitInfo? e then
@@ -823,6 +850,13 @@ meta def solve (goal : MVarId) : VCGenM SolveResult := goal.withContext do
       | throwError "Failed to apply split rule for {indentExpr e}"
     return .goals goals
 
+  -- Zeta-unfold local let bindings on demand
+  if let some fvarId := f.fvarId? then
+    if let some val ← fvarId.getValue? then
+      trace[Elab.Tactic.Do.vcgen] "fvar-zeta: {(← fvarId.getUserName)}"
+      let e' ← shareCommonInc (val.betaRev e.getAppRevArgs)
+      return .goals [← replaceProgDefEq e']
+
   -- Apply registered specifications (both triple and simp specs use cached backward rules).
   if f.isConst || f.isFVar then
     trace[Elab.Tactic.Do.vcgen] "Applying a spec for {e}. Excess args: {excessArgs}"

tests/bench/mvcgen/sym/test_vcgen.lean

@@ -35,6 +35,8 @@ set_option maxHeartbeats 10000000
     `(tactic| mvcgen') `(tactic| grind) [10]
   runBenchUsingTactic ``AddSubCancelSimp.Goal [``AddSubCancelSimp.loop, ``AddSubCancelSimp.step]
     `(tactic| mvcgen') `(tactic| grind) [10]
+  runBenchUsingTactic ``LetBinding.Goal [``LetBinding.loop, ``LetBinding.step]
+    `(tactic| mvcgen') `(tactic| grind) [10]
   runBenchUsingTactic ``GetThrowSet.Goal [``GetThrowSet.loop, ``GetThrowSet.step]
     `(tactic| mvcgen') `(tactic| sorry) [10]
   -- `mvcgen' with grind`: grind integrated into VCGen loop
@@ -76,3 +78,14 @@ example : Goal 10 := by
   mvcgen' simplifying_assumptions [Nat.add_assoc]
   case vc11 => trace_state; grind
   all_goals grind
+
+-- Verify that the let-binding code paths are exercised.
+-- `unfold` (unlike `simp only`) preserves letE nodes in the program, exercising:
+-- let-hoist, let-intro (non-duplicable value), and fvar-zeta (let-bound program head).
+-- Run with `set_option trace.Elab.Tactic.Do.vcgen true` to see the traces.
+open LetBinding in
+example : ∀ post, ⦃post⦄ step 5 ⦃⇓_ => post⦄ := by
+  unfold step
+  intro post
+  mvcgen'
+  grind

tests/elab/4595_slowdown.lean

@@ -1,6 +1,8 @@
 -- The final declaration blew up by a factor of about 40x heartbeats on an earlier draft of
 -- https://github.com/leanprover/lean4/pull/4595, so this is here as a regression test.
 
+set_option maxHeartbeats 400000
+
 universe v v₁ v₂ v₃ u u₁ u₂ u₃
 
 section Mathlib.Combinatorics.Quiver.Basic

tests/elab/4595_slowdown.lean.out.expected

@@ -1,12 +1,12 @@
-4595_slowdown.lean:104:14-104:25: warning: declaration uses `sorry`
-4595_slowdown.lean:136:9-136:17: warning: declaration uses `sorry`
-4595_slowdown.lean:154:8-154:16: warning: declaration uses `sorry`
-4595_slowdown.lean:181:8-181:14: warning: declaration uses `sorry`
+4595_slowdown.lean:106:14-106:25: warning: declaration uses `sorry`
+4595_slowdown.lean:138:9-138:17: warning: declaration uses `sorry`
+4595_slowdown.lean:156:8-156:16: warning: declaration uses `sorry`
 4595_slowdown.lean:183:8-183:14: warning: declaration uses `sorry`
-4595_slowdown.lean:186:0-186:8: warning: declaration uses `sorry`
-4595_slowdown.lean:194:8-194:19: warning: declaration uses `sorry`
-4595_slowdown.lean:197:8-197:15: warning: declaration uses `sorry`
-4595_slowdown.lean:207:4-207:13: warning: declaration uses `sorry`
-4595_slowdown.lean:229:8-229:14: warning: declaration uses `sorry`
-4595_slowdown.lean:231:8-231:16: warning: declaration uses `sorry`
-4595_slowdown.lean:233:4-233:11: warning: declaration uses `sorry`
+4595_slowdown.lean:185:8-185:14: warning: declaration uses `sorry`
+4595_slowdown.lean:188:0-188:8: warning: declaration uses `sorry`
+4595_slowdown.lean:196:8-196:19: warning: declaration uses `sorry`
+4595_slowdown.lean:199:8-199:15: warning: declaration uses `sorry`
+4595_slowdown.lean:209:4-209:13: warning: declaration uses `sorry`
+4595_slowdown.lean:231:8-231:14: warning: declaration uses `sorry`
+4595_slowdown.lean:233:8-233:16: warning: declaration uses `sorry`
+4595_slowdown.lean:235:4-235:11: warning: declaration uses `sorry`