perf: correct over-allocated capacity for imported constant hashmaps (#13238)

privateConstantMap capacity was inflated by IR extraConstNames that are
only inserted into const2ModIdx. const2ModIdx capacity included
numPublicConsts even though public constants are never inserted into it.

.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)

.vscode/tasks.json

@@ -11,6 +11,15 @@
 				"isDefault": true
 			}
 		},
+		{
+			"label": "build stage2",
+			"type": "shell",
+			"command": "make -C build/release stage2 -j$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)",
+			"problemMatcher": [],
+			"group": {
+				"kind": "build"
+			}
+		},
 		{
 			"label": "build-old",
 			"type": "shell",

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,17 @@ 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

@@ -8,7 +8,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4 CACHE STRING "")
-set(LEAN_VERSION_MINOR 30 CACHE STRING "")
+set(LEAN_VERSION_MINOR 31 CACHE STRING "")
 set(LEAN_VERSION_PATCH 0 CACHE STRING "")
 set(LEAN_VERSION_IS_RELEASE 0 CACHE STRING "") # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
@@ -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.lean

@@ -40,7 +40,6 @@ public import Init.Grind
 public import Init.GrindInstances
 public import Init.Sym
 public import Init.While
-public import Init.Repeat
 public import Init.Syntax
 public import Init.Internal
 public import Init.Try

src/Init/Data/ByteArray/Basic.lean

@@ -20,12 +20,20 @@ universe u
 
 namespace ByteArray
 
-deriving instance BEq for ByteArray
+@[extern "lean_sarray_dec_eq"]
+def beq (lhs rhs : @& ByteArray) : Bool :=
+  lhs.data == rhs.data
+
+instance : BEq ByteArray where
+  beq := beq
 
 attribute [ext] ByteArray
 
-instance : DecidableEq ByteArray :=
-  fun _ _ => decidable_of_decidable_of_iff ByteArray.ext_iff.symm
+@[extern "lean_sarray_dec_eq"]
+def decEq (lhs rhs : @& ByteArray) : Decidable (lhs = rhs) :=
+  decidable_of_decidable_of_iff ByteArray.ext_iff.symm
+
+instance : DecidableEq ByteArray := decEq
 
 instance : Inhabited ByteArray where
   default := empty

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/Internal/Order.lean

@@ -8,5 +8,4 @@ module
 prelude
 public import Init.Internal.Order.Basic
 public import Init.Internal.Order.Lemmas
-public import Init.Internal.Order.MonadTail
 public import Init.Internal.Order.Tactic

src/Init/Internal/Order/MonadTail.lean

@@ -1,140 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Graf
--/
-module
-
-prelude
-public import Init.Internal.Order.Basic
-import all Init.System.ST  -- for EST.bind in MonadTail instance
-
-set_option linter.missingDocs true
-
-public section
-
-namespace Lean.Order
-
-/--
-A *tail monad* is a monad whose bind operation preserves any suitable ordering of the continuation.
-Specifically, `MonadTail m` asserts that every `m β` carries a chain-complete partial order (CCPO)
-and that `>>=` is monotone in its second (continuation) argument with respect to that order.
-
-This is a weaker requirement than `MonoBind`, which requires monotonicity in both arguments.
-`MonadTail` is sufficient for `partial_fixpoint`-based recursive definitions where the
-recursive call only appears in the continuation (second argument) of `>>=`.
--/
-class MonadTail (m : Type u → Type v) [Bind m] where
-  /-- Every `m β` with `Nonempty β` has a chain-complete partial order. -/
-  instCCPO β [Nonempty β] : CCPO (m β)
-  /-- Bind is monotone in the second (continuation) argument. -/
-  bind_mono_right {a : m α} {f₁ f₂ : α → m β} [Nonempty β] (h : ∀ x, f₁ x ⊑ f₂ x) :
-    a >>= f₁ ⊑ a >>= f₂
-
-attribute [implicit_reducible] MonadTail.instCCPO
-attribute [instance] MonadTail.instCCPO
-
-@[scoped partial_fixpoint_monotone]
-theorem MonadTail.monotone_bind_right
-    (m : Type u → Type v) [Monad m] [MonadTail m]
-    {α β : Type u} [Nonempty β]
-    {γ : Sort w} [PartialOrder γ]
-    (f : m α) (g : γ → α → m β)
-    (hmono : monotone g) :
-    monotone (fun (x : γ) => f >>= g x) :=
-  fun _ _ h => MonadTail.bind_mono_right (hmono _ _ h)
-
-instance : MonadTail Id where
-  instCCPO _ := inferInstanceAs (CCPO (FlatOrder (b := Classical.ofNonempty)))
-  bind_mono_right h := h _
-
-instance {σ : Type u} {m : Type u → Type v} [Monad m] [MonadTail m] [Nonempty σ] :
-    MonadTail (StateT σ m) where
-  instCCPO α := inferInstanceAs (CCPO (σ → m (α × σ)))
-  bind_mono_right h := by
-    intro s
-    show StateT.bind _ _ s ⊑ StateT.bind _ _ s
-    simp only [StateT.bind]
-    apply MonadTail.bind_mono_right (m := m)
-    intro ⟨x, s'⟩
-    exact h x s'
-
-instance {ε : Type u} {m : Type u → Type v} [Monad m] [MonadTail m] :
-    MonadTail (ExceptT ε m) where
-  instCCPO β := MonadTail.instCCPO (Except ε β)
-  bind_mono_right h := by
-    apply MonadTail.bind_mono_right (m := m)
-    intro x
-    cases x with
-    | error => exact PartialOrder.rel_refl
-    | ok a => exact h a
-
-instance : MonadTail (Except ε) where
-  instCCPO β := inferInstanceAs (CCPO (FlatOrder (b := Classical.ofNonempty)))
-  bind_mono_right h := by
-    cases ‹Except _ _› with
-    | error => exact FlatOrder.rel.refl
-    | ok a => exact h a
-
-instance {m : Type u → Type v} [Monad m] [MonadTail m] :
-    MonadTail (OptionT m) where
-  instCCPO β := MonadTail.instCCPO (Option β)
-  bind_mono_right h := by
-    apply MonadTail.bind_mono_right (m := m)
-    intro x
-    cases x with
-    | none => exact PartialOrder.rel_refl
-    | some a => exact h a
-
-instance : MonadTail Option where
-  instCCPO _ := inferInstance
-  bind_mono_right h := MonoBind.bind_mono_right h
-
-instance {ρ : Type u} {m : Type u → Type v} [Monad m] [MonadTail m] :
-    MonadTail (ReaderT ρ m) where
-  instCCPO α := inferInstanceAs (CCPO (ρ → m α))
-  bind_mono_right h := by
-    intro r
-    show ReaderT.bind _ _ r ⊑ ReaderT.bind _ _ r
-    simp only [ReaderT.bind]
-    apply MonadTail.bind_mono_right (m := m)
-    intro x
-    exact h x r
-
-set_option linter.missingDocs false in
-noncomputable def ST.bot' [Nonempty α] (s : Void σ) : @FlatOrder (ST.Out σ α) (.mk Classical.ofNonempty (Classical.choice ⟨s⟩)) :=
-  .mk Classical.ofNonempty (Classical.choice ⟨s⟩)
-
-instance [Nonempty α] : CCPO (ST σ α) where
-  rel := PartialOrder.rel (α := ∀ s, FlatOrder (ST.bot' s))
-  rel_refl := PartialOrder.rel_refl
-  rel_antisymm := PartialOrder.rel_antisymm
-  rel_trans := PartialOrder.rel_trans
-  has_csup hchain := CCPO.has_csup (α := ∀ s, FlatOrder (ST.bot' s)) hchain
-
-instance : MonadTail (ST σ) where
-  instCCPO _ := inferInstance
-  bind_mono_right {_ _ a f₁ f₂} _ h := by
-    intro w
-    change FlatOrder.rel (ST.bind a f₁ w) (ST.bind a f₂ w)
-    simp only [ST.bind]
-    apply h
-
-instance : MonadTail BaseIO :=
-  inferInstanceAs (MonadTail (ST IO.RealWorld))
-
-instance [Nonempty ε] : MonadTail (EST ε σ) where
-  instCCPO _ := inferInstance
-  bind_mono_right h := MonoBind.bind_mono_right h
-
-instance [Nonempty ε] : MonadTail (EIO ε) :=
-  inferInstanceAs (MonadTail (EST ε IO.RealWorld))
-
-instance : MonadTail IO :=
-  inferInstanceAs (MonadTail (EIO IO.Error))
-
-instance {ω : Type} {σ : Type} {m : Type → Type} [Monad m] [MonadTail m] :
-    MonadTail (StateRefT' ω σ m) :=
-  inferInstanceAs (MonadTail (ReaderT (ST.Ref ω σ) m))
-
-end Lean.Order

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/Init/Repeat.lean

@@ -1,51 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Graf
--/
-module
-
-prelude
-public import Init.Core
-public import Init.Internal.Order.MonadTail
-import Init.While
-
-set_option linter.missingDocs true
-
-@[expose] public section
-
-namespace Lean
-
-open Lean.Order
-
-/-!
-# `Repeat` type for verified `repeat`/`while` loops
-
-This module provides a `Repeat` type that serves as an alternative to `Loop` for `repeat`/`while`
-loops. Unlike `Loop`, which uses `partial` recursion, `Repeat` is implemented using
-`partial_fixpoint` and `MonadTail`, enabling verified reasoning about loop programs.
--/
-
-/-- A type for `repeat`/`while` loops that supports verified reasoning via `partial_fixpoint`. -/
-structure Repeat where
-
-set_option linter.missingDocs false in
-open Lean.Order.MonadTail in
-def Repeat.forIn {β : Type u} {m : Type u → Type v}
-    [Nonempty β] [Monad m] [Lean.Order.MonadTail m]
-    (b : β) (f : Unit → β → m (ForInStep β)) : m β := do
-  match ← f () b with
-  | ForInStep.done b => pure b
-  | ForInStep.yield b => Repeat.forIn b f
-partial_fixpoint
-
-instance [Monad m] [Lean.Order.MonadTail m] : ForIn m Repeat Unit where
-  forIn _ init f := haveI : Nonempty _ := ⟨init⟩; Repeat.forIn init f
-
-macro_rules
-  | `(doElem| repeat $seq) => do
-    if ← Macro.hasDecl `Lean.Elab.Do.elabDoRepeat then
-      Lean.Macro.throwUnsupported
-    `(doElem| for _ in Repeat.mk do $seq)
-
-end Lean

src/Init/While.lean

@@ -32,11 +32,8 @@ partial def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] (_ : Loop
 instance [Monad m] : ForIn m Loop Unit where
   forIn := Loop.forIn
 
-syntax (name := doRepeat) "repeat " doSeq : doElem
+syntax "repeat " doSeq : doElem
 
-/-- Bootstrapping fallback macro for `repeat`.
-Expands to `for _ in Loop.mk do ...`. Overridden by the macro in `Init.Repeat` after
-bootstrapping. -/
 macro_rules
   | `(doElem| repeat $seq) => `(doElem| for _ in Loop.mk do $seq)
 

src/Lean/Compiler/LCNF/Basic.lean

@@ -1230,7 +1230,14 @@ def instantiateRevRangeArgs (e : Expr) (beginIdx endIdx : Nat) (args : Array (Ar
   else
     e.instantiateRevRange beginIdx endIdx (args.map (·.toExpr))
 
-/-- Lookup function for compiler extensions with sorted persisted state that works in both `lean` and `leanir`. -/
+/--
+Lookup function for compiler extensions with sorted persisted state that works in both `lean` and
+`leanir`.
+
+`preferImported` defaults to false because in `leanir`, we do not want to mix information from
+`meta` compilation in `lean` with our own state. But in `lean`, setting `preferImported` can help
+with avoiding unnecessary task blocks.
+-/
 @[inline] def findExtEntry? [Inhabited σ] (env : Environment) (ext : PersistentEnvExtension α β σ) (declName : Name)
     (findAtSorted? : Array α → Name → Option α')
     (findInState? : σ → Name → Option α') : Option α' :=

src/Lean/Compiler/LCNF/Check.lean

@@ -232,6 +232,7 @@ partial def checkCases (c : Cases .pure) : CheckM Unit := do
       withParams params do check k
 
 partial def check (code : Code .pure) : CheckM Unit := do
+  checkSystem "LCNF check"
   match code with
   | .let decl k => checkLetDecl decl; withFVarId decl.fvarId do check k
   | .fun decl k =>

src/Lean/Compiler/LCNF/Main.lean

@@ -78,9 +78,13 @@ def isValidMainType (type : Expr) : Bool :=
     isValidResultName resultName
   | _ => false
 
+/-- A postponed call of `compileDecls`. -/
 structure PostponedCompileDecls where
+  /-- Declaration names of this mutual group. -/
   declNames : Array Name
-deriving BEq, Hashable
+  /-- Options at time of original call, to be restored for tracing etc. -/
+  options : Options
+deriving BEq
 
 /--
 Saves postponed `compileDecls` calls.
@@ -101,16 +105,20 @@ builtin_initialize postponedCompileDeclsExt : SimplePersistentEnvExtension Postp
       { exported := #[], server := #[], «private» := es.toArray }
   }
 
-def resumeCompilation (declName : Name) : CoreM Unit := do
+def resumeCompilation (declName : Name) (baseOpts : Options) : CoreM Unit := do
   let some decls := postponedCompileDeclsExt.getState (← getEnv) |>.find? declName | return
+  let opts := baseOpts.mergeBy (fun _ base _ => base) decls.options
+  let opts := compiler.postponeCompile.set opts false
   modifyEnv (postponedCompileDeclsExt.modifyState · fun s => decls.declNames.foldl (·.erase) s)
-  withOptions (compiler.postponeCompile.set · false) do
+  -- NOTE: we *must* throw away the current options as they could depend on the specific recursion
+  -- we did to get here.
+  withOptions (fun _ => opts) do
   Core.prependError m!"Failed to compile `{declName}`" do
-    (← compileDeclsRef.get) decls.declNames
+    (← compileDeclsRef.get) decls.declNames baseOpts
 
 namespace PassManager
 
-partial def run (declNames : Array Name) : CompilerM Unit := withAtLeastMaxRecDepth 8192 do
+partial def run (declNames : Array Name) (baseOpts : Options) : CompilerM Unit := withAtLeastMaxRecDepth 8192 do
   /-
   Note: we need to increase the recursion depth because we currently do to save phase1
   declarations in .olean files. Then, we have to recursively compile all dependencies,
@@ -141,11 +149,14 @@ partial def run (declNames : Array Name) : CompilerM Unit := withAtLeastMaxRecDe
 
   -- Now that we have done all input checks, check for postponement
   if (← getEnv).header.isModule && (← compiler.postponeCompile.getM) then
-    modifyEnv (postponedCompileDeclsExt.addEntry · { declNames := decls.map (·.name) })
+    modifyEnv (postponedCompileDeclsExt.addEntry · { declNames := decls.map (·.name), options := ← getOptions })
     -- meta defs are compiled locally so they are available for execution/compilation without
     -- importing `.ir` but still marked for `leanir` compilation so that we do not have to persist
     -- module-local compilation information between the two processes
-    if !decls.any (isMarkedMeta (← getEnv) ·.name) then
+    if decls.any (isMarkedMeta (← getEnv) ·.name) then
+      -- avoid re-compiling the meta defs in this process; the entry for `leanir` is not affected
+      modifyEnv (postponedCompileDeclsExt.modifyState · fun s => decls.foldl (·.erase ·.name) s)
+    else
       trace[Compiler] "postponing compilation of {decls.map (·.name)}"
       return
 
@@ -157,7 +168,7 @@ partial def run (declNames : Array Name) : CompilerM Unit := withAtLeastMaxRecDe
       let .let { value := .const c .., .. } .. := c | return
       -- Need to do some lookups to get the actual name passed to `compileDecls`
       let c := Compiler.getImplementedBy? (← getEnv) c |>.getD c
-      resumeCompilation c
+      resumeCompilation c baseOpts
 
   let decls := markRecDecls decls
   let manager ← getPassManager
@@ -188,6 +199,7 @@ where
     profileitM Exception profilerName (← getOptions) do
       let mut state : (pu : Purity) × Array (Decl pu) := ⟨inPhase, decls⟩
       for pass in passes do
+        checkSystem "LCNF compiler"
         state ← withTraceNode `Compiler (fun _ => return m!"compiler phase: {pass.phase}, pass: {pass.name}") do
           let decls ← withPhase pass.phase do
             state.fst.withAssertPurity pass.phase.toPurity fun h => do
@@ -199,9 +211,9 @@ where
 
 end PassManager
 
-def main (declNames : Array Name) : CoreM Unit := do
+def main (declNames : Array Name) (baseOpts : Options) : CoreM Unit := do
   withTraceNode `Compiler (fun _ => return m!"compiling: {declNames}") do
-    CompilerM.run <| PassManager.run declNames
+    CompilerM.run <| PassManager.run declNames baseOpts
 
 builtin_initialize
   compileDeclsRef.set main

src/Lean/Compiler/LCNF/Simp/SimpM.lean

@@ -146,7 +146,7 @@ Similar to the default `Lean.withIncRecDepth`, but include the `inlineStack` in
 @[inline] def withIncRecDepth (x : SimpM α) : SimpM α := do
   let curr ← MonadRecDepth.getRecDepth
   let max  ← MonadRecDepth.getMaxRecDepth
-  if curr == max then
+  if max != 0 && curr == max then
     throwMaxRecDepth
   else
     MonadRecDepth.withRecDepth (curr+1) x

src/Lean/Compiler/LCNF/ToMono.lean

@@ -279,13 +279,13 @@ partial def casesFloatArrayToMono (c : Cases .pure) (_ : c.typeName == ``FloatAr
   let k ← k.toMono
   return .let decl k
 
-/-- Eliminate `cases` for `String. -/
+/-- Eliminate `cases` for `String`. -/
 partial def casesStringToMono (c : Cases .pure) (_ : c.typeName == ``String) : ToMonoM (Code .pure) := do
   assert! c.alts.size == 1
   let .alt _ ps k := c.alts[0]! | unreachable!
   eraseParams ps
   let p := ps[0]!
-  let decl := { fvarId := p.fvarId, binderName := p.binderName, type := anyExpr, value := .const ``String.toList [] #[.fvar c.discr] }
+  let decl := { fvarId := p.fvarId, binderName := p.binderName, type := anyExpr, value := .const ``String.toByteArray [] #[.fvar c.discr] }
   modifyLCtx fun lctx => lctx.addLetDecl decl
   let k ← k.toMono
   return .let decl k

src/Lean/Compiler/Main.lean

@@ -19,7 +19,7 @@ that fulfill the requirements of `shouldGenerateCode`.
 def compile (declNames : Array Name) : CoreM Unit := do profileitM Exception "compiler new" (← getOptions) do
   withOptions (compiler.postponeCompile.set · false) do
   withTraceNode `Compiler (fun _ => return m!"compiling: {declNames}") do
-    LCNF.main declNames
+    LCNF.main declNames {}
 
 builtin_initialize
   registerTraceClass `Compiler

src/Lean/CoreM.lean

@@ -453,6 +453,9 @@ Throws an internal interrupt exception if cancellation has been requested. The e
 caught by `try catch` but is intended to be caught by `Command.withLoggingExceptions` at the top
 level of elaboration. In particular, we want to skip producing further incremental snapshots after
 the exception has been thrown.
+
+Like `checkSystem` but without the global heartbeat check, for callers that have their own
+heartbeat tracking (e.g. `SynthInstance`).
  -/
 @[inline] def checkInterrupted : CoreM Unit := do
   if let some tk := (← read).cancelTk? then
@@ -708,11 +711,11 @@ breaks the cycle by making `compileDeclsImpl` a "dynamic" call through the ref t
 to the linker. In the compiler there is a matching `builtin_initialize` to set this ref to the
 actual implementation of compileDeclsRef.
 -/
-builtin_initialize compileDeclsRef : IO.Ref (Array Name → CoreM Unit) ←
-  IO.mkRef (fun _ => throwError m!"call to compileDecls with uninitialized compileDeclsRef")
+builtin_initialize compileDeclsRef : IO.Ref (Array Name → Options → CoreM Unit) ←
+  IO.mkRef (fun _ _ => throwError m!"call to compileDecls with uninitialized compileDeclsRef")
 
 private def compileDeclsImpl (declNames : Array Name) : CoreM Unit := do
-  (← compileDeclsRef.get) declNames
+  (← compileDeclsRef.get) declNames {}
 
 -- `ref?` is used for error reporting if available
 def compileDecls (decls : Array Name) (logErrors := true) : CoreM Unit := do

src/Lean/Data/Options.lean

@@ -82,11 +82,17 @@ def mergeBy (f : Name → DataValue → DataValue → DataValue) (o1 o2 : Option
 
 end Options
 
+structure OptionDeprecation where
+  since    : String
+  text?    : Option String := none
+  deriving Inhabited
+
 structure OptionDecl where
   name     : Name
   declName : Name := by exact decl_name%
   defValue : DataValue
   descr    : String := ""
+  deprecation? : Option OptionDeprecation := none
   deriving Inhabited
 
 def OptionDecl.fullDescr (self : OptionDecl) : String := Id.run do
@@ -183,6 +189,7 @@ namespace Option
 protected structure Decl (α : Type) where
   defValue : α
   descr    : String := ""
+  deprecation? : Option OptionDeprecation := none
 
 protected def get? [KVMap.Value α] (opts : Options) (opt : Lean.Option α) : Option α :=
   opts.get? opt.name
@@ -214,6 +221,7 @@ protected def register [KVMap.Value α] (name : Name) (decl : Lean.Option.Decl
     declName := ref
     defValue := KVMap.Value.toDataValue decl.defValue
     descr := decl.descr
+    deprecation? := decl.deprecation?
   }
   return { name := name, defValue := decl.defValue }
 

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/DeprecatedModule.lean

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+-/
+module
+
+prelude
+public import Lean.Compiler.ModPkgExt
+
+public section
+
+namespace Lean
+
+structure DeprecatedModuleEntry where
+  message? : Option String := none
+  since? : Option String := none
+  deriving Inhabited
+
+register_builtin_option linter.deprecated.module : Bool := {
+  defValue := true
+  descr := "if true, generate warnings when importing deprecated modules"
+}
+
+builtin_initialize deprecatedModuleExt : ModuleEnvExtension <| Option DeprecatedModuleEntry ←
+  registerModuleEnvExtension <| pure none
+
+def Environment.getDeprecatedModuleByIdx? (env : Environment) (idx : ModuleIdx) : Option DeprecatedModuleEntry :=
+  deprecatedModuleExt.getStateByIdx? env idx |>.join
+
+def Environment.setDeprecatedModule (entry : Option DeprecatedModuleEntry) (env : Environment) : Environment :=
+  deprecatedModuleExt.setState env entry
+
+def formatDeprecatedModuleWarning (env : Environment) (idx : ModuleIdx) (modName : Name)
+    (entry : DeprecatedModuleEntry) : String :=
+  let msg := entry.message?.getD ""
+  let replacements := env.header.moduleData[idx.toNat]!.imports.filter fun imp =>
+    imp.module != `Init
+  let lines := replacements.foldl (init := "") fun acc imp =>
+    acc ++ s!"import {imp.module}\n"
+  s!"{msg}\n\
+    '{modName}' has been deprecated: please replace this import by\n\n\
+    {lines}"
+
+end Lean

src/Lean/Elab/App.lean

@@ -1832,13 +1832,15 @@ To infer a namespace from the expected type, we do the following operations:
 - if the type is of the form `c x₁ ... xₙ` with `c` a constant, then try using `c` as the namespace,
   and if that doesn't work, try unfolding the expression and continuing.
 -/
-private partial def resolveDottedIdentFn (idRef : Syntax) (id : Name) (expectedType? : Option Expr) : TermElabM (List (Expr × Syntax × List Syntax)) := do
+private partial def resolveDottedIdentFn (idRef : Syntax) (id : Name) (explicitUnivs : List Level) (expectedType? : Option Expr) : TermElabM (List (Expr × Syntax × List Syntax)) := do
   unless id.isAtomic do
     throwError "Invalid dotted identifier notation: The name `{id}` must be atomic"
   tryPostponeIfNoneOrMVar expectedType?
   let some expectedType := expectedType?
     | throwNoExpectedType
   addCompletionInfo <| CompletionInfo.dotId idRef id (← getLCtx) expectedType?
+  -- We will check deprecations in `elabAppFnResolutions`.
+  withoutCheckDeprecated do
   withForallBody expectedType fun resultType => do
     go resultType expectedType #[]
 where
@@ -1878,8 +1880,10 @@ where
           |>.filter (fun (_, fieldList) => fieldList.isEmpty)
           |>.map Prod.fst
         if !candidates.isEmpty then
-          candidates.mapM fun resolvedName => return (← mkConst resolvedName, ← getRef, [])
+          candidates.mapM fun resolvedName => return (← mkConst resolvedName explicitUnivs, ← getRef, [])
         else if let some (fvar, []) ← resolveLocalName fullName then
+          unless explicitUnivs.isEmpty do
+            throwInvalidExplicitUniversesForLocal fvar
           return [(fvar, ← getRef, [])]
         else
           throwUnknownIdentifierAt (← getRef) (declHint := fullName) <| m!"Unknown constant `{.ofConstName fullName}`"
@@ -1919,6 +1923,10 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
       let some idx := idxStx.isFieldIdx?
         | throwError "Internal error: Unexpected field index syntax `{idxStx}`"
       elabAppFn e (LVal.fieldIdx idxStx idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
+    let elabDottedIdent (id : Syntax) (explicitUnivs : List Level) (explicit : Bool) : TermElabM (Array (TermElabResult Expr)) := do
+      let res ← withRef f <| resolveDottedIdentFn id id.getId.eraseMacroScopes explicitUnivs expectedType?
+      -- Use (forceTermInfo := true) because we want to record the result of .ident resolution even in patterns
+      elabAppFnResolutions f res lvals namedArgs args expectedType? explicit ellipsis overloaded acc (forceTermInfo := true)
     match f with
     | `($(e).$idx:fieldIdx) => elabFieldIdx e idx explicit
     | `($e |>.$idx:fieldIdx) => elabFieldIdx e idx explicit
@@ -1934,16 +1942,17 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
     | `($id:ident.{$us,*}) => do
       let us ← elabExplicitUnivs us
       elabAppFnId id us lvals namedArgs args expectedType? explicit ellipsis overloaded acc
-    | `(@$id:ident) =>
-      elabAppFn id lvals namedArgs args expectedType? (explicit := true) ellipsis overloaded acc
-    | `(@$_:ident.{$_us,*}) =>
+    | `(.$id:ident) => elabDottedIdent id [] explicit
+    | `(.$id:ident.{$us,*}) =>
+      let us ← elabExplicitUnivs us
+      elabDottedIdent id us explicit
+    | `(@$_:ident)
+    | `(@$_:ident.{$_us,*})
+    | `(@.$_:ident)
+    | `(@.$_:ident.{$_us,*}) =>
       elabAppFn (f.getArg 1) lvals namedArgs args expectedType? (explicit := true) ellipsis overloaded acc
     | `(@$_)     => throwUnsupportedSyntax -- invalid occurrence of `@`
     | `(_)       => throwError "A placeholder `_` cannot be used where a function is expected"
-    | `(.$id:ident) =>
-        let res ← withRef f <| resolveDottedIdentFn id id.getId.eraseMacroScopes expectedType?
-        -- Use (forceTermInfo := true) because we want to record the result of .ident resolution even in patterns
-        elabAppFnResolutions f res lvals namedArgs args expectedType? explicit ellipsis overloaded acc (forceTermInfo := true)
     | _ => do
       let catchPostpone := !overloaded
       /- If we are processing a choice node, then we should use `catchPostpone == false` when elaborating terms.
@@ -2086,13 +2095,15 @@ private def elabAtom : TermElab := fun stx expectedType? => do
 
 @[builtin_term_elab explicit] def elabExplicit : TermElab := fun stx expectedType? =>
   match stx with
-  | `(@$_:ident)          => elabAtom stx expectedType?  -- Recall that `elabApp` also has support for `@`
-  | `(@$_:ident.{$_us,*}) => elabAtom stx expectedType?
-  | `(@$(_).$_:fieldIdx)  => elabAtom stx expectedType?
-  | `(@$(_).$_:ident)     => elabAtom stx expectedType?
-  | `(@($t))             => elabTerm t expectedType? (implicitLambda := false)    -- `@` is being used just to disable implicit lambdas
-  | `(@$t)               => elabTerm t expectedType? (implicitLambda := false)   -- `@` is being used just to disable implicit lambdas
-  | _                    => throwUnsupportedSyntax
+  | `(@$_:ident)           => elabAtom stx expectedType?  -- Recall that `elabApp` also has support for `@`
+  | `(@$_:ident.{$_us,*})  => elabAtom stx expectedType?
+  | `(@$(_).$_:fieldIdx)   => elabAtom stx expectedType?
+  | `(@$(_).$_:ident)      => elabAtom stx expectedType?
+  | `(@.$_:ident)          => elabAtom stx expectedType?
+  | `(@.$_:ident.{$_us,*}) => elabAtom stx expectedType?
+  | `(@($t))               => elabTerm t expectedType? (implicitLambda := false)   -- `@` is being used just to disable implicit lambdas
+  | `(@$t)                 => elabTerm t expectedType? (implicitLambda := false)   -- `@` is being used just to disable implicit lambdas
+  | _                      => throwUnsupportedSyntax
 
 @[builtin_term_elab choice] def elabChoice : TermElab := elabAtom
 @[builtin_term_elab proj] def elabProj : TermElab := elabAtom

src/Lean/Elab/BuiltinCommand.lean

@@ -9,10 +9,12 @@ prelude
 public import Lean.Meta.Reduce
 public import Lean.Elab.Eval
 public import Lean.Elab.Command
+import Lean.Elab.DeprecatedSyntax
 public import Lean.Elab.Open
 import Init.Data.Nat.Order
 import Init.Data.Order.Lemmas
 import Init.System.Platform
+import Lean.DeprecatedModule
 
 public section
 
@@ -508,10 +510,20 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
     pure ()
 
 @[builtin_command_elab «set_option»] def elabSetOption : CommandElab := fun stx => do
-  let options ← Elab.elabSetOption stx[1] stx[3]
+  let (options, decl) ← Elab.elabSetOption stx[1] stx[3]
+  withRef stx[1] <| Elab.checkDeprecatedOption (stx[1].getId.eraseMacroScopes) decl
   modify fun s => { s with maxRecDepth := maxRecDepth.get options }
   modifyScope fun scope => { scope with opts := options }
 
+@[builtin_command_elab «unlock_limits»] def elabUnlockLimits : CommandElab := fun _ => do
+  let opts ← getOptions
+  let opts := maxHeartbeats.set opts 0
+  let opts := maxRecDepth.set opts 0
+  let opts := synthInstance.maxHeartbeats.set opts 0
+  modifyScope ({ · with opts })
+  -- update cached value as well
+  modify ({ · with maxRecDepth := 0 })
+
 open Lean.Parser.Command.InternalSyntax in
 @[builtin_macro Lean.Parser.Command.«in»] def expandInCmd : Macro
   | `($cmd₁ in%$tk $cmd₂) =>
@@ -706,4 +718,54 @@ where
     let env ← getEnv
     IO.eprintln (← env.dbgFormatAsyncState)
 
+/-- Elaborate `deprecated_module`, marking the current module as deprecated. -/
+@[builtin_command_elab Parser.Command.deprecated_module]
+def elabDeprecatedModule : CommandElab
+  | `(Parser.Command.deprecated_module| deprecated_module $[$msg?]? $[(since := $since?)]?) => do
+    let message? := msg?.map TSyntax.getString
+    let since? := since?.map TSyntax.getString
+    if (deprecatedModuleExt.getState (← getEnv)).isSome then
+      logWarning "module is already marked as deprecated"
+    if since?.isNone then
+      logWarning "`deprecated_module` should specify the date or library version \
+        at which the deprecation was introduced, using `(since := \"...\")`"
+    modifyEnv fun env => env.setDeprecatedModule (some { message?, since? })
+  | _ => throwUnsupportedSyntax
+
+/-- Elaborate `#show_deprecated_modules`, displaying all deprecated modules. -/
+@[builtin_command_elab Parser.Command.showDeprecatedModules]
+def elabShowDeprecatedModules : CommandElab := fun _ => do
+  let env ← getEnv
+  let mut parts : Array String := #["Deprecated modules\n"]
+  for h : idx in [:env.header.moduleNames.size] do
+    if let some entry := env.getDeprecatedModuleByIdx? idx then
+      let modName := env.header.moduleNames[idx]
+      let msg := match entry.message? with
+        | some str => s!"message '{str}'"
+        | none => "no message"
+      let replacements := env.header.moduleData[idx]!.imports.filter fun imp =>
+        imp.module != `Init
+      parts := parts.push s!"'{modName}' deprecates to\n{replacements.map (·.module)}\nwith {msg}\n"
+  -- Also show the current module's deprecation if set.
+  if let some entry := deprecatedModuleExt.getState env then
+    let modName := env.mainModule
+    let msg := match entry.message? with
+      | some str => s!"message '{str}'"
+      | none => "no message"
+    let replacements := env.imports.filter fun imp =>
+      imp.module != `Init
+    parts := parts.push s!"'{modName}' deprecates to\n{replacements.map (·.module)}\nwith {msg}\n"
+  logInfo (String.intercalate "\n" parts.toList)
+
+@[builtin_command_elab Parser.Command.deprecatedSyntax] def elabDeprecatedSyntax : CommandElab := fun stx => do
+  let id := stx[1]
+  let kind ← liftCoreM <| checkSyntaxNodeKindAtNamespaces id.getId (← getCurrNamespace)
+  let text? := if stx[2].isNone then none else stx[2][0].isStrLit?
+  let since? := if stx[3].isNone then none else stx[3][3].isStrLit?
+  if since?.isNone then
+    logWarning "`deprecated_syntax` should specify the date or library version at which the \
+      deprecation was introduced, using `(since := \"...\")`"
+  modifyEnv fun env =>
+    deprecatedSyntaxExt.addEntry env { kind, text?, since? }
+
 end Lean.Elab.Command

src/Lean/Elab/BuiltinDo.lean

@@ -15,4 +15,3 @@ public import Lean.Elab.BuiltinDo.Jump
 public import Lean.Elab.BuiltinDo.Misc
 public import Lean.Elab.BuiltinDo.For
 public import Lean.Elab.BuiltinDo.TryCatch
-public import Lean.Elab.BuiltinDo.Repeat

src/Lean/Elab/BuiltinDo/Let.lean

@@ -81,8 +81,15 @@ private def pushTypeIntoReassignment (letOrReassign : LetOrReassign) (decl : TSy
   else
     pure decl
 
-partial def elabDoLetOrReassign (letOrReassign : LetOrReassign) (decl : TSyntax ``letDecl)
+private def checkLetConfigInDo (config : Term.LetConfig) : DoElabM Unit := do
+  if config.postponeValue then
+    throwError "`+postponeValue` is not supported in `do` blocks"
+  if config.generalize then
+    throwError "`+generalize` is not supported in `do` blocks"
+
+partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOrReassign) (decl : TSyntax ``letDecl)
     (dec : DoElemCont) : DoElabM Expr := do
+  checkLetConfigInDo config
   let vars ← getLetDeclVars decl
   letOrReassign.checkMutVars vars
   -- Some decl preprocessing on the patterns and expected types:
@@ -91,7 +98,7 @@ partial def elabDoLetOrReassign (letOrReassign : LetOrReassign) (decl : TSyntax
   match decl with
   | `(letDecl| $decl:letEqnsDecl) =>
     let declNew ← `(letDecl| $(⟨← liftMacroM <| Term.expandLetEqnsDecl decl⟩):letIdDecl)
-    return ← Term.withMacroExpansion decl declNew <| elabDoLetOrReassign letOrReassign declNew dec
+    return ← Term.withMacroExpansion decl declNew <| elabDoLetOrReassign config letOrReassign declNew dec
   | `(letDecl| $pattern:term $[: $xType?]? := $rhs) =>
     let rhs ← match xType? with | some xType => `(($rhs : $xType)) | none => pure rhs
     let contElab : DoElabM Expr := elabWithReassignments letOrReassign vars dec.continueWithUnit
@@ -99,15 +106,21 @@ partial def elabDoLetOrReassign (letOrReassign : LetOrReassign) (decl : TSyntax
     -- The infamous MVar postponement trick below popularized by `if` is necessary in Lake.CLI.Main.
     -- We need it because we specify a constant motive, otherwise the `match` elaborator would have postponed.
     let mvar ← Lean.withRef rhs `(?m)
-    let term ← `(let_mvar% ?m := $rhs;
-                 wait_if_type_mvar% ?m;
-                 match (motive := ∀_, $(← Term.exprToSyntax mγ)) $mvar:term with
-                 | $pattern:term => $body)
+    let term ← if let some h := config.eq? then
+      `(let_mvar% ?m := $rhs;
+        wait_if_type_mvar% ?m;
+        match $h:ident : $mvar:term with
+        | $pattern:term => $body)
+    else
+      `(let_mvar% ?m := $rhs;
+        wait_if_type_mvar% ?m;
+        match (motive := ∀_, $(← Term.exprToSyntax mγ)) $mvar:term with
+        | $pattern:term => $body)
     Term.withMacroExpansion (← getRef) term do Term.elabTermEnsuringType term (some mγ)
   | `(letDecl| $decl:letIdDecl) =>
     let { id, binders, type, value } := Term.mkLetIdDeclView decl
     let id ← if id.isIdent then pure id else Term.mkFreshIdent id (canonical := true)
-    let nondep := letOrReassign matches .have
+    let nondep := config.nondep || letOrReassign matches .have
     -- Only non-`mut` lets will be elaborated as `let`s; `let mut` and reassigns behave as `have`s.
     -- See `elabLetDeclAux` for rationale.
     let (type, val) ← Term.elabBindersEx binders fun xs => do
@@ -128,8 +141,25 @@ partial def elabDoLetOrReassign (letOrReassign : LetOrReassign) (decl : TSyntax
     withLetDecl id.getId (kind := kind) type val (nondep := nondep) fun x => do
       Term.addLocalVarInfo id x
       elabWithReassignments letOrReassign vars do
-      let body ← dec.continueWithUnit
-      mkLetFVars #[x] body (usedLetOnly := false) (generalizeNondepLet := false)
+      match config.eq? with
+      | none =>
+        let body ← dec.continueWithUnit
+        if config.zeta then
+          pure <| (← body.abstractM #[x]).instantiate1 val
+        else
+          mkLetFVars #[x] body (usedLetOnly := config.usedOnly) (generalizeNondepLet := false)
+      | some h =>
+        let hTy ← mkEq x val
+        withLetDecl h.getId hTy (← mkEqRefl x) (nondep := true) fun h' => do
+          Term.addLocalVarInfo h h'
+          let body ← dec.continueWithUnit
+          if config.zeta then
+            pure <| (← body.abstractM #[x, h']).instantiateRev #[val, ← mkEqRefl val]
+          else if nondep then
+            let f ← mkLambdaFVars #[x, h'] body
+            return mkApp2 f val (← mkEqRefl val)
+          else
+            mkLetFVars #[x, h'] body (usedLetOnly := config.usedOnly) (generalizeNondepLet := false)
   | _ => throwUnsupportedSyntax
 
 def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``doPatDecl]) (dec : DoElemCont) : DoElabM Expr := do
@@ -168,13 +198,21 @@ def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``do
         elabDoElem (← `(doElem| $pattern:term := $x)) dec
   | _ => throwUnsupportedSyntax
 
+private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letConfig)
+    (mutTk? : Option Syntax) (initConfig : Term.LetConfig := {}) : DoElabM Term.LetConfig := do
+  if mutTk?.isSome && !letConfigStx.raw[0].getArgs.isEmpty then
+    throwErrorAt letConfigStx "configuration options are not allowed with `let mut`"
+  Term.mkLetConfig letConfigStx initConfig
+
 @[builtin_doElem_elab Lean.Parser.Term.doLet] def elabDoLet : DoElab := fun stx dec => do
-  let `(doLet| let $[mut%$mutTk?]? $decl:letDecl) := stx | throwUnsupportedSyntax
-  elabDoLetOrReassign (.let mutTk?) decl dec
+  let `(doLet| let $[mut%$mutTk?]? $config:letConfig $decl:letDecl) := stx | throwUnsupportedSyntax
+  let config ← getLetConfigAndCheckMut config mutTk?
+  elabDoLetOrReassign config (.let mutTk?) decl dec
 
 @[builtin_doElem_elab Lean.Parser.Term.doHave] def elabDoHave : DoElab := fun stx dec => do
-  let `(doHave| have $decl:letDecl) := stx | throwUnsupportedSyntax
-  elabDoLetOrReassign .have decl dec
+  let `(doHave| have $config:letConfig $decl:letDecl) := stx | throwUnsupportedSyntax
+  let config ← Term.mkLetConfig config { nondep := true }
+  elabDoLetOrReassign config .have decl dec
 
 @[builtin_doElem_elab Lean.Parser.Term.doLetRec] def elabDoLetRec : DoElab := fun stx dec => do
   let `(doLetRec| let rec $decls:letRecDecls) := stx | throwUnsupportedSyntax
@@ -192,14 +230,17 @@ def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``do
   | `(doReassign| $x:ident $[: $xType?]? := $rhs) =>
     let decl : TSyntax ``letIdDecl ← `(letIdDecl| $x:ident $[: $xType?]? := $rhs)
     let decl : TSyntax ``letDecl := ⟨mkNode ``letDecl #[decl]⟩
-    elabDoLetOrReassign .reassign decl dec
+    elabDoLetOrReassign {} .reassign decl dec
   | `(doReassign| $decl:letPatDecl) =>
     let decl : TSyntax ``letDecl := ⟨mkNode ``letDecl #[decl]⟩
-    elabDoLetOrReassign .reassign decl dec
+    elabDoLetOrReassign {} .reassign decl dec
   | _ => throwUnsupportedSyntax
 
 @[builtin_doElem_elab Lean.Parser.Term.doLetElse] def elabDoLetElse : DoElab := fun stx dec => do
-  let `(doLetElse| let $[mut%$mutTk?]? $pattern := $rhs | $otherwise $(body?)?) := stx | throwUnsupportedSyntax
+  let `(doLetElse| let $[mut%$mutTk?]? $cfg:letConfig $pattern := $rhs | $otherwise $(body?)?) := stx
+    | throwUnsupportedSyntax
+  let config ← getLetConfigAndCheckMut cfg mutTk?
+  checkLetConfigInDo config
   let letOrReassign := LetOrReassign.let mutTk?
   let vars ← getPatternVarsEx pattern
   letOrReassign.checkMutVars vars
@@ -208,10 +249,17 @@ def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``do
   if mutTk?.isSome then
     for var in vars do
       body ← `(doSeqIndent| let mut $var := $var; do $body:doSeqIndent)
-  elabDoElem (← `(doElem| match $rhs:term with | $pattern => $body:doSeqIndent | _ => $otherwise:doSeqIndent)) dec
+  if let some h := config.eq? then
+    elabDoElem (← `(doElem| match $h:ident : $rhs:term with | $pattern => $body:doSeqIndent | _ => $otherwise:doSeqIndent)) dec
+  else
+    elabDoElem (← `(doElem| match $rhs:term with | $pattern => $body:doSeqIndent | _ => $otherwise:doSeqIndent)) dec
 
 @[builtin_doElem_elab Lean.Parser.Term.doLetArrow] def elabDoLetArrow : DoElab := fun stx dec => do
-  let `(doLetArrow| let $[mut%$mutTk?]? $decl) := stx | throwUnsupportedSyntax
+  let `(doLetArrow| let $[mut%$mutTk?]? $cfg:letConfig $decl) := stx | throwUnsupportedSyntax
+  let config ← getLetConfigAndCheckMut cfg mutTk?
+  checkLetConfigInDo config
+  if config.nondep || config.usedOnly || config.zeta || config.eq?.isSome then
+    throwErrorAt cfg "configuration options are not supported with `←`"
   elabDoArrow (.let mutTk?) decl dec
 
 @[builtin_doElem_elab Lean.Parser.Term.doReassignArrow] def elabDoReassignArrow : DoElab := fun stx dec => do

src/Lean/Elab/BuiltinDo/Repeat.lean

@@ -1,30 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Graf
--/
-module
-
-prelude
-public import Lean.Elab.BuiltinDo.Basic
-meta import Lean.Parser.Do
-import Lean.Elab.BuiltinDo.For
-import Lean.Elab.Do.Switch
-
-public section
-
-namespace Lean.Elab.Do
-
-open Lean.Parser.Term
-
-@[builtin_doElem_elab Lean.doRepeat] def elabDoRepeat : DoElab := fun stx dec => do
-  let `(doElem| repeat $seq) := stx | throwUnsupportedSyntax
-  let expanded ←
-    if Term.backward.do.while.get (← getOptions) then
-      `(doElem| for _ in Loop.mk do $seq)
-    else
-      `(doElem| for _ in Repeat.mk do $seq)
-  Term.withMacroExpansion stx expanded <|
-    withRef expanded <| elabDoElem ⟨expanded⟩ dec
-
-end Lean.Elab.Do

src/Lean/Elab/BuiltinTerm.lean

@@ -371,7 +371,8 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
     popScope
 
 @[builtin_term_elab «set_option»] def elabSetOption : TermElab := fun stx expectedType? => do
-  let options ← Elab.elabSetOption stx[1] stx[3]
+  let (options, decl) ← Elab.elabSetOption stx[1] stx[3]
+  withRef stx[1] <| Elab.checkDeprecatedOption (stx[1].getId.eraseMacroScopes) decl
   withOptions (fun _ => options) do
     try
       elabTerm stx[5] expectedType?

src/Lean/Elab/Command.lean

@@ -10,6 +10,7 @@ public import Lean.Meta.Diagnostics
 public import Lean.Elab.Binders
 public import Lean.Elab.Command.Scope
 public import Lean.Elab.SetOption
+import Lean.Elab.DeprecatedSyntax
 public meta import Lean.Parser.Command
 
 public section
@@ -468,6 +469,7 @@ where go := do
       else withTraceNode `Elab.command (fun _ => return stx) (tag :=
         -- special case: show actual declaration kind for `declaration` commands
         (if stx.isOfKind ``Parser.Command.declaration then stx[1] else stx).getKind.toString) do
+        checkDeprecatedSyntax stx (← read).macroStack
         let s ← get
         match (← liftMacroM <| expandMacroImpl? s.env stx) with
         | some (decl, stxNew?) =>
@@ -873,7 +875,7 @@ first evaluates any local `set_option ... in ...` clauses and then invokes `cmd`
 partial def withSetOptionIn (cmd : CommandElab) : CommandElab := fun stx => do
   if stx.getKind == ``Lean.Parser.Command.in &&
      stx[0].getKind == ``Lean.Parser.Command.set_option then
-      let opts ← Elab.elabSetOption stx[0][1] stx[0][3]
+      let (opts, _) ← Elab.elabSetOption stx[0][1] stx[0][3]
       Command.withScope (fun scope => { scope with opts }) do
         withSetOptionIn cmd stx[2]
   else

src/Lean/Elab/DeprecatedSyntax.lean

@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+-/
+module
+
+prelude
+public import Lean.MonadEnv
+public import Lean.Linter.Basic
+public import Lean.Elab.Util
+
+public section
+
+namespace Lean.Linter
+
+register_builtin_option linter.deprecated.syntax : Bool := {
+  defValue := true
+  descr := "if true, generate warnings when deprecated syntax is used"
+}
+
+end Lean.Linter
+
+namespace Lean.Elab
+
+/-- Entry recording that a syntax kind has been deprecated. -/
+structure SyntaxDeprecationEntry where
+  /-- The syntax node kind that is deprecated. -/
+  kind : SyntaxNodeKind
+  /-- Optional deprecation message. -/
+  text? : Option String := none
+  /-- Optional version or date at which the syntax was deprecated. -/
+  since? : Option String := none
+
+builtin_initialize deprecatedSyntaxExt :
+    SimplePersistentEnvExtension SyntaxDeprecationEntry (NameMap SyntaxDeprecationEntry) ←
+  registerSimplePersistentEnvExtension {
+    addImportedFn := mkStateFromImportedEntries (fun m e => m.insert e.kind e) {}
+    addEntryFn := fun m e => m.insert e.kind e
+  }
+
+/--
+Check whether `stx` is a deprecated syntax kind, and if so, emit a warning.
+
+If `macroStack` is non-empty, the warning is attributed to the macro call site rather than the
+syntax itself.
+-/
+def checkDeprecatedSyntax [Monad m] [MonadEnv m] [MonadLog m] [MonadOptions m]
+    [AddMessageContext m] [MonadRef m] (stx : Syntax) (macroStack : MacroStack) : m Unit := do
+  let env ← getEnv
+  let kind := stx.getKind
+  if let some entry := (deprecatedSyntaxExt.getState env).find? kind then
+    let extraMsg := match entry.text? with
+      | some text => m!": {text}"
+      | none => m!""
+    match macroStack with
+    | { before := macroStx, .. } :: { before := callerStx, .. } :: _ =>
+      let expandedFrom :=
+        if callerStx.getKind != macroStx.getKind then
+          m!" (expanded from '{callerStx.getKind}')"
+        else m!""
+      Linter.logLintIf Linter.linter.deprecated.syntax macroStx
+        m!"macro '{macroStx.getKind}'{expandedFrom} produces deprecated syntax '{kind}'{extraMsg}"
+    | { before := macroStx, .. } :: [] =>
+      Linter.logLintIf Linter.linter.deprecated.syntax macroStx
+        m!"macro '{macroStx.getKind}' produces deprecated syntax '{kind}'{extraMsg}"
+    | [] =>
+      Linter.logLintIf Linter.linter.deprecated.syntax stx
+        m!"syntax '{kind}' has been deprecated{extraMsg}"
+
+end Lean.Elab

src/Lean/Elab/Do/InferControlInfo.lean

@@ -94,12 +94,12 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
   | `(doExpr| $_:term) => return { numRegularExits := 1 }
   | `(doElem| do $doSeq) => ofSeq doSeq
   -- Let
-  | `(doElem| let $[mut]? $_:letDecl) => return .pure
-  | `(doElem| have $_:letDecl) => return .pure
+  | `(doElem| let $[mut]? $_:letConfig $_:letDecl) => return .pure
+  | `(doElem| have $_:letConfig $_:letDecl) => return .pure
   | `(doElem| let rec $_:letRecDecl) => return .pure
-  | `(doElem| let $[mut]? $_ := $_ | $otherwise $(body?)?) =>
+  | `(doElem| let $[mut]? $_:letConfig $_ := $_ | $otherwise $(body?)?) =>
     ofLetOrReassign #[] none otherwise body?
-  | `(doElem| let $[mut]? $decl) =>
+  | `(doElem| let $[mut]? $_:letConfig $decl) =>
     ofLetOrReassignArrow false decl
   | `(doElem| $decl:letIdDeclNoBinders) =>
     ofLetOrReassign (← getLetIdDeclVars ⟨decl⟩) none none none
@@ -169,15 +169,16 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
     let bodyInfo ← match body? with | none => pure {} | some body => ofSeq ⟨body⟩
     return otherwiseInfo.alternative bodyInfo
   | _ =>
-    let handlers := controlInfoElemAttribute.getEntries (← getEnv) stx.raw.getKind
+    let kind := stx.raw.getKind
+    let handlers := controlInfoElemAttribute.getEntries (← getEnv) kind
     for handler in handlers do
       let res ← catchInternalId unsupportedSyntaxExceptionId
         (some <$> handler.value stx)
         (fun _ => pure none)
       if let some info := res then return info
     throwError
-      "No `ControlInfo` inference handler found for `{stx.raw.getKind}` in syntax {indentD stx}\n\
-       Register a handler with `@[doElem_control_info {stx.raw.getKind}]`."
+      "No `ControlInfo` inference handler found for `{kind}` in syntax {indentD stx}\n\
+       Register a handler with `@[doElem_control_info {kind}]`."
 
 partial def ofLetOrReassignArrow (reassignment : Bool) (decl : TSyntax [``doIdDecl, ``doPatDecl]) : TermElabM ControlInfo := do
   match decl with

src/Lean/Elab/Do/Legacy.lean

@@ -36,6 +36,7 @@ private def getDoSeq (doStx : Syntax) : Syntax :=
 def elabLiftMethod : TermElab := fun stx _ =>
   throwErrorAt stx "invalid use of `(<- ...)`, must be nested inside a 'do' expression"
 
+
 /-- Return true if we should not lift `(<- ...)` actions nested in the syntax nodes with the given kind. -/
 private def liftMethodDelimiter (k : SyntaxNodeKind) : Bool :=
   k == ``Parser.Term.do ||
@@ -76,9 +77,9 @@ private def liftMethodForbiddenBinder (stx : Syntax) : Bool :=
   else if k == ``Parser.Term.let then
     letDeclHasBinders stx[1]
   else if k == ``Parser.Term.doLet then
-    letDeclHasBinders stx[2]
+    letDeclHasBinders stx[3]
   else if k == ``Parser.Term.doLetArrow then
-    letDeclArgHasBinders stx[2]
+    letDeclArgHasBinders stx[3]
   else
     false
 
@@ -701,12 +702,12 @@ def getLetDeclVars (letDecl : Syntax) : TermElabM (Array Var) := do
     throwError "unexpected kind of let declaration"
 
 def getDoLetVars (doLet : Syntax) : TermElabM (Array Var) :=
-  -- leading_parser "let " >> optional "mut " >> letDecl
-  getLetDeclVars doLet[2]
+  -- leading_parser "let " >> optional "mut " >> letConfig >> letDecl
+  getLetDeclVars doLet[3]
 
 def getDoHaveVars (doHave : Syntax) : TermElabM (Array Var) :=
-  -- leading_parser "have" >> letDecl
-  getLetDeclVars doHave[1]
+  -- leading_parser "have" >> letConfig >> letDecl
+  getLetDeclVars doHave[2]
 
 def getDoLetRecVars (doLetRec : Syntax) : TermElabM (Array Var) := do
   -- letRecDecls is an array of `(group (optional attributes >> letDecl))`
@@ -727,9 +728,9 @@ def getDoPatDeclVars (doPatDecl : Syntax) : TermElabM (Array Var) := do
   let pattern := doPatDecl[0]
   getPatternVarsEx pattern
 
--- leading_parser "let " >> optional "mut " >> (doIdDecl <|> doPatDecl)
+-- leading_parser "let " >> optional "mut " >> letConfig >> (doIdDecl <|> doPatDecl)
 def getDoLetArrowVars (doLetArrow : Syntax) : TermElabM (Array Var) := do
-  let decl := doLetArrow[2]
+  let decl := doLetArrow[3]
   if decl.getKind == ``Parser.Term.doIdDecl then
     return #[getDoIdDeclVar decl]
   else if decl.getKind == ``Parser.Term.doPatDecl then
@@ -1060,14 +1061,15 @@ def seqToTerm (action : Syntax) (k : Syntax) : M Syntax := withRef action <| wit
 def declToTerm (decl : Syntax) (k : Syntax) : M Syntax := withRef decl <| withFreshMacroScope do
   let kind := decl.getKind
   if kind == ``Parser.Term.doLet then
-    let letDecl := decl[2]
-    `(let $letDecl:letDecl; $k)
+    let letConfig : TSyntax ``Parser.Term.letConfig := ⟨decl[2]⟩
+    let letDecl := decl[3]
+    `(let $letConfig:letConfig $letDecl:letDecl; $k)
   else if kind == ``Parser.Term.doLetRec then
     let letRecToken := decl[0]
     let letRecDecls := decl[1]
     return mkNode ``Parser.Term.letrec #[letRecToken, letRecDecls, mkNullNode, k]
   else if kind == ``Parser.Term.doLetArrow then
-    let arg := decl[2]
+    let arg := decl[3]
     if arg.getKind == ``Parser.Term.doIdDecl then
       let id     := arg[0]
       let type   := expandOptType id arg[1]
@@ -1415,7 +1417,7 @@ mutual
   /-- Generate `CodeBlock` for `doLetArrow; doElems`
      `doLetArrow` is of the form
      ```
-     "let " >> optional "mut " >> (doIdDecl <|> doPatDecl)
+     "let " >> optional "mut " >> letConfig >> (doIdDecl <|> doPatDecl)
      ```
      where
      ```
@@ -1424,7 +1426,7 @@ mutual
      ```
   -/
   partial def doLetArrowToCode (doLetArrow : Syntax) (doElems : List Syntax) : M CodeBlock := do
-    let decl    := doLetArrow[2]
+    let decl    := doLetArrow[3]
     if decl.getKind == ``Parser.Term.doIdDecl then
       let y := decl[0]
       checkNotShadowingMutable #[y]
@@ -1475,11 +1477,11 @@ mutual
       throwError "unexpected kind of `do` declaration"
 
   partial def doLetElseToCode (doLetElse : Syntax) (doElems : List Syntax) : M CodeBlock := do
-    -- "let " >> optional "mut " >> termParser >> " := " >> termParser >> (checkColGt >> " | " >> doSeq) >> optional doSeq
-    let pattern := doLetElse[2]
-    let val     := doLetElse[4]
-    let elseSeq := doLetElse[6]
-    let bodySeq := doLetElse[7][0]
+    -- "let " >> optional "mut " >> letConfig >> termParser >> " := " >> termParser >> (checkColGt >> " | " >> doSeq) >> optional doSeq
+    let pattern := doLetElse[3]
+    let val     := doLetElse[5]
+    let elseSeq := doLetElse[7]
+    let bodySeq := doLetElse[8][0]
     let contSeq ← if isMutableLet doLetElse then
       let vars ← (← getPatternVarsEx pattern).mapM fun var => `(doElem| let mut $var := $var)
       pure (vars ++ (getDoSeqElems bodySeq).toArray)
@@ -1780,10 +1782,6 @@ mutual
             doIfToCode doElem doElems
           else if k == ``Parser.Term.doUnless then
             doUnlessToCode doElem doElems
-          else if k == `Lean.doRepeat then
-            let seq := doElem[1]
-            let expanded ← `(doElem| for _ in Loop.mk do $seq)
-            doSeqToCode (expanded :: doElems)
           else if k == ``Parser.Term.doFor then withFreshMacroScope do
             doForToCode doElem doElems
           else if k == ``Parser.Term.doMatch then

src/Lean/Elab/Do/Switch.lean

@@ -19,11 +19,6 @@ register_builtin_option backward.do.legacy : Bool := {
   descr    := "Use the legacy `do` elaborator instead of the new, extensible implementation."
 }
 
-register_builtin_option backward.do.while : Bool := {
-  defValue := false
-  descr    := "Use the legacy partial `Loop` type for `repeat`/`while` loops instead of `Repeat`, which is based on `partial_fixpoint`. Useful as a workaround when the monad lacks a `MonadTail` instance."
-}
-
 private def toDoElem (newKind : SyntaxNodeKind) : Macro := fun stx => do
   let stx := stx.setKind newKind
   withRef stx `(do $(⟨stx⟩):doElem)

src/Lean/Elab/DocString.lean

@@ -85,6 +85,10 @@ structure State where
   -/
   lctx : LocalContext
   /--
+  The local instances.
+
+  The `MonadLift TermElabM DocM` instance runs the lifted action with these instances, so elaboration
+  commands that mutate this state cause it to take effect in subsequent commands.
   -/
   localInstances : LocalInstances
   /--

src/Lean/Elab/Import.lean

@@ -9,6 +9,7 @@ prelude
 public import Lean.Parser.Module
 meta import Lean.Parser.Module
 import Lean.Compiler.ModPkgExt
+public import Lean.DeprecatedModule
 
 public section
 
@@ -42,12 +43,66 @@ def HeaderSyntax.toModuleHeader (stx : HeaderSyntax) : ModuleHeader where
 
 abbrev headerToImports := @HeaderSyntax.imports
 
+/--
+Check imported modules for deprecation and emit warnings.
+
+The `-- deprecated_module: ignore` comment can be placed on the `module` keyword to suppress
+all warnings, or on individual `import` statements to suppress specific ones.
+This follows the same pattern as `-- shake: keep` in Lake shake.
+
+The `headerStx?` parameter carries the header syntax used for checking trailing comments.
+When called from the Language Server, the main header syntax may have its trailing trivia
+stripped by `unsetTrailing` for caching purposes, so `origHeaderStx?` can supply the original
+(untrimmed) syntax to preserve `-- deprecated_module: ignore` annotations on the last import.
+-/
+def checkDeprecatedImports
+    (env : Environment) (imports : Array Import) (opts : Options)
+    (inputCtx : Parser.InputContext) (startPos : String.Pos.Raw) (messages : MessageLog)
+    (headerStx? : Option HeaderSyntax := none)
+    (origHeaderStx? : Option HeaderSyntax := none)
+    : MessageLog := Id.run do
+  let mut opts := opts
+  let mut ignoreDeprecatedImports : NameSet := {}
+  if let some headerStx := origHeaderStx? <|> headerStx? then
+    match headerStx with
+    | `(Parser.Module.header| $[module%$moduleTk]? $[prelude%$_]? $importsStx*) =>
+      if moduleTk.any (·.getTrailing?.any (·.toString.contains "deprecated_module: ignore")) then
+        opts := linter.deprecated.module.set opts false
+      for impStx in importsStx do
+        if impStx.raw.getTrailing?.any (·.toString.contains "deprecated_module: ignore") then
+          match impStx with
+          | `(Parser.Module.import| $[public%$_]? $[meta%$_]? import $[all%$_]? $n) =>
+            ignoreDeprecatedImports := ignoreDeprecatedImports.insert n.getId
+          | _ => pure ()
+    | _ => pure ()
+  if !linter.deprecated.module.get opts then
+    return messages
+  imports.foldl (init := messages) fun messages imp =>
+    if ignoreDeprecatedImports.contains imp.module then
+      messages
+    else
+    match env.getModuleIdx? imp.module with
+    | some idx =>
+      match env.getDeprecatedModuleByIdx? idx with
+      | some entry =>
+        let pos := inputCtx.fileMap.toPosition startPos
+        messages.add {
+          fileName := inputCtx.fileName
+          pos := pos
+          severity := .warning
+          data := .tagged ``deprecatedModuleExt <| formatDeprecatedModuleWarning env idx imp.module entry
+        }
+      | none => messages
+    | none => messages
+
 def processHeaderCore
     (startPos : String.Pos.Raw) (imports : Array Import) (isModule : Bool)
     (opts : Options) (messages : MessageLog) (inputCtx : Parser.InputContext)
     (trustLevel : UInt32 := 0) (plugins : Array System.FilePath := #[]) (leakEnv := false)
     (mainModule := Name.anonymous) (package? : Option PkgId := none)
     (arts : NameMap ImportArtifacts := {})
+    (headerStx? : Option HeaderSyntax := none)
+    (origHeaderStx? : Option HeaderSyntax := none)
     : IO (Environment × MessageLog) := do
   let level := if isModule then
     if Elab.inServer.get opts then
@@ -66,6 +121,7 @@ def processHeaderCore
     let pos := inputCtx.fileMap.toPosition startPos
     pure (env, messages.add { fileName := inputCtx.fileName, data := toString e, pos := pos })
   let env := env.setMainModule mainModule |>.setModulePackage package?
+  let messages := checkDeprecatedImports env imports opts inputCtx startPos messages headerStx? origHeaderStx?
   return (env, messages)
 
 /--
@@ -82,6 +138,7 @@ backwards compatibility measure not compatible with the module system.
     : IO (Environment × MessageLog) := do
   processHeaderCore header.startPos header.imports header.isModule
     opts messages inputCtx trustLevel plugins leakEnv mainModule
+    (headerStx? := header)
 
 def parseImports (input : String) (fileName : Option String := none) : IO (Array Import × Position × MessageLog) := do
   let fileName := fileName.getD "<input>"

src/Lean/Elab/Match.lean

@@ -1042,7 +1042,16 @@ def mkRedundantAlternativeMsg (altName? : Option Name) (altMsg? : Option Message
 
 def reportMatcherResultErrors (altLHSS : List AltLHS) (result : MatcherResult) : TermElabM Unit := do
   unless result.counterExamples.isEmpty do
-    withHeadRefOnly <| logError m!"Missing cases:\n{Meta.Match.counterExamplesToMessageData result.counterExamples}"
+    let maxCEx := Meta.Match.match.maxCounterExamples.get (← getOptions)
+    let (shown, truncated) :=
+      if result.counterExamples.length > maxCEx then
+        (result.counterExamples.take maxCEx, true)
+      else
+        (result.counterExamples, false)
+    let mut msg := m!"Missing cases:\n{Meta.Match.counterExamplesToMessageData shown}"
+    if truncated then
+      msg := msg ++ m!"\n(further cases omitted, increase `set_option match.maxCounterExamples {maxCEx}` to see more)"
+    withHeadRefOnly <| logError msg
     return ()
   unless match.ignoreUnusedAlts.get (← getOptions) || result.unusedAltIdxs.isEmpty do
     let mut i := 0

src/Lean/Elab/PatternVar.lean

@@ -69,6 +69,8 @@ private def throwCtorExpected {α} (ident : Option Syntax) : M α := do
 
   if candidates.size = 0 then
     throwError message
+  -- Sort for deterministic output (iteration order of `env.constants` is not stable)
+  candidates := candidates.qsort Name.lt
   let oneOfThese := if h : candidates.size = 1 then m!"`{candidates[0]}`" else m!"one of these"
   let hint ← m!"Using {oneOfThese} would be valid:".hint (ref? := idStx) (candidates.map fun candidate => {
     suggestion := mkIdent candidate
@@ -320,7 +322,7 @@ where
     if f.getKind == ``Parser.Term.dotIdent then
       let namedArgsNew ← namedArgs.mapM fun
         -- We must ensure that `ref[1]` remains original to allow named-argument hints
-        | { ref, name, val := Arg.stx arg } => withRef ref do `(Lean.Parser.Term.namedArgument| ($(ref[1]) := $(← collect arg)))
+        | { ref, name, val := Arg.stx arg, .. } => withRef ref do `(Lean.Parser.Term.namedArgument| ($(ref[1]) := $(← collect arg)))
         | _ => unreachable!
       let mut argsNew ← args.mapM fun | Arg.stx arg => collect arg | _ => unreachable!
       if ellipsis then

src/Lean/Elab/PreDefinition/WF/Unfold.lean

@@ -73,8 +73,9 @@ def splitMatchOrCasesOn (mvarId : MVarId) (e : Expr) (matcherInfo : MatcherInfo)
   if (← isMatcherApp e) then
     Split.splitMatch mvarId e
   else
-    assert! matcherInfo.numDiscrs = 1
-    let discr := e.getAppArgs[matcherInfo.numParams + 1]!
+    -- For casesOn, the last discriminant is the major premise;
+    -- `cases` will handle any index discriminants automatically.
+    let discr := e.getAppArgs[matcherInfo.numParams + matcherInfo.numDiscrs]!
     assert! discr.isFVar
     let subgoals ← mvarId.cases discr.fvarId!
     return subgoals.map (·.mvarId) |>.toList

src/Lean/Elab/Quotation/Precheck.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lean.Elab.Quotation.Util
+import Lean.Elab.DeprecatedSyntax
 
 public section
 
@@ -56,6 +57,14 @@ unsafe builtin_initialize precheckAttribute : KeyedDeclsAttribute Precheck ←
   }
 
 partial def precheck : Precheck := fun stx => do
+  -- Check for deprecated syntax kinds in quotations
+  if let some entry := (deprecatedSyntaxExt.getState (← getEnv)).find? stx.getKind then
+    let extraMsg := match entry.text? with
+      | some text => m!": {text}"
+      | none => m!""
+    withRef stx do
+      Linter.logLintIf Linter.linter.deprecated.syntax stx
+        m!"quotation uses deprecated syntax '{stx.getKind}'{extraMsg}"
   if let p::_ := precheckAttribute.getValues (← getEnv) stx.getKind then
     if ← catchInternalId unsupportedSyntaxExceptionId (do withRef stx <| p stx; pure true) (fun _ => pure false) then
       return

src/Lean/Elab/SetOption.lean

@@ -12,6 +12,11 @@ public import Init.Syntax
 public section
 namespace Lean.Elab
 
+register_builtin_option linter.deprecated.options : Bool := {
+  defValue := true
+  descr := "if true, generate deprecation warnings for deprecated options"
+}
+
 variable [Monad m] [MonadOptions m] [MonadError m] [MonadLiftT (EIO Exception) m] [MonadInfoTree m]
 
 private def throwUnconfigurable {α} (optionName : Name) : m α :=
@@ -43,7 +48,7 @@ where
         {indentExpr defValType}"
     | _ => throwUnconfigurable optionName
 
-def elabSetOption (id : Syntax) (val : Syntax) : m Options := do
+def elabSetOption (id : Syntax) (val : Syntax) : m (Options × OptionDecl) := do
   let ref ← getRef
   -- For completion purposes, we discard `val` and any later arguments.
   -- We include the first argument (the keyword) for position information in case `id` is `missing`.
@@ -51,9 +56,9 @@ def elabSetOption (id : Syntax) (val : Syntax) : m Options := do
   let optionName := id.getId.eraseMacroScopes
   let decl ← IO.toEIO (fun (ex : IO.Error) => Exception.error ref ex.toString) (getOptionDecl optionName)
   pushInfoLeaf <| .ofOptionInfo { stx := id, optionName, declName := decl.declName }
-  let rec setOption (val : DataValue) : m Options := do
+  let rec setOption (val : DataValue) : m (Options × OptionDecl) := do
     validateOptionValue optionName decl val
-    return (← getOptions).set optionName val
+    return ((← getOptions).set optionName val, decl)
   match val.isStrLit? with
   | some str => setOption (DataValue.ofString str)
   | none     =>
@@ -70,3 +75,17 @@ def elabSetOption (id : Syntax) (val : Syntax) : m Options := do
       throwUnconfigurable optionName
 
 end Lean.Elab
+
+namespace Lean.Elab
+
+variable {m : Type → Type} [Monad m] [MonadOptions m] [MonadLog m] [AddMessageContext m]
+
+def checkDeprecatedOption (optionName : Name) (decl : OptionDecl) : m Unit := do
+  unless linter.deprecated.options.get (← getOptions) do return
+  let some dep := decl.deprecation? | return
+  let extraMsg := match dep.text? with
+    | some text => m!": {text}"
+    | none => m!""
+  logWarning m!"`{optionName}` has been deprecated{extraMsg}"
+
+end Lean.Elab

src/Lean/Elab/StructInst.lean

@@ -574,8 +574,14 @@ private def addSourceFields (structName : Name) (sources : Array ExplicitSourceV
 
 private structure StructInstContext where
   view : StructInstView
-  /-- True if the structure instance has a trailing `..`. -/
-  ellipsis : Bool
+  /-- If true, then try using parent instances for missing fields. -/
+  useParentInstanceFields : Bool
+  /-- If true, then try using default values or autoParams for missing fields.
+  (Considered after `useParentInstanceFields`.) -/
+  useDefaults : Bool
+  /-- If true, then missing fields after default value synthesis remain as metavariables rather than yielding an error.
+  Only applies if `useDefaults` is true. -/
+  unsynthesizedAsMVars : Bool
   structName : Name
   structType : Expr
   /-- Structure universe levels. -/
@@ -748,6 +754,8 @@ private structure PendingField where
   deps : NameSet
   val? : Option Expr
 
+private def registerFieldMVarError (e : Expr) (ref : Syntax) (fieldName : Name) : StructInstM Unit :=
+  registerCustomErrorIfMVar e ref m!"Cannot synthesize placeholder for field `{fieldName}`"
 
 /--
 Synthesize pending optParams.
@@ -778,7 +786,7 @@ private def synthOptParamFields : StructInstM Unit := do
   -- Process default values for pending optParam fields.
   let mut pendingFields : Array PendingField ← optParamFields.filterMapM fun (fieldName, fieldType, required) => do
     if required || (← isFieldNotSolved? fieldName).isSome then
-      let (deps, val?) ← getFieldDefaultValue? fieldName
+      let (deps, val?) ← if (← read).useDefaults then getFieldDefaultValue? fieldName else pure ({}, none)
       if let some val := val? then
         trace[Elab.struct] "default value for {fieldName}:{indentExpr val}"
       else
@@ -831,44 +839,46 @@ private def synthOptParamFields : StructInstM Unit := do
               pending
         toRemove := toRemove.push selected.fieldName
     if toRemove.isEmpty then
-      if (← read).ellipsis then
-        for pendingField in pendingFields do
-          if let some mvarId ← isFieldNotSolved? pendingField.fieldName then
-            registerCustomErrorIfMVar (.mvar mvarId) (← read).view.ref m!"\
-              Cannot synthesize placeholder for field `{pendingField.fieldName}`"
-        return
-      let assignErrorsMsg := MessageData.joinSep (assignErrors.map (m!"\n\n" ++ ·)).toList ""
-      let mut requiredErrors : Array MessageData := #[]
-      let mut unsolvedFields : Std.HashSet Name := {}
-      for pendingField in pendingFields do
-        if (← isFieldNotSolved? pendingField.fieldName).isNone then
-          unsolvedFields := unsolvedFields.insert pendingField.fieldName
-          let e := (← get).fieldMap.get! pendingField.fieldName
-          requiredErrors := requiredErrors.push m!"\
-            Field `{pendingField.fieldName}` must be explicitly provided; its synthesized value is{indentExpr e}"
-      let requiredErrorsMsg := MessageData.joinSep (requiredErrors.map (m!"\n\n" ++ ·)).toList ""
-      let missingFields := pendingFields |>.filter (fun pending => pending.val?.isNone)
-      -- TODO(kmill): when fields are all stuck, report better.
-      -- For now, just report all pending fields in case there are no obviously missing ones.
-      let missingFields := if missingFields.isEmpty then pendingFields else missingFields
-      let missing := missingFields |>.map (s!"`{·.fieldName}`") |>.toList
-      let missingFieldsValues ← missingFields.mapM fun field => do
-        if unsolvedFields.contains field.fieldName then
-          pure <| (field.fieldName, some <| (← get).fieldMap.get! field.fieldName)
-        else pure (field.fieldName, none)
-      let missingFieldsHint ← mkMissingFieldsHint missingFieldsValues (← read).view.ref
-      let msg := m!"Fields missing: {", ".intercalate missing}{assignErrorsMsg}{requiredErrorsMsg}{missingFieldsHint}"
-      if (← readThe Term.Context).errToSorry then
-        -- Assign all pending problems using synthetic sorries and log an error.
-        for pendingField in pendingFields do
-          if let some mvarId ← isFieldNotSolved? pendingField.fieldName then
-            mvarId.assign <| ← mkLabeledSorry (← mvarId.getType) (synthetic := true) (unique := true)
-        logError msg
-        return
-      else
-        throwError msg
+      return ← handleStuck pendingFields assignErrors
     pendingSet := pendingSet.filter (!toRemove.contains ·)
     pendingFields := pendingFields.filter fun pendingField => pendingField.val?.isNone || !toRemove.contains pendingField.fieldName
+where
+  handleStuck (pendingFields : Array PendingField) (assignErrors : Array MessageData) : StructInstM Unit := do
+    if (← read).unsynthesizedAsMVars then
+      for pendingField in pendingFields do
+        if let some mvarId ← isFieldNotSolved? pendingField.fieldName then
+          registerFieldMVarError (.mvar mvarId) (← read).view.ref pendingField.fieldName
+      return
+    let assignErrorsMsg := MessageData.joinSep (assignErrors.map (m!"\n\n" ++ ·)).toList ""
+    let mut requiredErrors : Array MessageData := #[]
+    let mut unsolvedFields : Std.HashSet Name := {}
+    for pendingField in pendingFields do
+      if (← isFieldNotSolved? pendingField.fieldName).isNone then
+        unsolvedFields := unsolvedFields.insert pendingField.fieldName
+        let e := (← get).fieldMap.get! pendingField.fieldName
+        requiredErrors := requiredErrors.push m!"\
+          Field `{pendingField.fieldName}` must be explicitly provided; its synthesized value is{indentExpr e}"
+    let requiredErrorsMsg := MessageData.joinSep (requiredErrors.map (m!"\n\n" ++ ·)).toList ""
+    let missingFields := pendingFields |>.filter (fun pending => pending.val?.isNone)
+    -- TODO(kmill): when fields are all stuck, report better.
+    -- For now, just report all pending fields in case there are no obviously missing ones.
+    let missingFields := if missingFields.isEmpty then pendingFields else missingFields
+    let missing := missingFields |>.map (s!"`{·.fieldName}`") |>.toList
+    let missingFieldsValues ← missingFields.mapM fun field => do
+      if unsolvedFields.contains field.fieldName then
+        pure <| (field.fieldName, some <| (← get).fieldMap.get! field.fieldName)
+      else pure (field.fieldName, none)
+    let missingFieldsHint ← mkMissingFieldsHint missingFieldsValues (← read).view.ref
+    let msg := m!"Fields missing: {", ".intercalate missing}{assignErrorsMsg}{requiredErrorsMsg}{missingFieldsHint}"
+    if (← readThe Term.Context).errToSorry then
+      -- Assign all pending problems using synthetic sorries and log an error.
+      for pendingField in pendingFields do
+        if let some mvarId ← isFieldNotSolved? pendingField.fieldName then
+          mvarId.assign <| ← mkLabeledSorry (← mvarId.getType) (synthetic := true) (unique := true)
+      logError msg
+      return
+    else
+      throwError msg
 
 private def finalize : StructInstM Expr := withViewRef do
   let val := (← read).val.beta (← get).fields
@@ -1049,19 +1059,13 @@ These fields can still be solved for by parent instance synthesis later.
 -/
 private def processNoField (loop : StructInstM α) (fieldName : Name) (binfo : BinderInfo) (fieldType : Expr) : StructInstM α := do
   trace[Elab.struct] "processNoField `{fieldName}` of type {fieldType}"
-  if (← read).ellipsis && (← readThe Term.Context).inPattern then
-    -- See the note in `ElabAppArgs.processExplicitArg`
-    -- In ellipsis & pattern mode, do not use optParams or autoParams.
-    let e ← addStructFieldMVar fieldName fieldType
-    registerCustomErrorIfMVar e (← read).view.ref m!"don't know how to synthesize placeholder for field `{fieldName}`"
-    loop
-  else
+  if (← read).useDefaults then
     let autoParam? := fieldType.getAutoParamTactic?
     let fieldType := fieldType.consumeTypeAnnotations
     if binfo.isInstImplicit then
       let e ← addStructFieldMVar fieldName fieldType .synthetic
       modify fun s => { s with instMVars := s.instMVars.push e.mvarId! }
-      loop
+      return ← loop
     else if let some (.const tacticDecl ..) := autoParam? then
       match evalSyntaxConstant (← getEnv) (← getOptions) tacticDecl with
       | .error err       => throwError err
@@ -1078,12 +1082,11 @@ private def processNoField (loop : StructInstM α) (fieldName : Name) (binfo : B
         -- (See `processExplicitArg` for a comment about this.)
         addTermInfo' stx mvar
         addStructFieldAux fieldName mvar
-        loop
-    else
-      -- Default case: natural metavariable, register it for optParams
-      discard <| addStructFieldMVar fieldName fieldType
-      modify fun s => { s with optParamFields := s.optParamFields.push (fieldName, fieldType, binfo.isExplicit) }
-      loop
+        return ← loop
+  -- Default case: natural metavariable, register it for optParams
+  discard <| addStructFieldMVar fieldName fieldType
+  modify fun s => { s with optParamFields := s.optParamFields.push (fieldName, fieldType, binfo.isExplicit) }
+  loop
 
 private partial def loop : StructInstM Expr := withViewRef do
   let type := (← get).type
@@ -1178,8 +1181,7 @@ private partial def addParentInstanceFields : StructInstM Unit := do
 
 private def main : StructInstM Expr := do
   initializeState
-  unless (← read).ellipsis && (← readThe Term.Context).inPattern do
-    -- Inside a pattern with ellipsis mode, users expect to match just the fields provided.
+  if (← read).useParentInstanceFields then
     addParentInstanceFields
   loop
 
@@ -1198,7 +1200,17 @@ private def elabStructInstView (s : StructInstView) (structName : Name) (structT
   trace[Elab.struct] "expanded fields:\n{MessageData.joinSep (fields.toList.map (fun (_, field) => m!"- {MessageData.nestD (toMessageData field)}")) "\n"}"
   let ellipsis := s.sources.implicit.isSome
   let (val, _) ← main
-    |>.run { view := s, structName, structType, levels, params, fieldViews := fields, val := ctorFn, ellipsis }
+    |>.run { view := s, structName, structType, levels, params, fieldViews := fields, val := ctorFn
+             -- See the note in `ElabAppArgs.processExplicitArg`
+             -- For structure instances though, there's a sense in which app-style ellipsis mode is always enabled,
+             -- so we do not specifically check for it to disable defaults.
+             -- An effect of this is that if a user forgets `..` they'll be reminded with a "Fields missing" error.
+             useDefaults := !(← readThe Term.Context).inPattern
+             -- Similarly, for patterns we disable using parent instances to fill in fields
+             useParentInstanceFields := !(← readThe Term.Context).inPattern
+             -- In ellipsis mode, unsynthesized missing fields become metavariables, rather than being an error
+             unsynthesizedAsMVars := ellipsis
+     }
     |>.run { type := ctorFnType }
   return val
 

src/Lean/Elab/SyntheticMVars.lean

@@ -582,6 +582,7 @@ mutual
     -- We use `filterRevM` instead of `filterM` to make sure we process the synthetic metavariables using the order they were created.
     -- It would not be incorrect to use `filterM`.
     let remainingPendingMVars ← pendingMVars.filterRevM fun mvarId => do
+       checkSystem "synthesize pending MVars"
        -- We use `traceM` because we want to make sure the metavar local context is used to trace the message
        traceM `Elab.postpone (mvarId.withContext do addMessageContext m!"resuming {mkMVar mvarId}")
        let succeeded ← synthesizeSyntheticMVar mvarId postponeOnError runTactics

src/Lean/Elab/Tactic/Basic.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Lean.Meta.Tactic.Util
 public import Lean.Elab.Term
+import Lean.Elab.DeprecatedSyntax
 import Init.Omega
 
 public section
@@ -192,6 +193,7 @@ partial def evalTactic (stx : Syntax) : TacticM Unit := do
         Term.withoutTacticIncrementality true <| withTacticInfoContext stx do
           stx.getArgs.forM evalTactic
       else withTraceNode `Elab.step (fun _ => return stx) (tag := stx.getKind.toString) do
+        checkDeprecatedSyntax stx (← readThe Term.Context).macroStack
         let evalFns := tacticElabAttribute.getEntries (← getEnv) stx.getKind
         let macros  := macroAttribute.getEntries (← getEnv) stx.getKind
         if evalFns.isEmpty && macros.isEmpty then

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -190,7 +190,8 @@ private def getOptRotation (stx : Syntax) : Nat :=
     popScope
 
 @[builtin_tactic Parser.Tactic.set_option] def elabSetOption : Tactic := fun stx => do
-  let options ← Elab.elabSetOption stx[1] stx[3]
+  let (options, decl) ← Elab.elabSetOption stx[1] stx[3]
+  withRef stx[1] <| Elab.checkDeprecatedOption (stx[1].getId.eraseMacroScopes) decl
   withOptions (fun _ => options) do
     try
       evalTactic stx[5]

src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean

@@ -437,7 +437,8 @@ where
   replaceMainGoal [{ goal with mvarId }]
 
 @[builtin_grind_tactic setOption] def elabSetOption : GrindTactic := fun stx => do
-  let options ← Elab.elabSetOption stx[1] stx[3]
+  let (options, decl) ← Elab.elabSetOption stx[1] stx[3]
+  withRef stx[1] <| Elab.checkDeprecatedOption (stx[1].getId.eraseMacroScopes) decl
   withOptions (fun _ => options) do evalGrindTactic stx[5]
 
 @[builtin_grind_tactic setConfig] def elabSetConfig : GrindTactic := fun stx => do

src/Lean/Elab/Tactic/Grind/Config.lean

@@ -7,6 +7,8 @@ module
 prelude
 public import Lean.Elab.Tactic.Grind.Basic
 import Lean.Elab.Tactic.ConfigSetter
+import Lean.Elab.DeprecatedSyntax  -- shake: skip (workaround for `mkConfigSetter` failing to interpret `deprecatedSyntaxExt`, to be fixed)
+
 public section
 namespace Lean.Elab.Tactic.Grind
 

src/Lean/Elab/Term/TermElabM.lean

@@ -9,6 +9,7 @@ prelude
 public import Lean.Meta.Coe
 public import Lean.Util.CollectLevelMVars
 public import Lean.Linter.Deprecated
+import Lean.Elab.DeprecatedSyntax
 public import Lean.Elab.Attributes
 public import Lean.Elab.Level
 public import Lean.Elab.PreDefinition.TerminationHint
@@ -1794,6 +1795,7 @@ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone :
     withTraceNode `Elab.step (fun _ => return m!"expected type: {expectedType?}, term\n{stx}")
       (tag := stx.getKind.toString) do
     checkSystem "elaborator"
+    checkDeprecatedSyntax stx (← read).macroStack
     let env ← getEnv
     let result ← match (← liftMacroM (expandMacroImpl? env stx)) with
     | some (decl, stxNew?) =>
@@ -2122,11 +2124,14 @@ private def mkConsts (candidates : List (Name × List String)) (explicitLevels :
     let const ← withoutCheckDeprecated <| mkConst declName explicitLevels
     return (const, projs) :: result
 
+def throwInvalidExplicitUniversesForLocal {α} (e : Expr) : TermElabM α :=
+  throwError "invalid use of explicit universe parameters, `{e}` is a local variable"
+
 def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String)) := do
   addCompletionInfo <| CompletionInfo.id stx stx.getId (danglingDot := false) (← getLCtx) expectedType?
   if let some (e, projs) ← resolveLocalName n then
     unless explicitLevels.isEmpty do
-      throwError "invalid use of explicit universe parameters, `{e}` is a local variable"
+      throwInvalidExplicitUniversesForLocal e
     return [(e, projs)]
   let preresolved := preresolved.filterMap fun
     | .decl n projs => some (n, projs)

src/Lean/Environment.lean

@@ -2255,13 +2255,13 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
     return data
   let numPrivateConsts := moduleData.foldl (init := 0) fun numPrivateConsts data =>
     numPrivateConsts + data.constants.size
-  let numPrivateConsts := irData.foldl (init := numPrivateConsts) fun numPrivateConsts data =>
-    numPrivateConsts + data.extraConstNames.size
+  let numExtraConsts := irData.foldl (init := 0) fun numExtraConsts data =>
+    numExtraConsts + data.extraConstNames.size
   let numPublicConsts := modules.foldl (init := 0) fun numPublicConsts mod => Id.run do
     if !mod.isExported then numPublicConsts else
       let some data := mod.publicModule? | numPublicConsts
       numPublicConsts + data.constants.size
-  let mut const2ModIdx : Std.HashMap Name ModuleIdx := Std.HashMap.emptyWithCapacity (capacity := numPrivateConsts + numPublicConsts)
+  let mut const2ModIdx : Std.HashMap Name ModuleIdx := Std.HashMap.emptyWithCapacity (capacity := numPrivateConsts + numExtraConsts)
   let mut privateConstantMap : Std.HashMap Name ConstantInfo := Std.HashMap.emptyWithCapacity (capacity := numPrivateConsts)
   let mut publicConstantMap : Std.HashMap Name ConstantInfo := Std.HashMap.emptyWithCapacity (capacity := numPublicConsts)
   for h : modIdx in *...moduleData.size do

src/Lean/Exception.lean

@@ -245,7 +245,7 @@ We use this combinator to prevent stack overflows.
 @[inline] def withIncRecDepth [Monad m] [MonadError m] [MonadRecDepth m] (x : m α) : m α := do
   let curr ← MonadRecDepth.getRecDepth
   let max  ← MonadRecDepth.getMaxRecDepth
-  if curr == max then
+  if max != 0 && curr == max then
     throwMaxRecDepthAt (← getRef)
   else
     MonadRecDepth.withRecDepth (curr+1) x

src/Lean/Language/Lean.lean

@@ -478,11 +478,11 @@ where
         }
         result? := some {
           parserState
-          processedSnap := (← processHeader ⟨trimmedStx⟩ parserState)
+          processedSnap := (← processHeader ⟨trimmedStx⟩ stx parserState)
         }
       }
 
-  processHeader (stx : HeaderSyntax) (parserState : Parser.ModuleParserState) :
+  processHeader (stx : HeaderSyntax) (origStx : HeaderSyntax) (parserState : Parser.ModuleParserState) :
       LeanProcessingM (SnapshotTask HeaderProcessedSnapshot) := do
     let ctx ← read
     SnapshotTask.ofIO none none (.some ⟨0, ctx.endPos⟩) <|
@@ -498,6 +498,7 @@ where
       let (headerEnv, msgLog) ← Elab.processHeaderCore (leakEnv := true)
         stx.startPos setup.imports setup.isModule setup.opts .empty ctx.toInputContext
         setup.trustLevel setup.plugins setup.mainModuleName setup.package? setup.importArts
+        (headerStx? := stx) (origHeaderStx? := origStx)
       let stopTime := (← IO.monoNanosNow).toFloat / 1000000000
       let diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog)
       if msgLog.hasErrors then

src/Lean/Level.lean

@@ -441,18 +441,27 @@ def Result.imax : Result → Result → Result
   | f, Result.imaxNode Fs => Result.imaxNode (f::Fs)
   | f₁, f₂                => Result.imaxNode [f₁, f₂]
 
-def toResult (l : Level) (mvars : Bool) : Result :=
+structure Context where
+  mvars : Bool
+  lIndex? : LMVarId → Option Nat
+
+abbrev M := ReaderM Context
+
+def toResult (l : Level) : M Result := do
   match l with
-  | zero       => Result.num 0
-  | succ l     => Result.succ (toResult l mvars)
-  | max l₁ l₂  => Result.max (toResult l₁ mvars) (toResult l₂ mvars)
-  | imax l₁ l₂ => Result.imax (toResult l₁ mvars) (toResult l₂ mvars)
-  | param n    => Result.leaf n
+  | zero       => return Result.num 0
+  | succ l     => return Result.succ (← toResult l)
+  | max l₁ l₂  => return Result.max (← toResult l₁) (← toResult l₂)
+  | imax l₁ l₂ => return Result.imax (← toResult l₁) (← toResult l₂)
+  | param n    => return Result.leaf n
   | mvar n     =>
-    if mvars then
-      Result.leaf <| n.name.replacePrefix `_uniq (Name.mkSimple "?u")
+    if !(← read).mvars then
+      return Result.leaf `_
+    else if let some i := (← read).lIndex? n then
+      return Result.leaf <| Name.num (Name.mkSimple "?u") (i + 1)
     else
-      Result.leaf `_
+      -- Undefined mvar, use internal name
+      return Result.leaf <| n.name.replacePrefix `_uniq (Name.mkSimple "?_mvar")
 
 private def parenIfFalse : Format → Bool → Format
   | f, true  => f
@@ -469,7 +478,7 @@ mutual
     | Result.offset f 0,     r => format f r
     | Result.offset f (k+1), r =>
       let f' := format f false;
-      parenIfFalse (f' ++ "+" ++ Std.format (k+1)) r
+      parenIfFalse (f' ++ " + " ++ Std.format (k+1)) r
     | Result.maxNode fs,    r => parenIfFalse (Format.group <| "max"  ++ formatLst fs) r
     | Result.imaxNode fs,   r => parenIfFalse (Format.group <| "imax" ++ formatLst fs) r
 end
@@ -487,20 +496,20 @@ protected partial def Result.quote (r : Result) (prec : Nat) : Syntax.Level :=
 
 end PP
 
-protected def format (u : Level) (mvars : Bool) : Format :=
-  (PP.toResult u mvars).format true
+protected def format (u : Level) (mvars : Bool) (lIndex? : LMVarId → Option Nat) : Format :=
+  (PP.toResult u) |>.run { mvars, lIndex? } |>.format true
 
 instance : ToFormat Level where
-  format u := Level.format u (mvars := true)
+  format u := Level.format u (mvars := true) (lIndex? := fun _ => none)
 
 instance : ToString Level where
   toString u := Format.pretty (format u)
 
-protected def quote (u : Level) (prec : Nat := 0) (mvars : Bool := true) : Syntax.Level :=
-  (PP.toResult u (mvars := mvars)).quote prec
+protected def quote (u : Level) (prec : Nat := 0) (mvars : Bool := true) (lIndex? : LMVarId → Option Nat) : Syntax.Level :=
+  (PP.toResult u) |>.run { mvars, lIndex? } |>.quote prec
 
 instance : Quote Level `level where
-  quote := Level.quote
+  quote := Level.quote (lIndex? := fun _ => none)
 
 end Level
 

src/Lean/LibrarySuggestions/SymbolFrequency.lean

@@ -66,7 +66,11 @@ Helper function for running `MetaM` code during module export, when there is not
 Panics on errors.
 -/
 unsafe def _root_.Lean.Environment.unsafeRunMetaM [Inhabited α] (env : Environment) (x : MetaM α) : α :=
-   match unsafeEIO ((((withoutExporting x).run' {} {}).run' { fileName := "symbolFrequency", fileMap := default } { env })) with
+   match unsafeEIO ((((withoutExporting x).run' {} {}).run'
+    { fileName := "symbolFrequency", fileMap := default
+      -- avoid triggering since limit cannot be raised here
+      maxHeartbeats := 0 }
+    { env })) with
    | Except.ok a => a
    | Except.error ex => panic! match unsafeIO ex.toMessageData.toString with
      | Except.ok s => s

src/Lean/Linter/MissingDocs.lean

@@ -112,15 +112,37 @@ builtin_initialize
 def lint (stx : Syntax) (msg : String) : CommandElabM Unit :=
   logLint linter.missingDocs stx m!"missing doc string for {msg}"
 
+def lintEmpty (stx : Syntax) (msg : String) : CommandElabM Unit :=
+  logLint linter.missingDocs stx m!"empty doc string for {msg}"
+
 def lintNamed (stx : Syntax) (msg : String) : CommandElabM Unit :=
   lint stx s!"{msg} {stx.getId}"
 
+def lintEmptyNamed (stx : Syntax) (msg : String) : CommandElabM Unit :=
+  lintEmpty stx s!"{msg} {stx.getId}"
+
 def lintField (parent stx : Syntax) (msg : String) : CommandElabM Unit :=
   lint stx s!"{msg} {parent.getId}.{stx.getId}"
 
+def lintEmptyField (parent stx : Syntax) (msg : String) : CommandElabM Unit :=
+  lintEmpty stx s!"{msg} {parent.getId}.{stx.getId}"
+
 def lintStructField (parent stx : Syntax) (msg : String) : CommandElabM Unit :=
   lint stx s!"{msg} {parent.getId}.{stx.getId}"
 
+private def isEmptyDocString (docOpt : Syntax) : CommandElabM Bool := do
+  if docOpt.isNone then return false
+  let docStx : TSyntax `Lean.Parser.Command.docComment := ⟨docOpt[0]⟩
+  -- Verso doc comments with interpolated content cannot be extracted as plain text,
+  -- but they are clearly not empty.
+  if let .node _ `Lean.Parser.Command.versoCommentBody _ := docStx.raw[1] then
+    if !docStx.raw[1][0].isAtom then return false
+  let text ← getDocStringText docStx
+  return text.trimAscii.isEmpty
+
+def isMissingDoc (docOpt : Syntax) : CommandElabM Bool := do
+  return docOpt.isNone || (← isEmptyDocString docOpt)
+
 def hasInheritDoc (attrs : Syntax) : Bool :=
   attrs[0][1].getSepArgs.any fun attr =>
     attr[1].isOfKind ``Parser.Attr.simple &&
@@ -130,38 +152,68 @@ def hasTacticAlt (attrs : Syntax) : Bool :=
   attrs[0][1].getSepArgs.any fun attr =>
     attr[1].isOfKind ``Parser.Attr.tactic_alt
 
-def declModifiersPubNoDoc (mods : Syntax) : CommandElabM Bool := do
+def declModifiersDocStatus (mods : Syntax) : CommandElabM (Option Bool) := do
   let isPublic := if (← getEnv).header.isModule && !(← getScope).isPublic then
     mods[2][0].getKind == ``Command.public else
     mods[2][0].getKind != ``Command.private
-  return isPublic && mods[0].isNone && !hasInheritDoc mods[1]
+  if !isPublic || hasInheritDoc mods[1] then return none
+  if mods[0].isNone then return some false
+  if (← isEmptyDocString mods[0]) then return some true
+  return none
 
-def lintDeclHead (k : SyntaxNodeKind) (id : Syntax) : CommandElabM Unit := do
-  if k == ``«abbrev» then lintNamed id "public abbrev"
-  else if k == ``definition then lintNamed id "public def"
-  else if k == ``«opaque» then lintNamed id "public opaque"
-  else if k == ``«axiom» then lintNamed id "public axiom"
-  else if k == ``«inductive» then lintNamed id "public inductive"
-  else if k == ``classInductive then lintNamed id "public inductive"
-  else if k == ``«structure» then lintNamed id "public structure"
+def declModifiersPubNoDoc (mods : Syntax) : CommandElabM Bool := do
+  return (← declModifiersDocStatus mods).isSome
+
+private def lintDocStatus (isEmpty : Bool) (stx : Syntax) (msg : String) : CommandElabM Unit :=
+  if isEmpty then lintEmpty stx msg else lint stx msg
+
+private def lintDocStatusNamed (isEmpty : Bool) (stx : Syntax) (msg : String) : CommandElabM Unit :=
+  if isEmpty then lintEmptyNamed stx msg else lintNamed stx msg
+
+private def lintDocStatusField (isEmpty : Bool) (parent stx : Syntax) (msg : String) :
+    CommandElabM Unit :=
+  if isEmpty then lintEmptyField parent stx msg else lintField parent stx msg
+
+def lintDeclHead (k : SyntaxNodeKind) (id : Syntax) (isEmpty : Bool := false) :
+    CommandElabM Unit := do
+  if k == ``«abbrev» then lintDocStatusNamed isEmpty id "public abbrev"
+  else if k == ``definition then lintDocStatusNamed isEmpty id "public def"
+  else if k == ``«opaque» then lintDocStatusNamed isEmpty id "public opaque"
+  else if k == ``«axiom» then lintDocStatusNamed isEmpty id "public axiom"
+  else if k == ``«inductive» then lintDocStatusNamed isEmpty id "public inductive"
+  else if k == ``classInductive then lintDocStatusNamed isEmpty id "public inductive"
+  else if k == ``«structure» then lintDocStatusNamed isEmpty id "public structure"
+
+private def docOptStatus (docOpt attrs : Syntax) (checkTacticAlt := false) :
+    CommandElabM (Option Bool) := do
+  if hasInheritDoc attrs then return none
+  if checkTacticAlt && hasTacticAlt attrs then return none
+  if docOpt.isNone then return some false
+  if (← isEmptyDocString docOpt) then return some true
+  return none
 
 @[builtin_missing_docs_handler declaration]
 def checkDecl : SimpleHandler := fun stx => do
   let head := stx[0]; let rest := stx[1]
   if head[2][0].getKind == ``Command.private then return -- not private
   let k := rest.getKind
-  if (← declModifiersPubNoDoc head) then -- no doc string
-    lintDeclHead k rest[1][0]
+  if let some isEmpty ← declModifiersDocStatus head then
+    lintDeclHead k rest[1][0] isEmpty
   if k == ``«inductive» || k == ``classInductive then
     for stx in rest[4].getArgs do
       let head := stx[2]
-      if stx[0].isNone && (← declModifiersPubNoDoc head) then
-        lintField rest[1][0] stx[3] "public constructor"
+      -- Constructor has two doc comment positions: the leading one before `|` (stx[0])
+      -- and the one inside declModifiers (head[0]). If either is non-empty, skip.
+      let leadingEmpty ← isEmptyDocString stx[0]
+      if !stx[0].isNone && !leadingEmpty then
+        pure () -- constructor has a non-empty leading doc comment
+      else if let some modsEmpty ← declModifiersDocStatus head then
+        lintDocStatusField (leadingEmpty || modsEmpty) rest[1][0] stx[3] "public constructor"
     unless rest[5].isNone do
       for stx in rest[5][0][1].getArgs do
         let head := stx[0]
-        if (← declModifiersPubNoDoc head) then -- no doc string
-          lintField rest[1][0] stx[1] "computed field"
+        if let some isEmpty ← declModifiersDocStatus head then
+          lintDocStatusField isEmpty rest[1][0] stx[1] "computed field"
   else if rest.getKind == ``«structure» then
     unless rest[4][2].isNone do
       let redecls : Std.HashSet String.Pos.Raw :=
@@ -173,45 +225,52 @@ def checkDecl : SimpleHandler := fun stx => do
               else s
             else s
       let parent := rest[1][0]
-      let lint1 stx := do
+      let lint1 isEmpty stx := do
         if let some range := stx.getRange? then
           if redecls.contains range.start then return
-        lintField parent stx "public field"
+        lintDocStatusField isEmpty parent stx "public field"
       for stx in rest[4][2][0].getArgs do
         let head := stx[0]
-        if (← declModifiersPubNoDoc head) then
+        if let some isEmpty ← declModifiersDocStatus head then
           if stx.getKind == ``structSimpleBinder then
-            lint1 stx[1]
+            lint1 isEmpty stx[1]
           else
             for stx in stx[2].getArgs do
-              lint1 stx
+              lint1 isEmpty stx
 
 @[builtin_missing_docs_handler «initialize»]
 def checkInit : SimpleHandler := fun stx => do
-  if !stx[2].isNone && (← declModifiersPubNoDoc stx[0]) then
-    lintNamed stx[2][0] "initializer"
+  if !stx[2].isNone then
+    if let some isEmpty ← declModifiersDocStatus stx[0] then
+      lintDocStatusNamed isEmpty stx[2][0] "initializer"
 
 @[builtin_missing_docs_handler «notation»]
 def checkNotation : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] then
-    if stx[5].isNone then lint stx[3] "notation"
-    else lintNamed stx[5][0][3] "notation"
+  if stx[2][0][0].getKind != ``«local» then
+    if let some isEmpty ← docOptStatus stx[0] stx[1] then
+      if stx[5].isNone then lintDocStatus isEmpty stx[3] "notation"
+      else lintDocStatusNamed isEmpty stx[5][0][3] "notation"
 
 @[builtin_missing_docs_handler «mixfix»]
 def checkMixfix : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] then
-    if stx[5].isNone then lint stx[3] stx[3][0].getAtomVal
-    else lintNamed stx[5][0][3] stx[3][0].getAtomVal
+  if stx[2][0][0].getKind != ``«local» then
+    if let some isEmpty ← docOptStatus stx[0] stx[1] then
+      if stx[5].isNone then lintDocStatus isEmpty stx[3] stx[3][0].getAtomVal
+      else lintDocStatusNamed isEmpty stx[5][0][3] stx[3][0].getAtomVal
 
 @[builtin_missing_docs_handler «syntax»]
 def checkSyntax : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] && !hasTacticAlt stx[1] then
-    if stx[5].isNone then lint stx[3] "syntax"
-    else lintNamed stx[5][0][3] "syntax"
+  if stx[2][0][0].getKind != ``«local» then
+    if let some isEmpty ← docOptStatus stx[0] stx[1] (checkTacticAlt := true) then
+      if stx[5].isNone then lintDocStatus isEmpty stx[3] "syntax"
+      else lintDocStatusNamed isEmpty stx[5][0][3] "syntax"
 
 def mkSimpleHandler (name : String) (declNameStxIdx := 2) : SimpleHandler := fun stx => do
-  if stx[0].isNone then
-    lintNamed stx[declNameStxIdx] name
+  if (← isMissingDoc stx[0]) then
+    if (← isEmptyDocString stx[0]) then
+      lintEmptyNamed stx[declNameStxIdx] name
+    else
+      lintNamed stx[declNameStxIdx] name
 
 @[builtin_missing_docs_handler syntaxAbbrev]
 def checkSyntaxAbbrev : SimpleHandler := mkSimpleHandler "syntax"
@@ -221,20 +280,22 @@ def checkSyntaxCat : SimpleHandler := mkSimpleHandler "syntax category"
 
 @[builtin_missing_docs_handler «macro»]
 def checkMacro : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] && !hasTacticAlt stx[1] then
-    if stx[5].isNone then lint stx[3] "macro"
-    else lintNamed stx[5][0][3] "macro"
+  if stx[2][0][0].getKind != ``«local» then
+    if let some isEmpty ← docOptStatus stx[0] stx[1] (checkTacticAlt := true) then
+      if stx[5].isNone then lintDocStatus isEmpty stx[3] "macro"
+      else lintDocStatusNamed isEmpty stx[5][0][3] "macro"
 
 @[builtin_missing_docs_handler «elab»]
 def checkElab : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] && !hasTacticAlt stx[1] then
-    if stx[5].isNone then lint stx[3] "elab"
-    else lintNamed stx[5][0][3] "elab"
+  if stx[2][0][0].getKind != ``«local» then
+    if let some isEmpty ← docOptStatus stx[0] stx[1] (checkTacticAlt := true) then
+      if stx[5].isNone then lintDocStatus isEmpty stx[3] "elab"
+      else lintDocStatusNamed isEmpty stx[5][0][3] "elab"
 
 @[builtin_missing_docs_handler classAbbrev]
 def checkClassAbbrev : SimpleHandler := fun stx => do
-  if (← declModifiersPubNoDoc stx[0]) then
-    lintNamed stx[3] "class abbrev"
+  if let some isEmpty ← declModifiersDocStatus stx[0] then
+    lintDocStatusNamed isEmpty stx[3] "class abbrev"
 
 @[builtin_missing_docs_handler Parser.Tactic.declareSimpLikeTactic]
 def checkSimpLike : SimpleHandler := mkSimpleHandler "simp-like tactic"
@@ -244,8 +305,8 @@ def checkRegisterBuiltinOption : SimpleHandler := mkSimpleHandler (declNameStxId
 
 @[builtin_missing_docs_handler Option.registerOption]
 def checkRegisterOption : SimpleHandler := fun stx => do
-  if (← declModifiersPubNoDoc stx[0]) then
-    lintNamed stx[2] "option"
+  if let some isEmpty ← declModifiersDocStatus stx[0] then
+    lintDocStatusNamed isEmpty stx[2] "option"
 
 @[builtin_missing_docs_handler registerSimpAttr]
 def checkRegisterSimpAttr : SimpleHandler := mkSimpleHandler "simp attr"
@@ -253,7 +314,7 @@ def checkRegisterSimpAttr : SimpleHandler := mkSimpleHandler "simp attr"
 @[builtin_missing_docs_handler «in»]
 def handleIn : Handler := fun _ stx => do
   if stx[0].getKind == ``«set_option» then
-    let opts ← Elab.elabSetOption stx[0][1] stx[0][3]
+    let (opts, _) ← Elab.elabSetOption stx[0][1] stx[0][3]
     withScope (fun scope => { scope with opts }) do
       missingDocs.run stx[2]
   else

src/Lean/Message.lean

@@ -244,7 +244,7 @@ def ofLevel (l : Level) : MessageData :=
   .ofLazy
     (fun ctx? => do
       let msg ← ofFormat <$> match ctx? with
-        | .none => pure (format l)
+        | .none => pure (l.format true (fun _ => none))
         | .some ctx => ppLevel ctx l
       return Dynamic.mk msg)
     (fun _ => false)

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/AbstractNestedProofs.lean

@@ -70,6 +70,7 @@ structure Context where
 abbrev M := ReaderT Context $ MonadCacheT ExprStructEq Expr MetaM
 
 partial def visit (e : Expr) : M Expr := do
+  checkSystem "abstract nested proofs"
   if e.isAtomic then
     pure e
   else

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/Eqns.lean

@@ -19,6 +19,7 @@ namespace Lean.Meta
 register_builtin_option backward.eqns.nonrecursive : Bool := {
     defValue := true
     descr    := "Create fine-grained equational lemmas even for non-recursive definitions."
+    deprecation? := some { since := "2026-03-30" }
   }
 
 register_builtin_option backward.eqns.deepRecursiveSplit : Bool := {
@@ -28,6 +29,7 @@ register_builtin_option backward.eqns.deepRecursiveSplit : Bool := {
                 that do not contain recursive calls do not cause further splits in the \
                 equational lemmas. This was the behavior before Lean 4.12, and the purpose of \
                 this option is to help migrating old code."
+    deprecation? := some { since := "2026-03-30" }
   }
 
 

src/Lean/Meta/HasAssignableMVar.lean

@@ -0,0 +1,54 @@
+/-
+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 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/InferType.lean

@@ -180,12 +180,14 @@ private def inferFVarType (fvarId : FVarId) : MetaM Expr := do
 
 @[inline] private def checkInferTypeCache (e : Expr) (inferType : MetaM Expr) : MetaM Expr := do
   if !(← read).cacheInferType || e.hasMVar then
+    Core.checkInterrupted
     inferType
   else
     let key ← mkExprConfigCacheKey e
     match (← get).cache.inferType.find? key with
     | some type => return type
     | none =>
+      Core.checkInterrupted
       let type ← inferType
       unless type.hasMVar do
         modifyInferTypeCache fun c => c.insert key type

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/Match/Match.lean

@@ -78,6 +78,14 @@ register_builtin_option backward.match.rowMajor : Bool := {
     it splits them from left to right, which can lead to unnecessary code bloat."
 }
 
+register_builtin_option match.maxCounterExamples : Nat := {
+  defValue := 5
+  descr := "Maximum number of missing-case counter-examples to generate. \
+    When this limit is reached, the match compiler stops exploring further \
+    case splits for counter-example generation. Increase if you need to see \
+    all missing cases."
+}
+
 private def mkIncorrectNumberOfPatternsMsg [ToMessageData α]
     (discrepancyKind : String) (expected actual : Nat) (pats : List α) :=
   let patternsMsg := MessageData.joinSep (pats.map toMessageData) ", "
@@ -269,10 +277,16 @@ def isCurrVarInductive (p : Problem) : MetaM Bool := do
     let val? ← getInductiveVal? x
     return val?.isSome
 
-private def isConstructorTransition (p : Problem) : MetaM Bool := do
-  return (← isCurrVarInductive p)
-    && (hasCtorPattern p || p.alts.isEmpty)
-    && p.alts.all fun alt => match alt.patterns with
+private def isConstructorTransition (p : Problem) : StateRefT State MetaM Bool := do
+  if !(← isCurrVarInductive p) then return false
+  if p.alts.isEmpty then
+    /- When there are no alternatives left and we have already accumulated enough
+       counter-examples, stop exploring further case splits. This prevents
+       combinatorial explosion when generating "missing cases" diagnostics. -/
+    let maxCEx := match.maxCounterExamples.get (← getOptions)
+    return (← get).counterExamples.length < maxCEx
+  else
+    return hasCtorPattern p && p.alts.all fun alt => match alt.patterns with
       | .ctor .. :: _        => true
       | .inaccessible _ :: _ => true -- should be a done pattern by now
       | _                    => false

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/Main.lean

@@ -714,7 +714,6 @@ where
 set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_simp]
 def simpImpl (e : Expr) : SimpM Result := withIncRecDepth do
-  checkSystem "simp"
   if (← isProof e) then
     return { expr := e }
   trace[Meta.Tactic.simp.heads] "{repr e.toHeadIndex}"

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
 /--
@@ -218,6 +219,7 @@ where
     else
       let candidates := candidates.insertionSort fun e₁ e₂ => e₁.1.priority > e₂.1.priority
       for (thm, numExtraArgs) in candidates do
+        checkSystem "simp"
         if inErasedSet thm then continue
         if rflOnly then
           unless thm.rfl do
@@ -245,6 +247,7 @@ where
     else
       let candidates := candidates.insertionSort fun e₁ e₂ => e₁.priority > e₂.priority
       for thm in candidates do
+        checkSystem "simp"
         unless inErasedSet thm || (rflOnly && !thm.rfl) do
           let result? ← withNewMCtxDepth do
             let val  ← thm.getValue

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

@@ -722,6 +722,7 @@ def simpAppUsingCongr (e : Expr) : SimpM Result := do
     if i == 0 then
       simp f
     else
+      checkSystem "simp"
       let i := i - 1
       let .app f a := e | unreachable!
       let fr ← visit f i

src/Lean/Meta/Transform.lean

@@ -50,6 +50,7 @@ partial def transform {m} [Monad m] [MonadLiftT CoreM m] [MonadControlT CoreM m]
   let _ : MonadLiftT (ST IO.RealWorld) m := { monadLift := fun x => liftM (m := CoreM) (liftM (m := ST IO.RealWorld) x) }
   let rec visit (e : Expr) : MonadCacheT ExprStructEq Expr m Expr :=
     checkCache { val := e : ExprStructEq } fun _ => Core.withIncRecDepth do
+      Core.checkSystem "transform"
       let rec visitPost (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do
         match (← post e) with
         | .done e      => pure e
@@ -107,6 +108,7 @@ partial def transformWithCache {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT
   let _ : MonadLiftT (ST IO.RealWorld) m := { monadLift := fun x => liftM (m := MetaM) (liftM (m := ST IO.RealWorld) x) }
   let rec visit (e : Expr) : MonadCacheT ExprStructEq Expr m Expr :=
     checkCache { val := e : ExprStructEq } fun _ => Meta.withIncRecDepth do
+      (Core.checkSystem "transform" : MetaM Unit)
       let rec visitPost (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do
         match (← post e) with
         | .done e      => pure e

src/Lean/Meta/WHNF.lean

@@ -650,7 +650,7 @@ expand let-expressions, expand assigned meta-variables, unfold aux declarations.
 partial def whnfCore (e : Expr) : MetaM Expr :=
   go e
 where
-  go (e : Expr) : MetaM Expr :=
+  go (e : Expr) : MetaM Expr := do
     whnfEasyCases e fun e => do
       trace[Meta.whnf] e
       match e with

src/Lean/MetavarContext.lean

@@ -247,6 +247,18 @@ very simple unification and/or non-nested TC. So, if the "app builder" becomes a
 we may solve the issue by implementing `isDefEqCheap` that never invokes TC and uses tmp metavars.
 -/
 
+structure LevelMetavarDecl where
+  /-- The nesting depth of this metavariable. We do not want
+  unification subproblems to influence the results of parent
+  problems. The depth keeps track of this information and ensures
+  that unification subproblems cannot leak information out, by unifying
+  based on depth. -/
+  depth : Nat
+  /-- This field tracks how old a metavariable is. It is set using a counter at `MetavarContext`.
+  We primarily use the index of a level metavariable for pretty printing. -/
+  index : Nat
+  deriving Inhabited
+
 /--
 `LocalInstance` represents a local typeclass instance registered by and for
 the elaborator. It stores the name of the typeclass in `className`, and the
@@ -309,7 +321,8 @@ structure MetavarDecl where
   kind           : MetavarKind
   /-- See comment at `CheckAssignment` `Meta/ExprDefEq.lean` -/
   numScopeArgs   : Nat := 0
-  /-- We use this field to track how old a metavariable is. It is set using a counter at `MetavarContext` -/
+  /-- We use this field to track how old a metavariable is. It is set using a counter at `MetavarContext`.
+  We also use it for pretty printing anonymous metavariables. -/
   index          : Nat
   deriving Inhabited
 
@@ -340,9 +353,12 @@ structure MetavarContext where
   depth          : Nat := 0
   /-- At what depth level mvars can be assigned. -/
   levelAssignDepth : Nat := 0
+  /-- Counter for setting the field `index` at `LevelMetavarDecl`. -/
+  lmvarCounter   : Nat := 0
   /-- Counter for setting the field `index` at `MetavarDecl` -/
   mvarCounter    : Nat := 0
-  lDepth         : PersistentHashMap LMVarId Nat := {}
+  /-- Level metavariable declarations. -/
+  lDecls         : PersistentHashMap LMVarId LevelMetavarDecl := {}
   /-- Metavariable declarations. -/
   decls          : PersistentHashMap MVarId MetavarDecl := {}
   /-- Index mapping user-friendly names to ids. -/
@@ -444,11 +460,21 @@ def _root_.Lean.MVarId.isAssignedOrDelayedAssigned [Monad m] [MonadMCtx m] (mvar
   let mctx ← getMCtx
   return mctx.eAssignment.contains mvarId || mctx.dAssignment.contains mvarId
 
+def MetavarContext.findLevelDecl? (mctx : MetavarContext) (mvarId : LMVarId) : Option LevelMetavarDecl :=
+  mctx.lDecls.find? mvarId
+
+def MetavarContext.getLevelDecl (mctx : MetavarContext) (mvarId : LMVarId) : LevelMetavarDecl :=
+  match mctx.lDecls.find? mvarId with
+  | some decl => decl
+  | none      => panic! s!"unknown universe metavariable {mvarId.name}"
+
 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}"
+  let decl := mctx.getLevelDecl mvarId
+  return decl.depth >= mctx.levelAssignDepth
+
+def MetavarContext.findDecl? (mctx : MetavarContext) (mvarId : MVarId) : Option MetavarDecl :=
+  mctx.decls.find? mvarId
 
 def MetavarContext.getDecl (mctx : MetavarContext) (mvarId : MVarId) : MetavarDecl :=
   match mctx.decls.find? mvarId with
@@ -484,30 +510,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
@@ -826,10 +828,11 @@ def addExprMVarDeclExp (mctx : MetavarContext) (mvarId : MVarId) (userName : Nam
    It is used to implement actions in the monads `MetaM`, `ElabM` and `TacticM`.
    It should not be used directly since the argument `(mvarId : MVarId)` is assumed to be "unique". -/
 def addLevelMVarDecl (mctx : MetavarContext) (mvarId : LMVarId) : MetavarContext :=
-  { mctx with lDepth := mctx.lDepth.insert mvarId mctx.depth }
-
-def findDecl? (mctx : MetavarContext) (mvarId : MVarId) : Option MetavarDecl :=
-  mctx.decls.find? mvarId
+  { mctx with
+    lmvarCounter := mctx.lmvarCounter + 1
+    lDecls := mctx.lDecls.insert mvarId {
+      depth := mctx.depth
+      index := mctx.lmvarCounter } }
 
 def findUserName? (mctx : MetavarContext) (userName : Name) : Option MVarId :=
   mctx.userNames.find? userName
@@ -909,12 +912,13 @@ def setFVarBinderInfo (mctx : MetavarContext) (mvarId : MVarId)
   mctx.modifyExprMVarLCtx mvarId (·.setBinderInfo fvarId bi)
 
 def findLevelDepth? (mctx : MetavarContext) (mvarId : LMVarId) : Option Nat :=
-  mctx.lDepth.find? mvarId
+  (mctx.findLevelDecl? mvarId).map LevelMetavarDecl.depth
 
 def getLevelDepth (mctx : MetavarContext) (mvarId : LMVarId) : Nat :=
-  match mctx.findLevelDepth? mvarId with
-  | some d => d
-  | none   => panic! "unknown metavariable"
+  (mctx.getLevelDecl mvarId).depth
+
+def findLevelIndex? (mctx : MetavarContext) (mvarId : LMVarId) : Option Nat :=
+  (mctx.findLevelDecl? mvarId).map LevelMetavarDecl.index
 
 def isAnonymousMVar (mctx : MetavarContext) (mvarId : MVarId) : Bool :=
   match mctx.findDecl? mvarId with

src/Lean/Parser/Command.lean

@@ -622,6 +622,15 @@ declaration signatures.
 /-- Debugging command: Prints the result of `Environment.dumpAsyncEnvState`. -/
 @[builtin_command_parser] def dumpAsyncEnvState := leading_parser
   "#dump_async_env_state"
+/--
+Mark a syntax kind as deprecated. When this syntax is elaborated, a warning will be emitted.
+
+```
+deprecated_syntax Lean.Parser.Term.let_fun "use `have` instead" (since := "2026-03-18")
+```
+-/
+@[builtin_command_parser] def deprecatedSyntax := leading_parser
+  "deprecated_syntax " >> ident >> optional (ppSpace >> strLit) >> optional (" (" >> nonReservedSymbol "since" >> " := " >> strLit >> ")")
 @[builtin_command_parser] def «init_quot»    := leading_parser
   "init_quot"
 /--
@@ -629,6 +638,27 @@ An internal bootstrapping command that reinterprets a Markdown docstring as Vers
 -/
 @[builtin_command_parser] def «docs_to_verso»    := leading_parser
   "docs_to_verso " >> sepBy1 ident ", "
+/--
+`deprecated_module` marks the current module as deprecated.
+When another module imports a deprecated module, a warning is emitted during elaboration.
+
+```
+deprecated_module "use NewModule instead" (since := "2026-03-19")
+```
+
+The warning message is optional but recommended.
+The warning can be disabled with `set_option linter.deprecated.module false` or
+`-Dlinter.deprecated.module=false`.
+-/
+@[builtin_command_parser] def «deprecated_module» := leading_parser
+  "deprecated_module" >> optional (ppSpace >> strLit) >> optional (" (" >> nonReservedSymbol "since" >> " := " >> strLit >> ")")
+
+/--
+`#show_deprecated_modules` displays all modules in the current environment that have been
+marked with `deprecated_module`.
+-/
+@[builtin_command_parser] def showDeprecatedModules := leading_parser
+  "#show_deprecated_modules"
 
 def optionValue := nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit
 /--
@@ -648,6 +678,12 @@ only in a single term or tactic.
 -/
 @[builtin_command_parser] def «set_option»   := leading_parser
   "set_option " >> identWithPartialTrailingDot >> ppSpace >> optionValue
+/--
+`unlock_limits` disables all built-in resource limit options (currently `maxRecDepth`,
+`maxHeartbeats`, and `synthInstance.maxHeartbeats`) in the current scope by setting them to 0.
+-/
+@[builtin_command_parser] def «unlock_limits» := leading_parser
+  "unlock_limits"
 def eraseAttr := leading_parser
   "-" >> rawIdent
 @[builtin_command_parser] def «attribute»    := leading_parser

src/Lean/Parser/Do.lean

@@ -67,9 +67,9 @@ def notFollowedByRedefinedTermToken :=
     "token at 'do' element"
 
 @[builtin_doElem_parser] def doLet      := leading_parser
-  "let " >> optional "mut " >> letDecl
+  "let " >> optional "mut " >> letConfig >> letDecl
 @[builtin_doElem_parser] def doLetElse  := leading_parser withPosition <|
-  "let " >> optional "mut " >> termParser >> " := " >> termParser >>
+  "let " >> optional "mut " >> letConfig >> termParser >> " := " >> termParser >>
   (checkColGe >> " | " >> doSeqIndent) >> optional (checkColGe >> doSeqIndent)
 
 @[builtin_doElem_parser] def doLetExpr  := leading_parser withPosition <|
@@ -89,7 +89,7 @@ def doPatDecl  := leading_parser
   atomic (termParser >> optType >> ppSpace >> leftArrow) >>
   doElemParser >> optional ((checkColGe >> " | " >> doSeqIndent) >> optional (checkColGe >> doSeqIndent))
 @[builtin_doElem_parser] def doLetArrow      := leading_parser withPosition <|
-  "let " >> optional "mut " >> (doIdDecl <|> doPatDecl)
+  "let " >> optional "mut " >> letConfig >> (doIdDecl <|> doPatDecl)
 
 /-
 We use `letIdDeclNoBinders` to define `doReassign`.
@@ -114,7 +114,7 @@ def letIdDeclNoBinders := leading_parser
 @[builtin_doElem_parser] def doReassignArrow := leading_parser
   notFollowedByRedefinedTermToken >> (doIdDecl <|> doPatDecl)
 @[builtin_doElem_parser] def doHave     := leading_parser
-  "have" >> Term.letDecl
+  "have" >> Term.letConfig >> Term.letDecl
 /-
 In `do` blocks, we support `if` without an `else`.
 Thus, we use indentation to prevent examples such as

src/Lean/Parser/Term.lean

@@ -882,13 +882,19 @@ the available context).
 -/
 def identProjKind := `Lean.Parser.Term.identProj
 
+@[builtin_term_parser] def dotIdent := leading_parser
+  "." >> checkNoWsBefore >> rawIdent
+
 def isIdent (stx : Syntax) : Bool :=
   -- antiquotations should also be allowed where an identifier is expected
   stx.isAntiquot || stx.isIdent
 
+def isIdentOrDotIdent (stx : Syntax) : Bool :=
+  isIdent stx || stx.isOfKind ``dotIdent
+
 /-- `x.{u, ...}` explicitly specifies the universes `u, ...` of the constant `x`. -/
 @[builtin_term_parser] def explicitUniv : TrailingParser := trailing_parser
-  checkStackTop isIdent "expected preceding identifier" >>
+  checkStackTop isIdentOrDotIdent "expected preceding identifier" >>
   checkNoWsBefore "no space before '.{'" >> ".{" >>
   sepBy1 levelParser ", " >> "}"
 /-- `x@e` or `x@h:e` matches the pattern `e` and binds its value to the identifier `x`.
@@ -976,9 +982,6 @@ appropriate parameter for the underlying monad's `ST` effects, then passes it to
 @[builtin_term_parser] def dynamicQuot := withoutPosition <| leading_parser
   "`(" >> ident >> "| " >> incQuotDepth (parserOfStack 1) >> ")"
 
-@[builtin_term_parser] def dotIdent := leading_parser
-  "." >> checkNoWsBefore >> rawIdent
-
 /--
 Implementation of the `show_term` term elaborator.
 -/

src/Lean/Parser/Types.lean

@@ -469,6 +469,7 @@ def seq : FirstTokens → FirstTokens → FirstTokens
   | epsilon,      tks          => tks
   | optTokens s₁, optTokens s₂ => optTokens (s₁ ++ s₂)
   | optTokens s₁, tokens s₂    => tokens (s₁ ++ s₂)
+  | optTokens _,  unknown      => unknown
   | tks,          _            => tks
 
 def toOptional : FirstTokens → FirstTokens

src/Lean/PrettyPrinter.lean

@@ -70,6 +70,9 @@ def ppExprLegacy (env : Environment) (mctx : MetavarContext) (lctx : LocalContex
     { fileName := "<PrettyPrinter>", fileMap := default }
     { env := env }
 
+def ppLevel (l : Level) : MetaM Format := do
+  ppCategory `level (← delabLevel l (prec := 0))
+
 def ppTactic (stx : TSyntax `tactic) : CoreM Format := ppCategory `tactic stx
 
 def ppCommand (stx : Syntax.Command) : CoreM Format := ppCategory `command stx
@@ -110,7 +113,7 @@ builtin_initialize
     ppExprWithInfos := fun ctx e => ctx.runMetaM <| withoutContext <| ppExprWithInfos e
     ppConstNameWithInfos := fun ctx n => ctx.runMetaM <| withoutContext <| ppConstNameWithInfos n
     ppTerm := fun ctx stx => ctx.runCoreM <| withoutContext <| ppTerm stx
-    ppLevel := fun ctx l => return l.format (mvars := getPPMVarsLevels ctx.opts)
+    ppLevel := fun ctx l => ctx.runMetaM <| withoutContext <| ppLevel l
     ppGoal := fun ctx mvarId => ctx.runMetaM <| withoutContext <| Meta.ppGoal mvarId
   }
 

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -450,6 +450,10 @@ partial def delab : Delab := do
   else
     return stx
 
+def delabLevel (l : Level) (prec : Nat) : DelabM Syntax.Level := do
+  let mvars ← getPPOption getPPMVarsLevels
+  return Level.quote l prec (mvars := mvars) (lIndex? := (← getMCtx).findLevelIndex?)
+
 /--
 Registers an unexpander for applications of a given constant.
 
@@ -477,7 +481,11 @@ unsafe builtin_initialize appUnexpanderAttribute : KeyedDeclsAttribute Unexpande
 end Delaborator
 
 open SubExpr (Pos PosMap)
-open Delaborator (OptionsPerPos topDownAnalyze DelabM)
+open Delaborator (OptionsPerPos topDownAnalyze DelabM getPPOption)
+
+def delabLevel (l : Level) (prec : Nat) : MetaM Syntax.Level := do
+  let mvars := getPPMVarsLevels (← getOptions)
+  return Level.quote l prec (mvars := mvars) (lIndex? := (← getMCtx).findLevelIndex?)
 
 def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab : DelabM α) :
     MetaM (α × PosMap Elab.Info) := do

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -91,10 +91,9 @@ def delabSort : Delab := do
   | Level.zero => `(Prop)
   | Level.succ .zero => `(Type)
   | _ =>
-    let mvars ← getPPOption getPPMVarsLevels
     match l.dec with
-    | some l' => `(Type $(Level.quote l' (prec := max_prec) (mvars := mvars)))
-    | none    => `(Sort $(Level.quote l (prec := max_prec) (mvars := mvars)))
+    | some l' => `(Type $(← delabLevel l' (prec := max_prec)))
+    | none    => `(Sort $(← delabLevel l (prec := max_prec)))
 
 /--
 Delaborator for `const` expressions.
@@ -131,8 +130,8 @@ def delabConst : Delab := do
 
   let stx ←
     if !ls.isEmpty && (← getPPOption getPPUniverses) then
-      let mvars ← getPPOption getPPMVarsLevels
-      `($(mkIdent c).{$[$(ls.toArray.map (Level.quote · (prec := 0) (mvars := mvars)))],*})
+      let ls' ← ls.toArray.mapM fun l => delabLevel l (prec := 0)
+      `($(mkIdent c).{$ls',*})
     else
       pure <| mkIdent c
 
@@ -620,8 +619,9 @@ private partial def collectStructFields
             if s'.induct == parentName then
               let (fieldValues, fields) ← collectStructFields structName levels params fields fieldValues s'
               return (i + 1, fieldValues, fields)
-      /- Does this field have a default value? and if so, can we omit the field? -/
-      unless ← getPPOption getPPStructureInstancesDefaults do
+      /- Does this field have a default value? and if so, can we omit the field?
+      We cannot omit fields for patterns, since default values do not apply for them. -/
+      unless ← pure (← read).inPattern <||> getPPOption getPPStructureInstancesDefaults do
         if let some defFn := getEffectiveDefaultFnForField? (← getEnv) structName fieldName then
           -- Use `withNewMCtxDepth` to prevent delaborator from solving metavariables.
           if let some (_, defValue) ← withNewMCtxDepth <| instantiateStructDefaultValueFn? defFn levels params (pure ∘ fieldValues.get?) then

src/Lean/Server/Test/Runner.lean

@@ -641,13 +641,13 @@ def processGenericRequest : RunnerM Unit := do
   let params := params.setObjVal! "position" (toJson s.pos)
   logResponse s.method params
 
-def processDirective (ws directive : String) (directiveTargetLineNo : Nat) : RunnerM Unit := do
+def processDirective (_ws directive : String) (directiveTargetLineNo : Nat)
+    (directiveTargetColumn : Nat) : RunnerM Unit := do
   let directive := directive.drop 1
   let colon := directive.find ':'
   let method := directive.sliceTo colon |>.trimAscii |>.copy
   -- TODO: correctly compute in presence of Unicode
-  let directiveTargetColumn := ws.rawEndPos + "--"
-  let pos : Lsp.Position := { line := directiveTargetLineNo, character := directiveTargetColumn.byteIdx }
+  let pos : Lsp.Position := { line := directiveTargetLineNo, character := directiveTargetColumn }
   let params :=
     if h : ¬colon.IsAtEnd then
       directive.sliceFrom (colon.next h) |>.trimAscii.copy
@@ -686,10 +686,15 @@ def processLine (line : String) : RunnerM Unit := do
     match directive.front with
     | 'v' => pure <| (← get).lineNo + 1  -- TODO: support subsequent 'v'... or not
     | '^' => pure <| (← get).lastActualLineNo
+    -- `⬑` is like `^` but targets the column of the `--` marker itself (i.e. column 0 when the
+    -- marker is at the start of the line), rather than the column after `--`.
+    | '⬑' => pure <| (← get).lastActualLineNo
     | _ =>
       skipLineWithoutDirective
       return
-  processDirective ws directive directiveTargetLineNo
+  let directiveTargetColumn :=
+    if directive.front == '⬑' then ws.rawEndPos.byteIdx else (ws.rawEndPos + "--").byteIdx
+  processDirective ws directive directiveTargetLineNo (directiveTargetColumn := directiveTargetColumn)
   skipLineWithDirective
 
 

src/Lean/Shell.lean

@@ -12,6 +12,7 @@ import Lean.Server.Watchdog
 import Lean.Server.FileWorker
 import Lean.Compiler.LCNF.EmitC
 import Init.System.Platform
+import Lean.Compiler.Options
 
 /-  Lean companion to  `shell.cpp` -/
 
@@ -340,7 +341,10 @@ def ShellOptions.process (opts : ShellOptions)
   | 'I' => -- `-I, --stdin`
     return {opts with useStdin := true}
   | 'r' => -- `--run`
-    return {opts with run := true}
+    return {opts with
+      run := true
+      -- can't get IR if it's postponed
+      leanOpts := Compiler.compiler.postponeCompile.set opts.leanOpts false }
   | 'o' => -- `--o, olean=fname`
     return {opts with oleanFileName? := ← checkOptArg "o" optArg?}
   | 'i' => -- `--i, ilean=fname`

src/Lean/Util/PPExt.lean

@@ -52,7 +52,7 @@ structure PPFns where
   ppExprWithInfos : PPContext → Expr → IO FormatWithInfos
   ppConstNameWithInfos : PPContext → Name → IO FormatWithInfos
   ppTerm : PPContext → Term → IO Format
-  ppLevel : PPContext → Level → BaseIO Format
+  ppLevel : PPContext → Level → IO Format
   ppGoal : PPContext → MVarId → IO Format
   deriving Inhabited
 
@@ -67,7 +67,7 @@ builtin_initialize ppFnsRef : IO.Ref PPFns ←
     ppExprWithInfos := fun _ e => return format (toString e)
     ppConstNameWithInfos := fun _ n => return format n
     ppTerm := fun ctx stx => return formatRawTerm ctx stx
-    ppLevel := fun _ l => return format l
+    ppLevel := fun ctx l => return l.format true ctx.mctx.findLevelIndex?
     ppGoal := fun _ mvarId => return formatRawGoal mvarId
   }
 
@@ -108,8 +108,14 @@ def ppTerm (ctx : PPContext) (stx : Term) : BaseIO Format := do
       else
         pure f!"failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)"
 
-def ppLevel (ctx : PPContext) (l : Level) : BaseIO Format :=
-  ppExt.getState ctx.env |>.ppLevel ctx l
+def ppLevel (ctx : PPContext) (l : Level) : BaseIO Format := do
+  match (← ppExt.getState ctx.env |>.ppLevel ctx l |>.toBaseIO) with
+  | .ok fmt => return fmt
+  | .error ex =>
+    if pp.rawOnError.get ctx.opts then
+      pure f!"[Error pretty printing level: {ex}. Falling back to raw printer.]{Format.line}{l.format true ctx.mctx.findLevelIndex?}"
+    else
+      pure f!"failed to pretty print level (use 'set_option pp.rawOnError true' for raw representation)"
 
 def ppGoal (ctx : PPContext) (mvarId : MVarId) : BaseIO Format := do
   match (← ppExt.getState ctx.env |>.ppGoal ctx mvarId |>.toBaseIO) with

src/Lean/Util/RecDepth.lean

@@ -14,7 +14,7 @@ namespace Lean
 
 register_builtin_option maxRecDepth : Nat := {
   defValue := defaultMaxRecDepth
-  descr    := "maximum recursion depth for many Lean procedures"
+  descr    := "maximum recursion depth for many Lean procedures, 0 means no limit"
 }
 
 end Lean

src/LeanIR.lean

@@ -57,15 +57,19 @@ def setConfigOption (opts : Options) (arg : String) : IO Options := do
 
 public def main (args : List String) : IO UInt32 := do
   let setupFile::irFile::c::optArgs := args | do
-    IO.println s!"usage: leanir <setup.json> <module> <output.ir> <output.c> <-Dopt=val>..."
+    IO.println s!"usage: leanir <setup.json> <output.ir> <output.c> [--stat] <-Dopt=val>..."
     return 1
 
   let setup ← ModuleSetup.load setupFile
   let modName := setup.name
 
+  let mut printStats := false
   let mut opts := setup.options.toOptions
   for optArg in optArgs do
-    opts ← setConfigOption opts optArg
+    if optArg == "--stat" then
+      printStats := true
+    else
+      opts ← setConfigOption opts optArg
   opts := Compiler.compiler.inLeanIR.set opts true
   opts := maxHeartbeats.set opts 0
 
@@ -127,12 +131,15 @@ public def main (args : List String) : IO UInt32 := do
     modifyEnv (postponedCompileDeclsExt.setState · (decls.foldl (fun s e => e.declNames.foldl (·.insert · e) s) {}))
     for decl in decls do
       for decl in decl.declNames do
-        resumeCompilation decl
+        try
+          resumeCompilation decl (← getOptions)
+        finally
+          addTraceAsMessages
+      for msg in (← Core.getAndEmptyMessageLog).unreported do
+        IO.eprintln (← msg.toString)
   catch e =>
     unless e.isInterrupt do
       logError e.toMessageData
-  finally
-    addTraceAsMessages
 
   let .ok (_, s) := res? | unreachable!
   let env := s.env
@@ -155,4 +162,6 @@ public def main (args : List String) : IO UInt32 := do
     out.write data.toUTF8
 
   displayCumulativeProfilingTimes
+  if printStats then
+    env.displayStats
   return 0

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/Do/SPred/DerivedLaws.lean

@@ -178,36 +178,6 @@ theorem entails_pure_elim_cons {σ : Type u} [Inhabited σ] (P Q : Prop) : entai
 @[simp] theorem entails_4 {P Q : SPred [σ₁, σ₂, σ₃, σ₄]} : SPred.entails P Q ↔ (∀ s₁ s₂ s₃ s₄, (P s₁ s₂ s₃ s₄).down → (Q s₁ s₂ s₃ s₄).down) := iff_of_eq rfl
 @[simp] theorem entails_5 {P Q : SPred [σ₁, σ₂, σ₃, σ₄, σ₅]} : SPred.entails P Q ↔ (∀ s₁ s₂ s₃ s₄ s₅, (P s₁ s₂ s₃ s₄ s₅).down → (Q s₁ s₂ s₃ s₄ s₅).down) := iff_of_eq rfl
 
-/-!
-# `SPred.evalsTo`
-
-Relates a stateful value `SVal σs α` to a pure value `a : α`, lifting equality through the state.
--/
-
-/-- Relates a stateful value to a pure value, lifting equality through the state layers. -/
-def evalsTo {α : Type u} {σs : List (Type u)} (f : SVal σs α) (a : α) : SPred σs :=
-  match σs with
-  | [] => ⌜a = f⌝
-  | _ :: _ => fun s => evalsTo (f s) a
-
-@[simp, grind =] theorem evalsTo_nil {f : SVal [] α} {a : α} :
-    evalsTo f a = ⌜a = f⌝ := rfl
-
-theorem evalsTo_cons {f : σ → SVal σs α} {a : α} {s : σ} :
-    evalsTo (σs := σ::σs) f a s = evalsTo (f s) a := rfl
-
-@[simp, grind =] theorem evalsTo_1 {f : SVal [σ] α} {a : α} {s : σ} :
-    evalsTo f a s = evalsTo (f s) a := rfl
-
-@[simp, grind =] theorem evalsTo_2 {f : SVal [σ₁, σ₂] α} {a : α} {s₁ : σ₁} {s₂ : σ₂} :
-    evalsTo f a s₁ s₂ = evalsTo (f s₁ s₂) a := rfl
-
-theorem evalsTo_total {P : SPred σs} (f : SVal σs α) :
-    P ⊢ₛ ∃ m, evalsTo f m := by
-  induction σs with
-  | nil => simp
-  | cons _ _ ih => intro s; apply ih
-
 /-! # Tactic support -/
 
 namespace Tactic
@@ -368,4 +338,3 @@ theorem Frame.frame {P Q T : SPred σs} {φ : Prop} [HasFrame P Q φ]
     · exact HasFrame.reassoc.mp.trans SPred.and_elim_r
     · intro hp
       exact HasFrame.reassoc.mp.trans (SPred.and_elim_l' (h hp))
-

src/Std/Do/SPred/Laws.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Std.Do.SPred.Notation
-import Init.PropLemmas
 
 @[expose] public section
 
@@ -158,17 +157,3 @@ theorem imp_curry {P Q : SVal.StateTuple σs → Prop} : (SVal.curry (fun t =>
   induction σs
   case nil => rfl
   case cons σ σs ih => intro s; simp only [imp_cons, SVal.curry_cons]; exact ih
-
-/-! # Prop-indexed quantifiers -/
-
-/-- Simplifies an existential over a true proposition. -/
-theorem exists_prop_of_true {p : Prop} (h : p) {P : p → SPred σs} : spred(∃ (h : p), P h) = P h := by
-  induction σs with
-  | nil => ext; exact _root_.exists_prop_of_true h
-  | cons σ σs ih => ext; exact ih
-
-/-- Simplifies a universal over a true proposition. -/
-theorem forall_prop_of_true {p : Prop} (h : p) {P : p → SPred σs} : spred(∀ (h : p), P h) = P h := by
-  induction σs with
-  | nil => ext; exact _root_.forall_prop_of_true h
-  | cons σ σs ih => ext; exact ih

src/Std/Do/Triple/RepeatSpec.lean

@@ -1,94 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Graf
--/
-module
-
-prelude
-public import Std.Do.Triple.SpecLemmas
-import Std.Tactic.Do.Syntax
-
-set_option linter.missingDocs true
-
-@[expose] public section
-
-namespace Std.Do
-
-/-!
-# Specification theorem for `Repeat` loops
-
-This file contains the `@[spec]` theorem for `forIn` over `Lean.Repeat`, which enables
-verified reasoning about `repeat`/`while` loops using `mvcgen`.
--/
-
-set_option mvcgen.warning false
-
-/-- A variant (termination measure) for a `Repeat`/`while` loop. -/
-@[spec_invariant_type]
-abbrev RepeatVariant (β : Type u) (ps : PostShape.{u}) := β → SVal ps.args (ULift Nat)
-
-set_option linter.missingDocs false in
-abbrev RepeatVariant.eval {β ps} (variant : RepeatVariant β ps) (b : β) (n : Nat) :=
-  SPred.evalsTo (variant b) ⟨n⟩
-
-/-- An invariant for a `Repeat`/`while` loop. -/
-@[spec_invariant_type]
-abbrev RepeatInvariant β ps := PostCond (Bool × β) ps
-
-section
-
-variable {β : Type u} {m : Type u → Type v} {ps : PostShape.{u}}
-
-private theorem RepeatVariant.eval_total {P : SPred ps.args} (variant : RepeatVariant β ps) (b : β) :
-    P ⊢ₛ ∃ m, RepeatVariant.eval variant b m := by
-  mintro _
-  mhave h2 := SPred.evalsTo_total (variant b)
-  mcases h2 with ⟨m, h2⟩
-  mexists m.down
-
-private theorem RepeatVariant.add_eval {P Q : SPred ps.args} (variant : RepeatVariant β ps) (b : β)
-    (h : spred(∃ m, RepeatVariant.eval variant b m ∧ P) ⊢ₛ Q) : P ⊢ₛ Q := by
-  apply SPred.entails.trans _ h
-  mintro _
-  mhave h2 := RepeatVariant.eval_total variant b
-  mcases h2 with ⟨m, h2⟩
-  mexists m
-  mconstructor <;> massumption
-
-end
-
-section
-
-variable {β : Type u} {m : Type u → Type v} {ps : PostShape.{u}}
-variable [Monad m] [Lean.Order.MonadTail m] [WPMonad m ps]
-
-@[spec]
-theorem Spec.forIn_repeat
-    {l : _root_.Lean.Repeat} {init : β} {f : Unit → β → m (ForInStep β)}
-    (measure : RepeatVariant β ps)
-    (inv : RepeatInvariant β ps)
-    (step : ∀ b mb,
-      Triple (f () b)
-        spred(RepeatVariant.eval measure b mb ∧ inv.1 (false, b))
-        (fun r => match r with
-          | .yield b' => spred(∃ mb', RepeatVariant.eval measure b' mb' ∧ ⌜mb' < mb⌝ ∧ inv.1 (false, b'))
-          | .done b' => inv.1 (true, b'), inv.2)) :
-    Triple (forIn l init f) spred(inv.1 (false, init)) (fun b => inv.1 (true, b), inv.2) := by
-  haveI : Nonempty β := ⟨init⟩
-  simp only [forIn]
-  apply RepeatVariant.add_eval measure init
-  apply SPred.exists_elim
-  intro minit
-  induction minit using Nat.strongRecOn generalizing init with
-  | _ minit ih =>
-  rw [_root_.Lean.Repeat.forIn.eq_1]
-  mvcgen [step, ih] with
-  | vc2 =>
-    mrename_i h
-    mcases h with ⟨mb', ⟨hmeasure, ⌜hmb'⌝, h⟩⟩
-    mspec Triple.of_entails_wp (ih mb' hmb')
-
-end
-
-end Std.Do

src/Std/Do/Triple/SpecLemmas.lean

@@ -10,7 +10,6 @@ public import Std.Do.Triple.Basic
 public import Init.Data.Range.Polymorphic.Iterators
 import Init.Data.Range.Polymorphic
 public import Init.Data.Slice.Array
-public import Init.Repeat
 
 -- This public import is a workaround for #10652.
 -- Without it, adding the `spec` attribute for `instMonadLiftTOfMonadLift` will fail.
@@ -2189,5 +2188,3 @@ theorem Spec.forIn_stringSlice
       next => apply Triple.pure; simp
       next b => simp [ih _ _ hsp.next]
   | endPos => simpa using Triple.pure _ (by simp)
-
-

src/Std/Internal/Async/Basic.lean

@@ -8,7 +8,6 @@ module
 prelude
 public import Init.System.Promise
 public import Init.While
-public import Init.Internal.Order.MonadTail
 
 public section
 
@@ -488,24 +487,6 @@ instance : Monad BaseAsync where
   pure := BaseAsync.pure
   bind := BaseAsync.bind
 
-set_option linter.unusedVariables false in
-/-- `BaseAsync.bind` is monotone in the continuation argument with respect to the CCPO on
-`BaseAsync`. This is an axiom because the `MaybeTask.ofTask` case of `BaseAsync.bind` uses
-`BaseIO.bindTask`, which is `@[extern] opaque` and cannot be unfolded. The property holds
-because `bind` only calls the continuation on values produced by `a`. -/
-axiom bind_mono_right' {α β : Type} [inst : Nonempty (MaybeTask β)]
-    (a : BaseIO (MaybeTask α)) (f₁ f₂ : α → BaseIO (MaybeTask β))
-    (h : ∀ x, @Lean.Order.PartialOrder.rel (BaseIO (MaybeTask β)) (Lean.Order.CCPO.toPartialOrder) (f₁ x) (f₂ x)) :
-    @Lean.Order.PartialOrder.rel (BaseIO (MaybeTask β)) (Lean.Order.CCPO.toPartialOrder)
-      (BaseAsync.bind a f₁) (BaseAsync.bind a f₂)
-
-set_option linter.unusedVariables false in
-instance : Lean.Order.MonadTail BaseAsync where
-  instCCPO _ := inferInstanceAs (Lean.Order.CCPO (BaseIO _))
-  bind_mono_right {α β a f₁ f₂} _ h :=
-    haveI : Nonempty (MaybeTask β) := ⟨.pure Classical.ofNonempty⟩
-    bind_mono_right' (β := β) a f₁ f₂ h
-
 instance : MonadLift BaseIO BaseAsync where
   monadLift := BaseAsync.lift
 
@@ -726,15 +707,6 @@ instance : Monad (EAsync ε) where
   pure := EAsync.pure
   bind := EAsync.bind
 
-instance : Lean.Order.MonadTail (EAsync ε) where
-  instCCPO _ := inferInstanceAs (Lean.Order.CCPO (BaseAsync _))
-  bind_mono_right {α β a f₁ f₂} _ h := by
-    haveI : Nonempty (MaybeTask (Except ε β)) := ⟨.pure Classical.ofNonempty⟩
-    exact BaseAsync.bind_mono_right' a _ _ fun x =>
-      match x with
-      | Except.error _ => Lean.Order.PartialOrder.rel_refl
-      | Except.ok a => h a
-
 instance : MonadLift (EIO ε) (EAsync ε) where
   monadLift := EAsync.lift