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/CLAUDE.md

@@ -7,6 +7,11 @@ To build Lean you should use `make -j$(nproc) -C build/release`.
 The build uses `ccache`, and in a sandbox `ccache` may complain about read-only file systems.
 Use `CCACHE_READONLY` and `CCACHE_TEMPDIR` instead of disabling ccache completely.
 
+To rebuild individual modules without a full build, use Lake directly:
+```
+cd src && lake build Init.Prelude
+```
+
 ## Running Tests
 
 See `tests/README.md` for full documentation. Quick reference:
@@ -56,6 +61,11 @@ make -C build/release/stage2 clean-stdlib
 ```
 must be run manually before building.
 
+To rebuild individual stage 2 modules without a full `make stage2`, use Lake directly:
+```
+cd build/release/stage2 && lake build Init.Prelude
+```
+
 ## New features
 
 When asked to implement new features:

.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)
@@ -614,6 +615,38 @@ else()
       OUTPUT_VARIABLE GIT_SHA1
       OUTPUT_STRIP_TRAILING_WHITESPACE
     )
+    # Fallback for jj workspaces where git cannot find .git directly.
+    # Use `jj git root` to find the backing git repo, then `jj log` to
+    # resolve the current workspace's commit (git HEAD points to the root
+    # workspace, not the current one).
+    if("${GIT_SHA1}" STREQUAL "")
+      find_program(JJ_EXECUTABLE jj)
+      if(JJ_EXECUTABLE)
+        execute_process(
+          COMMAND "${JJ_EXECUTABLE}" git root
+          WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
+          OUTPUT_VARIABLE _jj_git_dir
+          OUTPUT_STRIP_TRAILING_WHITESPACE
+          ERROR_QUIET
+          RESULT_VARIABLE _jj_git_root_result
+        )
+        execute_process(
+          COMMAND "${JJ_EXECUTABLE}" log -r @ --no-graph -T "commit_id"
+          WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
+          OUTPUT_VARIABLE _jj_commit
+          OUTPUT_STRIP_TRAILING_WHITESPACE
+          ERROR_QUIET
+          RESULT_VARIABLE _jj_rev_result
+        )
+        if(_jj_git_root_result EQUAL 0 AND _jj_rev_result EQUAL 0)
+          execute_process(
+            COMMAND git --git-dir "${_jj_git_dir}" ls-tree "${_jj_commit}" stage0 --object-only
+            OUTPUT_VARIABLE GIT_SHA1
+            OUTPUT_STRIP_TRAILING_WHITESPACE
+          )
+        endif()
+      endif()
+    endif()
     message(STATUS "stage0 sha1: ${GIT_SHA1}")
     # Now that we've prepared the information for the next stage, we can forget that we will use
     # Lake in the future as we won't use it in this stage
@@ -797,7 +830,14 @@ if(LLVM AND STAGE GREATER 0)
   set(EXTRA_LEANMAKE_OPTS "LLVM=1")
 endif()
 
-set(STDLIBS Init Std Lean Leanc LeanIR)
+set(
+  STDLIBS
+  Init
+  Std
+  Lean
+  Leanc
+  LeanIR
+)
 if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
   list(APPEND STDLIBS Lake LeanChecker)
 endif()
@@ -905,10 +945,7 @@ if(PREV_STAGE)
 endif()
 
 if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
-  add_custom_target(leanir ALL
-    DEPENDS leanshared
-    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanir
-    VERBATIM)
+  add_custom_target(leanir ALL DEPENDS leanshared COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanir VERBATIM)
 endif()
 
 # use Bash version for building, use Lean version in bin/ for tests & distribution

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/Fin/Lemmas.lean

@@ -527,6 +527,14 @@ theorem castLE_of_eq {m n : Nat} (h : m = n) {h' : m ≤ n} : castLE h' = Fin.ca
 
 @[simp, grind =] theorem val_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := rfl
 
+/-
+**Note**
+The current pattern inference heuristic includes the implicit term `n + m` as pattern of the pattern,
+but arithmetic is problematic in patterns because it is an interpreted symbol. For example,
+we will fail to match `@val n (castNat 0 i)`. Thus, we mark the implicit subterm with `no_index`
+-/
+grind_pattern val_castAdd => @val (no_index _) (castAdd m i)
+
 @[deprecated val_castAdd (since := "2025-11-21")]
 theorem coe_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := rfl
 
@@ -637,7 +645,15 @@ theorem exists_castSucc_eq {n : Nat} {i : Fin (n + 1)} : (∃ j, castSucc j = i)
 
 theorem succ_castSucc {n : Nat} (i : Fin n) : i.castSucc.succ = i.succ.castSucc := rfl
 
-@[simp, grind =] theorem val_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl
+@[simp] theorem val_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl
+
+/-
+**Note**
+The current pattern inference heuristic includes the implicit term `n + m` as pattern of the pattern,
+but arithmetic is problematic in patterns because it is an interpreted symbol. For example,
+we will fail to match `@val n (addNat i 0)`. Thus, we mark the implicit subterm with `no_index`
+-/
+grind_pattern val_addNat => @val (no_index _) (addNat i m)
 
 @[deprecated val_addNat (since := "2025-11-21")]
 theorem coe_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl

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/Grind/Util.lean

@@ -30,7 +30,13 @@ simpMatchDiscrsOnly (match 0 with | 0 => true | _ => false) = true
 ```
 using `eq_self`.
 -/
-def simpMatchDiscrsOnly {α : Sort u} (a : α) : α := a
+@[expose] def simpMatchDiscrsOnly {α : Sort u} (a : α) : α := a
+
+/--
+Gadget for protecting lambda abstractions created by `abstractGroundMismatches?`
+from beta reduction during preprocessing. See `ProveEq.lean` for details.
+-/
+@[expose] def abstractFn {α : Sort u} (a : α) : α := a
 
 /-- Gadget for representing offsets `t+k` in patterns. -/
 def offset (a b : Nat) : Nat := a + b

src/Init/Notation.lean

@@ -624,6 +624,23 @@ existing code. It may be removed in a future version of the library.
 syntax (name := deprecated) "deprecated" (ppSpace ident)? (ppSpace str)?
     (" (" &"since" " := " str ")")? : attr
 
+/--
+The attribute `@[deprecated_arg old new]` marks a named parameter as deprecated.
+
+When a caller uses the old name with a replacement available, a deprecation warning is emitted
+and the argument is silently forwarded to the new parameter. When no replacement is provided,
+the parameter is treated as removed and using it produces an error.
+
+* `@[deprecated_arg old new (since := "2026-03-18")]` marks `old` as a deprecated alias for `new`.
+* `@[deprecated_arg old new "use foo instead" (since := "2026-03-18")]` adds a custom message.
+* `@[deprecated_arg old (since := "2026-03-18")]` marks `old` as a removed parameter (no replacement).
+* `@[deprecated_arg old "no longer needed" (since := "2026-03-18")]` removed with a custom message.
+
+A warning is emitted if `(since := "...")` is omitted.
+-/
+syntax (name := deprecated_arg) "deprecated_arg" ppSpace ident (ppSpace ident)? (ppSpace str)?
+    (" (" &"since" " := " str ")")? : attr
+
 /--
 The attribute `@[suggest_for ..]` on a declaration suggests likely ways in which
 someone might **incorrectly** refer to a definition.

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

@@ -185,13 +185,9 @@ example : foo.default = (default, default) :=
 abbrev inferInstance {α : Sort u} [i : α] : α := i
 
 set_option checkBinderAnnotations false in
-/-- `inferInstanceAs α` synthesizes an instance of type `α`, transporting it from a
-definitionally equal type if necessary. This is useful when `α` is definitionally equal to
-some `α'` for which instances are registered, as it prevents leaking the definition's RHS
-at lower transparencies.
-
-`inferInstanceAs` requires an expected type from context. If you just need to synthesize an
-instance without transporting between types, use `inferInstance` instead.
+/--
+`inferInstanceAs α` synthesizes an instance of type `α` and then adjusts it to conform to the
+expected type `β`, which must be inferable from context.
 
 Example:
 ```
@@ -199,7 +195,26 @@ def D := Nat
 instance : Inhabited D := inferInstanceAs (Inhabited Nat)
 ```
 
-See `Lean.Meta.WrapInstance` for details.
+The adjustment will make sure that when the resulting instance will not "leak" the RHS `Nat` when
+reduced at transparency levels below `semireducible`, i.e. where `D` would not be unfolded either,
+preventing "defeq abuse".
+
+More specifically, given the "source type" (the argument) and "target type" (the expected type),
+`inferInstanceAs` synthesizes an instance for the source type and then unfolds and rewraps its
+components (fields, nested instances) as necessary to make them compatible with the target type. The
+individual steps are represented by the following options, which all default to enabled and can be
+disabled to help with porting:
+
+* `backward.inferInstanceAs.wrap`: master switch for instance adjustment in both `inferInstanceAs`
+  and the default deriving handler
+* `backward.inferInstanceAs.wrap.reuseSubInstances`: reuse existing instances for the target type
+  for sub-instance fields to avoid non-defeq instance diamonds
+* `backward.inferInstanceAs.wrap.instances`: wrap non-reducible instances in auxiliary definitions
+* `backward.inferInstanceAs.wrap.data`: wrap data fields in auxiliary definitions (proof fields are
+  always wrapped)
+
+If you just need to synthesize an instance without transporting between types, use `inferInstance`
+instead, potentially with a type annotation for the expected type.
 -/
 abbrev «inferInstanceAs» (α : Sort u) [i : α] : α := i
 
@@ -3673,7 +3688,7 @@ def panic {α : Sort u} [Inhabited α] (msg : String) : α :=
   panicCore msg
 
 -- TODO: this be applied directly to `Inhabited`'s definition when we remove the above workaround
-attribute [nospecialize] Inhabited
+attribute [weak_specialize] Inhabited
 
 /--
 The `>>=` operator is overloaded via instances of `bind`.

src/Lean/Attributes.lean

@@ -186,11 +186,11 @@ def registerTagAttribute (name : Name) (descr : String)
     mkInitial       := pure {}
     addImportedFn   := fun _ _ => pure {}
     addEntryFn      := fun (s : NameSet) n => s.insert n
-    exportEntriesFnEx := fun env es _ =>
-      let r : Array Name := es.foldl (fun a e => a.push e) #[]
-      -- Do not export info for private defs
-      let r := r.filter (env.contains (skipRealize := false))
-      r.qsort Name.quickLt
+    exportEntriesFnEx := fun env es =>
+      let all : Array Name := es.foldl (fun a e => a.push e) #[] |>.qsort Name.quickLt
+      -- Do not export info for private defs at exported/server levels
+      let exported := all.filter ((env.setExporting true).contains (skipRealize := false))
+      { exported, server := exported, «private» := all }
     statsFn         := fun s => "tag attribute" ++ Format.line ++ "number of local entries: " ++ format s.size
     asyncMode       := asyncMode
     replay?         := some fun _ newState newConsts s =>
@@ -266,15 +266,14 @@ def registerParametricAttribute (impl : ParametricAttributeImpl α) : IO (Parame
     mkInitial       := pure ([], {})
     addImportedFn   := fun _ => pure ([], {})
     addEntryFn      := fun (decls, m) (p : Name × α) => (p.1 :: decls, m.insert p.1 p.2)
-    exportEntriesFnEx := fun env (decls, m) lvl => Id.run do
-      let mut r := if impl.preserveOrder then
+    exportEntriesFnEx := fun env (decls, m) => Id.run do
+      let all := if impl.preserveOrder then
         decls.toArray.reverse.filterMap (fun n => return (n, ← m.find? n))
       else
         let r := m.foldl (fun a n p => a.push (n, p)) #[]
         r.qsort (fun a b => Name.quickLt a.1 b.1)
-      if lvl != .private then
-        r := r.filter (fun ⟨n, a⟩ => impl.filterExport env n a)
-      r
+      let exported := all.filter (fun ⟨n, a⟩ => impl.filterExport env n a)
+      { exported, server := exported, «private» := all }
     statsFn         := fun (_, m) => "parametric attribute" ++ Format.line ++ "number of local entries: " ++ format m.size
   }
   let attrImpl : AttributeImpl := {
@@ -333,11 +332,11 @@ def registerEnumAttributes (attrDescrs : List (Name × String × α))
     mkInitial       := pure {}
     addImportedFn   := fun _ _ => pure {}
     addEntryFn      := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2
-    exportEntriesFnEx := fun env m _ =>
-      let r : Array (Name × α) := m.foldl (fun a n p => a.push (n, p)) #[]
-      -- Do not export info for private defs
-      let r := r.filter (env.contains (skipRealize := false) ·.1)
-      r.qsort (fun a b => Name.quickLt a.1 b.1)
+    exportEntriesFnEx := fun env m =>
+      let all : Array (Name × α) := m.foldl (fun a n p => a.push (n, p)) #[] |>.qsort (fun a b => Name.quickLt a.1 b.1)
+      -- Do not export info for private defs at exported/server levels
+      let exported := all.filter ((env.setExporting true).contains (skipRealize := false) ·.1)
+      { exported, server := exported, «private» := all }
     statsFn         := fun s => "enumeration attribute extension" ++ Format.line ++ "number of local entries: " ++ format s.size
     -- We assume (and check in `modifyState`) that, if used asynchronously, enum attributes are set
     -- only in the same context in which the tagged declaration was created

src/Lean/Compiler/ExternAttr.lean

@@ -55,11 +55,6 @@ private def syntaxToExternAttrData (stx : Syntax) : AttrM ExternAttrData := do
       entries := entries.push <| ExternEntry.inline backend str
   return { entries := entries.toList }
 
--- Forward declaration
-set_option compiler.ignoreBorrowAnnotation true in
-@[extern "lean_add_extern"]
-opaque addExtern (declName : Name) (externAttrData : ExternAttrData) : CoreM Unit
-
 builtin_initialize externAttr : ParametricAttribute ExternAttrData ←
   registerParametricAttribute {
     name := `extern
@@ -71,7 +66,7 @@ builtin_initialize externAttr : ParametricAttribute ExternAttrData ←
         if let some (.thmInfo ..) := env.find? declName then
           -- We should not mark theorems as extern
           return ()
-        addExtern declName externAttrData
+        compileDecls #[declName]
   }
 
 def getExternAttrData? (env : Environment) (n : Name) : Option ExternAttrData :=

src/Lean/Compiler/IR.lean

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Lean.Compiler.IR.AddExtern
 public import Lean.Compiler.IR.Basic
 public import Lean.Compiler.IR.Format
 public import Lean.Compiler.IR.CompilerM

src/Lean/Compiler/IR/AddExtern.lean

@@ -1,86 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Cameron Zwarich
--/
-
-module
-
-prelude
-import Init.While
-import Lean.Compiler.IR.ToIR
-import Lean.Compiler.LCNF.ToImpureType
-import Lean.Compiler.LCNF.ToImpure
-import Lean.Compiler.LCNF.ExplicitBoxing
-import Lean.Compiler.LCNF.Internalize
-public import Lean.Compiler.ExternAttr
-import Lean.Compiler.LCNF.ExplicitRC
-import Lean.Compiler.Options
-
-public section
-
-namespace Lean.IR
-
-set_option compiler.ignoreBorrowAnnotation true in
-@[export lean_add_extern]
-def addExtern (declName : Name) (externAttrData : ExternAttrData) : CoreM Unit := do
-  if !isPrivateName declName then
-    modifyEnv (Compiler.LCNF.setDeclPublic · declName)
-  let monoDecl ← addMono declName
-  let impureDecls ← addImpure monoDecl
-  addIr impureDecls
-where
-  addMono (declName : Name) : CoreM (Compiler.LCNF.Decl .pure) := do
-    let type ← Compiler.LCNF.getOtherDeclMonoType declName
-    let mut typeIter := type
-    let mut params := #[]
-    let ignoreBorrow := Compiler.compiler.ignoreBorrowAnnotation.get (← getOptions)
-    repeat
-      let .forallE binderName ty b _ := typeIter | break
-      let borrow := !ignoreBorrow && isMarkedBorrowed ty
-      params := params.push {
-        fvarId := (← mkFreshFVarId)
-        type := ty,
-        binderName,
-        borrow
-      }
-      typeIter := b
-    let decl := {
-      name := declName,
-      levelParams := [],
-      value := .extern externAttrData,
-      inlineAttr? := some .noinline,
-      type,
-      params,
-    }
-    decl.saveMono
-    return decl
-
-  addImpure (decl : Compiler.LCNF.Decl .pure) : CoreM (Array (Compiler.LCNF.Decl .impure)) := do
-    let type ← Compiler.LCNF.lowerResultType decl.type decl.params.size
-    let params ← decl.params.mapM fun param =>
-      return { param with type := ← Compiler.LCNF.toImpureType param.type }
-    let decl : Compiler.LCNF.Decl .impure := {
-      name := decl.name,
-      levelParams := decl.levelParams,
-      value := .extern externAttrData
-      inlineAttr? := some .noinline,
-      type,
-      params
-    }
-    Compiler.LCNF.CompilerM.run (phase := .impure) do
-      let decl ← decl.internalize
-      decl.saveImpure
-      let decls ← Compiler.LCNF.addBoxedVersions #[decl]
-      let decls ← Compiler.LCNF.runExplicitRc decls
-      for decl in decls do
-        decl.saveImpure
-        modifyEnv fun env => Compiler.LCNF.recordFinalImpureDecl env decl.name
-      return decls
-
-  addIr (decls : Array (Compiler.LCNF.Decl .impure)) : CoreM Unit := do
-    let decls ← toIR decls
-    logDecls `result decls
-    addDecls decls
-
-end Lean.IR

src/Lean/Compiler/IR/CompilerM.lean

@@ -86,11 +86,11 @@ builtin_initialize declMapExt : SimplePersistentEnvExtension Decl DeclMap ←
     addEntryFn    := fun s d => s.insert d.name d
     -- Store `meta` closure only in `.olean`, turn all other decls into opaque externs.
     -- Leave storing the remainder for `meta import` and server `#eval` to `exportIREntries` below.
-    exportEntriesFnEx? := some fun env s entries _ =>
+    exportEntriesFnEx? := some fun env s entries =>
       let decls := entries.foldl (init := #[]) fun decls decl => decls.push decl
       let entries := sortDecls decls
       -- Do not save all IR even in .olean.private as it will be in .ir anyway
-      if env.header.isModule then
+      .uniform <| if env.header.isModule then
         entries.filterMap fun d => do
           if isDeclMeta env d.name then
             return d
@@ -126,12 +126,12 @@ private def exportIREntries (env : Environment) : Array (Name × Array EnvExtens
   -- save all initializers independent of meta/private. Non-meta initializers will only be used when
   -- .ir is actually loaded, and private ones iff visible.
   let initDecls : Array (Name × Name) :=
-    regularInitAttr.ext.exportEntriesFn env (regularInitAttr.ext.getState env) .private
+    (regularInitAttr.ext.exportEntriesFn env (regularInitAttr.ext.getState env)).private
   -- safety: cast to erased type
   let initDecls : Array EnvExtensionEntry := unsafe unsafeCast initDecls
 
   -- needed during initialization via interpreter
-  let modPkg : Array (Option PkgId) := modPkgExt.exportEntriesFn env (modPkgExt.getState env) .private
+  let modPkg : Array (Option PkgId) := (modPkgExt.exportEntriesFn env (modPkgExt.getState env)).private
   -- safety: cast to erased type
   let modPkg : Array EnvExtensionEntry := unsafe unsafeCast modPkg
 

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

@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+module
+
+prelude
+public import Lean.Compiler.LCNF.CompilerM
+public import Lean.Compiler.LCNF.PassManager
+
+namespace Lean.Compiler.LCNF
+
+/-!
+# Coalesce Reference Counting Operations
+
+This pass coalesces multiple `inc`/`dec` operations on the same variable within a basic block.
+Within a basic block, it is always safe to:
+- Move all increments on a variable to the first `inc` location (summing the counts). Because if
+  there are later `inc`s no intermediate operation can observe RC=1 (as the value must stay alive
+  until the later inc) and thus doing all relevant `inc` in the beginning doesn't change
+  semantics.
+- Move all decrements on a variable to the last `dec` location (summing the counts). Because the
+  value is guaranteed to stay alive until at least the last `dec` anyway so a similar argument to
+  `inc` holds.
+
+Crucially this pass must be placed after `expandResetReuse` as that one relies on `inc`s still being
+present in their original location for optimization purposes.
+-/
+
+private structure State where
+  /-- Total inc count per variable in the current basic block (accumulated going forward). -/
+  incTotal : Std.HashMap FVarId Nat := {}
+  /-- Total dec count per variable in the current basic block (accumulated going forward). -/
+  decTotal : Std.HashMap FVarId Nat := {}
+  /--
+  Inc count seen so far per variable going backward. When this equals `incTotal`, we've
+  reached the first inc and should emit the coalesced operation.
+  -/
+  incAccum : Std.HashMap FVarId Nat := {}
+  /--
+  Whether we've already emitted the coalesced dec for a variable (going backward, the first
+  dec encountered is the last in the block).
+  -/
+  decPlaced : Std.HashSet FVarId := {}
+
+private abbrev M := StateRefT State CompilerM
+
+/--
+Coalesce inc/dec operations within individual basic blocks.
+-/
+partial def Code.coalesceRC (code : Code .impure) : CompilerM (Code .impure) := do
+  go code |>.run' {}
+where
+  go (code : Code .impure) : M (Code .impure) := do
+    match code with
+    | .inc fvarId n check persistent k _ =>
+      modify fun s => { s with incTotal := s.incTotal.alter fvarId (fun v? => some ((v?.getD 0) + n)) }
+      let k ← go k
+      modify fun s => { s with incAccum := s.incAccum.alter fvarId (fun v? => some ((v?.getD 0) + n)) }
+      let s ← get
+      if s.incAccum[fvarId]! == s.incTotal[fvarId]! then
+        return .inc fvarId s.incTotal[fvarId]! check persistent k
+      else
+        return k
+    | .dec fvarId n check persistent k _ =>
+      modify fun s => { s with decTotal := s.decTotal.alter fvarId (fun v? => some ((v?.getD 0) + n)) }
+      let k ← go k
+      let s ← get
+      if !s.decPlaced.contains fvarId then
+        modify fun s => { s with decPlaced := s.decPlaced.insert fvarId }
+        return .dec fvarId s.decTotal[fvarId]! check persistent k
+      else
+        return k
+    | .let _ k =>
+      let k ← go k
+      return code.updateCont! k
+    | .jp decl k =>
+      let value ← decl.value.coalesceRC
+      let decl ← decl.updateValue value
+      let k ← go k
+      return code.updateFun! decl k
+    | .cases c =>
+      let alts ← c.alts.mapMonoM (·.mapCodeM (·.coalesceRC))
+      return code.updateAlts! alts
+    | .del _ k _ =>
+      let k ← go k
+      return code.updateCont! k
+    | .oset (k := k) .. | .uset (k := k) .. | .sset (k := k) .. | .setTag (k := k) .. =>
+      let k ← go k
+      return code.updateCont! k
+    | .return .. | .jmp .. | .unreach .. => return code
+
+def Decl.coalesceRC (decl : Decl .impure) : CompilerM (Decl .impure) := do
+  let value ← decl.value.mapCodeM Code.coalesceRC
+  return { decl with value }
+
+public def coalesceRC : Pass :=
+  .mkPerDeclaration `coalesceRc .impure Decl.coalesceRC
+
+builtin_initialize
+  registerTraceClass `Compiler.coalesceRc (inherited := true)
+
+end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/ElimDeadBranches.lean

@@ -291,10 +291,9 @@ builtin_initialize functionSummariesExt : SimplePersistentEnvExtension (Name ×
   registerSimplePersistentEnvExtension {
     addImportedFn := fun _ => {}
     addEntryFn := fun s ⟨e, n⟩ => s.insert e n
-    exportEntriesFnEx? := some fun _ s _ => fun
+    exportEntriesFnEx? := some fun _ s _ =>
       -- preserved for non-modules, make non-persistent at some point?
-      | .private => s.toArray.qsort decLt
-      | _ => #[]
+      { exported := #[], server := #[], «private» := s.toArray.qsort decLt }
     asyncMode := .sync  -- compilation is non-parallel anyway
     replay? := some <| SimplePersistentEnvExtension.replayOfFilter (!·.contains ·.1) (fun s ⟨e, n⟩ => s.insert e n)
   }

src/Lean/Compiler/LCNF/ExpandResetReuse.lean

@@ -69,8 +69,8 @@ open ImpureType
 abbrev Mask := Array (Option FVarId)
 
 /--
-Try to erase `inc` instructions on projections of `targetId` occuring in the tail of `ds`.
-Return the updated `ds` and mask contianing the `FVarId`s whose `inc` was removed.
+Try to erase `inc` instructions on projections of `targetId` occurring in the tail of `ds`.
+Return the updated `ds` and mask containing the `FVarId`s whose `inc` was removed.
 -/
 partial def eraseProjIncFor (nFields : Nat) (targetId : FVarId) (ds : Array (CodeDecl .impure)) :
     CompilerM (Array (CodeDecl .impure) × Mask) := do

src/Lean/Compiler/LCNF/ExplicitRC.lean

@@ -31,9 +31,12 @@ namespace Lean.Compiler.LCNF
 open ImpureType
 
 /-!
-The following section contains the derived value analysis. It figures out a dependency tree of
+The following section contains the derived value analysis. It figures out a dependency graph of
 values that were derived from other values through projections or `Array` accesses. This information
 is later used in the derived borrow analysis to reduce reference counting pressure.
+
+When a derived value has more than one parent, it is derived from one of the parent values but we
+cannot statically determine which one.
 -/
 
 /--
@@ -41,10 +44,10 @@ Contains information about values derived through various forms of projection fr
 -/
 structure DerivedValInfo where
   /--
-  The variable this value was derived from. This is always set except for parameters as they have no
-  value to be derived from.
+  The set of variables this value may derive from. This is always set except for parameters as they
+  have no value to be derived from.
   -/
-  parent? : Option FVarId
+  parents : Array FVarId
   /--
   The set of variables that were derived from this value.
   -/
@@ -56,59 +59,85 @@ abbrev DerivedValMap := Std.HashMap FVarId DerivedValInfo
 namespace CollectDerivedValInfo
 
 structure State where
+  /--
+  The dependency graph of values.
+  -/
   varMap : DerivedValMap := {}
-  borrowedParams : FVarIdHashSet := {}
+  /--
+  The set of values that are to be interpreted as being borrowed by nature. This currently includes:
+  - borrowed parameters
+  - variables that are initialized from constants
+  -/
+  borrowedValues : FVarIdHashSet := {}
 
 abbrev M := StateRefT State CompilerM
 
 @[inline]
-def visitParam (p : Param .impure) : M Unit :=
+def addDerivedValue (parents : Array FVarId) (child : FVarId) : M Unit := do
   modify fun s => { s with
-    varMap := s.varMap.insert p.fvarId {
-      parent? := none
-      children := {}
-    }
-    borrowedParams :=
-      if p.borrow && p.type.isPossibleRef then
-        s.borrowedParams.insert p.fvarId
-      else
-        s.borrowedParams
+    varMap :=
+      let varMap := parents.foldl (init := s.varMap)
+        (·.modify · (fun info => { info with children := info.children.insert child }))
+      varMap.insert child { parents := parents, children := {} }
   }
 
 @[inline]
-def addDerivedValue (parent : FVarId) (child : FVarId) : M Unit := do
-  modify fun s => { s with
-    varMap :=
-      s.varMap
-        |>.modify parent (fun info => { info with children := info.children.insert child })
-        |>.insert child { parent? := some parent, children := {} }
-  }
+def addBorrowedValue (fvarId : FVarId) : M Unit := do
+  modify fun s => { s with borrowedValues := s.borrowedValues.insert fvarId }
 
-def removeFromParent (child : FVarId) : M Unit := do
-  if let some parent := (← get).varMap.get? child |>.bind (·.parent?) then
-    modify fun s => { s with
-      varMap := s.varMap.modify parent fun info =>
-        { info with children := info.children.erase child }
-    }
+def addDerivedLetValue (parents : Array FVarId) (child : FVarId) : M Unit := do
+  let type ← getType child
+  if !type.isPossibleRef then
+    return ()
+  let parents ← parents.filterM fun fvarId => do
+    let type ← getType fvarId
+    return type.isPossibleRef
+  addDerivedValue parents child
+  if parents.isEmpty then
+      addBorrowedValue child
+
+@[inline]
+def visitParam (p : Param .impure) : M Unit := do
+  addDerivedValue #[] p.fvarId
+  if p.borrow && p.type.isPossibleRef then
+    addBorrowedValue p.fvarId
+
+def removeFromParents (child : FVarId) : M Unit := do
+  if let some entry := (← get).varMap.get? child then
+    for parent in entry.parents do
+      modify fun s => { s with
+        varMap := s.varMap.modify parent fun info =>
+          { info with children := info.children.erase child }
+      }
 
 partial def collectCode (code : Code .impure) : M Unit := do
   match code with
   | .let decl k =>
     match decl.value with
     | .oproj _ parent =>
-      addDerivedValue parent decl.fvarId
+      addDerivedLetValue #[parent] decl.fvarId
     -- Keep in sync with PropagateBorrow, InferBorrow
     | .fap ``Array.getInternal args =>
       if let .fvar parent := args[1]! then
-        addDerivedValue parent decl.fvarId
+        addDerivedLetValue #[parent] decl.fvarId
     | .fap ``Array.get!Internal args =>
+      let mut parents := #[]
+      /-
+      Because execution may continue after a panic, the value resulting from a get!InternalBorrowed
+      may be derived from either the `Inhabited` instance or the `Array` argument.
+      -/
+      if let .fvar parent := args[1]! then
+        parents := parents.push parent
       if let .fvar parent := args[2]! then
-        addDerivedValue parent decl.fvarId
+        parents := parents.push parent
+      addDerivedLetValue parents decl.fvarId
     | .fap ``Array.uget args =>
       if let .fvar parent := args[1]! then
-        addDerivedValue parent decl.fvarId
+        addDerivedLetValue #[parent] decl.fvarId
+    | .fap _ #[] =>
+      addDerivedLetValue #[] decl.fvarId
     | .reset _ target =>
-      removeFromParent target
+      removeFromParents target
     | _ => pure ()
     collectCode k
   | .jp decl k =>
@@ -125,8 +154,8 @@ Collect the derived value tree as well as the set of parameters that take object
 -/
 def collect (ps : Array (Param .impure)) (code : Code .impure) :
     CompilerM (DerivedValMap × FVarIdHashSet) := do
-  let ⟨_, { varMap, borrowedParams }⟩ ← go |>.run {}
-  return ⟨varMap, borrowedParams⟩
+  let ⟨_, { varMap, borrowedValues }⟩ ← go |>.run {}
+  return ⟨varMap, borrowedValues⟩
 where
   go : M Unit := do
     ps.forM visitParam
@@ -170,13 +199,21 @@ def LiveVars.erase (liveVars : LiveVars) (fvarId : FVarId) : LiveVars :=
   let borrows := liveVars.borrows.erase fvarId
   { vars, borrows }
 
+@[inline]
+def LiveVars.insertBorrow (liveVars : LiveVars) (fvarId : FVarId) : LiveVars :=
+  { liveVars with borrows := liveVars.borrows.insert fvarId }
+
+@[inline]
+def LiveVars.insertLive (liveVars : LiveVars) (fvarId : FVarId) : LiveVars :=
+  { liveVars with vars := liveVars.vars.insert fvarId }
+
 abbrev JPLiveVarMap := FVarIdMap LiveVars
 
 structure Context where
   /--
-  The set of all parameters that are borrowed and take potential objects as arguments.
+  The set of all values that are borrowed and potentially objects
   -/
-  borrowedParams : FVarIdHashSet
+  borrowedValues : FVarIdHashSet
   /--
   The derived value tree.
   -/
@@ -277,18 +314,21 @@ def withCollectLiveVars (x : RcM α) : RcM (α × LiveVars) := do
   return (ret, collected)
 
 /--
-Traverse the transitive closure of values derived from `fvarId` and add them to `s` if they pass
-`shouldAdd`.
+Traverse the transitive closure of values derived from `fvarId` and add them to `s` if:
+- they pass `shouldAdd`.
+- all their parents are accessible
 -/
 @[specialize]
-partial def addDescendants (fvarId : FVarId) (derivedValMap : DerivedValMap) (s : FVarIdHashSet)
-    (shouldAdd : FVarId → Bool := fun _ => true) : FVarIdHashSet :=
+partial def addDescendants (fvarId : FVarId) (derivedValMap : DerivedValMap) (liveVars : LiveVars)
+    (shouldAdd : FVarId → Bool := fun _ => true) : LiveVars :=
   if let some info := derivedValMap.get? fvarId then
-    info.children.fold (init := s) fun s child =>
-      let s := if shouldAdd child then s.insert child else s
-      addDescendants child derivedValMap s shouldAdd
+    info.children.fold (init := liveVars) fun liveVars child =>
+      let cinfo := derivedValMap.get! child
+      let parentsOk := cinfo.parents.all fun fvarId => (liveVars.vars.contains fvarId || liveVars.borrows.contains fvarId)
+      let liveVars := if parentsOk && shouldAdd child then liveVars.insertBorrow child else liveVars
+      addDescendants child derivedValMap liveVars shouldAdd
   else
-    s
+    liveVars
 
 /--
 Mark `fvarId` as live from here on out and if there are any derived values that are not live anymore
@@ -299,20 +339,21 @@ alive after all).
 def useVar (fvarId : FVarId) (shouldBorrow : FVarId → Bool := fun _ => true) : RcM Unit := do
   if !(← isLive fvarId) then
     let derivedValMap := (← read).derivedValMap
+    modifyLive fun liveVars => { liveVars with vars := liveVars.vars.insert fvarId }
     modifyLive fun liveVars =>
-      { liveVars with
-          borrows := addDescendants fvarId derivedValMap liveVars.borrows fun y =>
-            !liveVars.vars.contains y && shouldBorrow y
-          vars := liveVars.vars.insert fvarId
-      }
+      addDescendants fvarId derivedValMap liveVars fun y =>
+        !liveVars.vars.contains y && shouldBorrow y
 
 def useArgs (args : Array (Arg .impure)) : RcM Unit := do
   args.forM fun arg =>
     match arg with
     | .fvar fvarId =>
       useVar fvarId fun y =>
-        -- If a value is used as an argument we are going to mark it live anyways so don't mark it
-        -- as borrowed.
+        /-
+        If we are in a situation like `f x y` where `x` would imply that `y` remains borrowed we are
+        going to mark `y` as being live instead of borrowed later on anyways. Instead we skip this
+        intermediate state and don't even begin to consider it as borrowed.
+        -/
         args.all fun arg =>
           match arg with
           | .fvar z => y != z
@@ -341,9 +382,9 @@ def setRetLiveVars : RcM Unit := do
   let derivedValMap := (← read).derivedValMap
   -- At the end of a function no values are live and all borrows derived from parameters will still
   -- be around.
-  let borrows := (← read).borrowedParams.fold (init := {}) fun borrows x =>
-    addDescendants x derivedValMap (borrows.insert x)
-  modifyLive fun _ => { vars := {}, borrows }
+  let liveVars := (← read).borrowedValues.fold (init := {}) fun liveVars x =>
+    addDescendants x derivedValMap (liveVars.insertBorrow x)
+  modifyLive (fun _ => liveVars)
 
 @[inline]
 def addInc (fvarId : FVarId) (k : Code .impure) (n : Nat := 1) : RcM (Code .impure) := do
@@ -625,9 +666,9 @@ partial def Code.explicitRc (code : Code .impure) : RcM (Code .impure) := do
 def Decl.explicitRc (decl : Decl .impure) :
     CompilerM (Decl .impure) := do
   let value ← decl.value.mapCodeM fun code => do
-    let ⟨derivedValMap, borrowedParams⟩ ← CollectDerivedValInfo.collect decl.params code
+    let ⟨derivedValMap, borrowedValues⟩ ← CollectDerivedValInfo.collect decl.params code
     go code |>.run {
-      borrowedParams,
+      borrowedValues,
       derivedValMap,
     } |>.run' {}
   return { decl with value }

src/Lean/Compiler/LCNF/InferBorrow.lean

@@ -375,7 +375,6 @@ where
     match v with
     | .reset _ x => ownFVar z (.resetReuse z); ownFVar x (.resetReuse z)
     | .reuse x _ _ args => ownFVar z (.resetReuse z); ownFVar x (.resetReuse z); ownArgsIfParam z args
-    | .ctor _ args => ownFVar z (.constructorResult z); ownArgsIfParam z args
     | .oproj _ x _ =>
       if ← isOwned x then ownFVar z (.forwardProjectionProp z)
       if ← isOwned z then ownFVar x (.backwardProjectionProp z)
@@ -384,6 +383,8 @@ where
       if let .fvar parent := args[1]! then
         if ← isOwned parent then ownFVar z (.forwardProjectionProp z)
     | .fap ``Array.get!Internal args =>
+      if let .fvar parent := args[1]! then
+        if ← isOwned parent then ownFVar z (.forwardProjectionProp z)
       if let .fvar parent := args[2]! then
         if ← isOwned parent then ownFVar z (.forwardProjectionProp z)
     | .fap ``Array.uget args =>
@@ -396,6 +397,9 @@ where
         let ps ← getParamInfo (.decl f)
         ownFVar z (.functionCallResult z)
         ownArgsUsingParams args ps (.functionCallArg z)
+    | .ctor i args =>
+      if !i.isScalar then
+        ownFVar z (.constructorResult z); ownArgsIfParam z args
     | .fvar x args =>
       ownFVar z (.functionCallResult z); ownFVar x (.fvarCall z); ownArgs (.fvarCall z) args
     | .pap _ args => ownFVar z (.functionCallResult z); ownArgs (.partialApplication z) args

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.
@@ -96,21 +100,25 @@ builtin_initialize postponedCompileDeclsExt : SimplePersistentEnvExtension Postp
     asyncMode     := .sync
     replay?       := some <| SimplePersistentEnvExtension.replayOfFilter
       (fun s e => !e.declNames.any s.contains) (fun s e => e.declNames.foldl (·.insert · e) s)
-    exportEntriesFnEx? := some fun _ _ es lvl =>
+    exportEntriesFnEx? := some fun _ _ es =>
       -- `leanir` imports the target module privately
-      if lvl == .private then es.toArray else #[]
+      { 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/Passes.lean

@@ -26,6 +26,7 @@ public import Lean.Compiler.LCNF.SimpCase
 public import Lean.Compiler.LCNF.InferBorrow
 public import Lean.Compiler.LCNF.ExplicitBoxing
 public import Lean.Compiler.LCNF.ExplicitRC
+public import Lean.Compiler.LCNF.CoalesceRC
 public import Lean.Compiler.LCNF.Toposort
 public import Lean.Compiler.LCNF.ExpandResetReuse
 public import Lean.Compiler.LCNF.SimpleGroundExpr
@@ -149,6 +150,7 @@ def builtinPassManager : PassManager := {
     explicitBoxing,
     explicitRc,
     expandResetReuse,
+    coalesceRC,
     pushProj (occurrence := 1),
     detectSimpleGround,
     inferVisibility (phase := .impure),

src/Lean/Compiler/LCNF/PhaseExt.lean

@@ -93,16 +93,15 @@ def mkDeclExt (phase : Phase) (name : Name := by exact decl_name%) :
     mkInitial := pure {},
     addImportedFn := fun _ => pure {},
     addEntryFn := fun s decl => s.insert decl.name decl
-    exportEntriesFnEx env s level := Id.run do
-      let mut entries := sortedEntries s declLt
-      if level != .private then
-        entries := entries.filterMap fun decl => do
-          guard <| isDeclPublic env decl.name
-          if isDeclTransparent env phase decl.name then
-            some decl
-          else
-            some { decl with value := .extern { entries := [.opaque] } }
-      return entries
+    exportEntriesFnEx env s := Id.run do
+      let all := sortedEntries s declLt
+      let exported := all.filterMap fun decl => do
+        guard <| isDeclPublic env decl.name
+        if isDeclTransparent env phase decl.name then
+          some decl
+        else
+          some { decl with value := .extern { entries := [.opaque] } }
+      return { exported, server := exported, «private» := all }
     statsFn := statsFn,
     asyncMode := .sync,
     replay? := some (replayFn phase)
@@ -138,13 +137,12 @@ def mkSigDeclExt (phase : Phase) (name : Name := by exact decl_name%) :
     mkInitial := pure {},
     addImportedFn := fun _ => pure {},
     addEntryFn := fun s sig => s.insert sig.name sig
-    exportEntriesFnEx env s level := Id.run do
-      let mut entries := sortedEntries s sigLt
-      if level != .private then
-        entries := entries.filterMap fun sig => do
-          guard <| isDeclPublic env sig.name
-          some sig
-      return entries
+    exportEntriesFnEx env s := Id.run do
+      let all := sortedEntries s sigLt
+      let exported := all.filterMap fun sig => do
+        guard <| isDeclPublic env sig.name
+        some sig
+      return { exported, server := exported, «private» := all }
     statsFn := statsFn,
     asyncMode := .sync,
     replay? := some (replayFn phase)

src/Lean/Compiler/LCNF/PropagateBorrow.lean

@@ -114,6 +114,9 @@ where
         let parentVal ← getOwnedness parent
         join z parentVal
     | .fap ``Array.get!Internal args =>
+      if let .fvar parent := args[1]! then
+        let parentVal ← getOwnedness parent
+        join z parentVal
       if let .fvar parent := args[2]! then
         let parentVal ← getOwnedness parent
         join z parentVal
@@ -124,7 +127,10 @@ where
     | .fap _ args =>
       let value := if args.isEmpty then .borrow else .own
       join z value
-    | .ctor .. | .fvar .. | .pap .. | .sproj .. | .uproj .. | .erased .. | .lit .. =>
+    | .ctor i _ =>
+      let value := if i.isScalar then .borrow else .own
+      join z value
+    | .fvar .. | .pap .. | .sproj .. | .uproj .. | .erased .. | .lit .. =>
       join z .own
     | _ => unreachable!
 

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

@@ -178,10 +178,11 @@ partial def compileToSimpleGroundExpr (code : Code .impure) : CompilerM (Option
 where
   go (code : Code .impure) : DetectM SimpleGroundExpr := do
     match code with
-    | .let decl (.return fvarId) =>
+    | .let decl (.return fvarId) | .let decl (.inc _ _ _ true  (.return fvarId)) =>
       guard <| decl.fvarId == fvarId
       compileFinalLet decl.value
     | .let decl k => compileNonFinalLet decl k
+    | .inc (persistent := true) (k := k) .. => go k
     | _ => failure
 
   @[inline]

src/Lean/Compiler/LCNF/SpecInfo.lean

@@ -20,8 +20,10 @@ inductive SpecParamInfo where
   /--
   A parameter that is an type class instance (or an arrow that produces a type class instance),
   and is fixed in recursive declarations. By default, Lean always specializes this kind of argument.
+  If the `weak` parameter is set we only specialize for this parameter iff another parameter causes
+  specialization as well.
   -/
-  | fixedInst
+  | fixedInst (weak : Bool)
   /--
   A parameter that is a function and is fixed in recursive declarations. If the user tags a declaration
   with `@[specialize]` without specifying which arguments should be specialized, Lean will specialize
@@ -49,14 +51,15 @@ namespace SpecParamInfo
 
 @[inline]
 def causesSpecialization : SpecParamInfo → Bool
-  | .fixedInst | .fixedHO | .user => true
-  | .fixedNeutral | .other => false
+  | .fixedInst false | .fixedHO | .user => true
+  | .fixedInst true | .fixedNeutral | .other => false
 
 end SpecParamInfo
 
 instance : ToMessageData SpecParamInfo where
   toMessageData
-    | .fixedInst => "I"
+    | .fixedInst false => "I"
+    | .fixedInst true => "W"
     | .fixedHO => "H"
     | .fixedNeutral => "N"
     | .user => "U"
@@ -130,6 +133,18 @@ private def isNoSpecType (env : Environment) (type : Expr) : Bool :=
     else
       false
 
+/--
+Return `true` if `type` is a type tagged with `@[weak_specialize]` or an arrow that produces this kind of type.
+-/
+private def isWeakSpecType (env : Environment) (type : Expr) : Bool :=
+  match type with
+  | .forallE _ _ b _ => isWeakSpecType env b
+  | _ =>
+    if let .const declName _ := type.getAppFn then
+      hasWeakSpecializeAttribute env declName
+    else
+      false
+
 /-!
 *Note*: `fixedNeutral` must have forward dependencies.
 
@@ -160,7 +175,7 @@ See comment at `.fixedNeutral`.
 private def hasFwdDeps (decl : Decl .pure) (paramsInfo : Array SpecParamInfo) (j : Nat) : Bool := Id.run do
   let param := decl.params[j]!
   for h : k in (j+1)...decl.params.size do
-    if paramsInfo[k]!.causesSpecialization then
+    if paramsInfo[k]!.causesSpecialization || paramsInfo[k]! matches .fixedInst .. then
       let param' := decl.params[k]
       if param'.type.containsFVar param.fvarId then
         return true
@@ -199,7 +214,7 @@ def computeSpecEntries (decls : Array (Decl .pure)) (autoSpecialize : Name → O
           else if isTypeFormerType param.type then
             pure .fixedNeutral
           else if (← isArrowClass? param.type).isSome then
-            pure .fixedInst
+            pure (.fixedInst (weak := isWeakSpecType (← getEnv) param.type))
           /-
           Recall that if `specArgs? == some #[]`, then user annotated function with `@[specialize]`, but did not
           specify which arguments must be specialized besides instances. In this case, we try to specialize

src/Lean/Compiler/LCNF/Specialize.lean

@@ -31,11 +31,8 @@ builtin_initialize specCacheExt : SimplePersistentEnvExtension CacheEntry Cache
   registerSimplePersistentEnvExtension {
     addEntryFn    := addEntry
     addImportedFn := fun es => (mkStateFromImportedEntries addEntry {} es).switch
-    exportEntriesFnEx? := some fun _ _ entries level =>
-      if level == .private then
-        entries.toArray
-      else
-        #[]
+    exportEntriesFnEx? := some fun _ _ entries =>
+      { exported := #[], server := #[], «private» := entries.toArray }
     asyncMode     := .sync
     replay?       := some <| SimplePersistentEnvExtension.replayOfFilter
       (!·.contains ·.key) addEntry
@@ -209,7 +206,7 @@ def collect (paramsInfo : Array SpecParamInfo) (args : Array (Arg .pure)) :
       match paramInfo with
       | .other =>
         argMask := argMask.push none
-      | .fixedNeutral | .user | .fixedInst | .fixedHO =>
+      | .fixedNeutral | .user | .fixedInst .. | .fixedHO =>
         argMask := argMask.push (some arg)
         Closure.collectArg arg
     return argMask
@@ -257,7 +254,8 @@ def shouldSpecialize (specEntry : SpecEntry) (args : Array (Arg .pure)) : Specia
     match paramInfo with
     | .other => pure ()
     | .fixedNeutral => pure () -- If we want to monomorphize types such as `Array`, we need to change here
-    | .fixedInst | .user => if ← isGround arg then return true
+    | .fixedInst true => pure ()  -- weak: don't trigger specialization on its own
+    | .fixedInst false | .user => if ← isGround arg then return true
     | .fixedHO => if ← hoCheck arg then return true
 
   return false
@@ -509,7 +507,7 @@ def updateLocalSpecParamInfo : SpecializeM Unit := do
   for entry in infos do
     if let some mask := (← get).parentMasks[entry.declName]? then
       let maskInfo info :=
-        mask.zipWith info (f := fun b i => if !b && i.causesSpecialization then .other else i)
+        mask.zipWith info (f := fun b i => if !b && (i.causesSpecialization || i matches .fixedInst ..) then .other else i)
       let entry := { entry with paramsInfo := maskInfo entry.paramsInfo }
       modify fun s => {
         s with

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/Compiler/MetaAttr.lean

@@ -39,11 +39,9 @@ private builtin_initialize declMetaExt : SimplePersistentEnvExtension Name NameS
     addEntryFn := fun s n => s.insert n
     asyncMode := .sync
     replay? := some <| SimplePersistentEnvExtension.replayOfFilter (!·.contains ·) (·.insert ·)
-    exportEntriesFnEx? := some fun env s entries => fun
-      | .private =>
-        let decls := entries.foldl (init := #[]) fun decls decl => decls.push decl
-        decls.qsort Name.quickLt
-      | _ => #[]
+    exportEntriesFnEx? := some fun env s entries =>
+      let decls := entries.foldl (init := #[]) fun decls decl => decls.push decl
+      { exported := #[], server := #[], «private» := decls.qsort Name.quickLt }
   }
 
 /-- Whether a declaration should be exported for interpretation. -/

src/Lean/Compiler/Specialize.lean

@@ -24,6 +24,17 @@ Marks a definition to never be specialized during code generation.
 builtin_initialize nospecializeAttr : TagAttribute ←
   registerTagAttribute `nospecialize "mark definition to never be specialized"
 
+/--
+Marks a type for weak specialization: Parameters of this type are only specialized when
+another argument already triggers specialization. Unlike `@[nospecialize]`, if specialization
+happens for other reasons, parameters of this type will participate in the specialization
+rather than being ignored.
+-/
+@[builtin_doc]
+builtin_initialize weakSpecializeAttr : TagAttribute ←
+  registerTagAttribute `weak_specialize
+    "mark type for weak specialization: instances are only specialized when another argument already triggers specialization"
+
 private def elabSpecArgs (declName : Name) (args : Array Syntax) : MetaM (Array Nat) := do
   if args.isEmpty then return #[]
   let info ← getConstInfo declName
@@ -82,4 +93,7 @@ def hasSpecializeAttribute (env : Environment) (declName : Name) : Bool :=
 def hasNospecializeAttribute (env : Environment) (declName : Name) : Bool :=
   nospecializeAttr.hasTag env declName
 
+def hasWeakSpecializeAttribute (env : Environment) (declName : Name) : Bool :=
+  weakSpecializeAttr.hasTag env declName
+
 end Lean.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/DeclarationRange.lean

@@ -18,10 +18,9 @@ namespace Lean
 
 builtin_initialize builtinDeclRanges : IO.Ref (NameMap DeclarationRanges) ← IO.mkRef {}
 builtin_initialize declRangeExt : MapDeclarationExtension DeclarationRanges ←
-  mkMapDeclarationExtension (exportEntriesFn := fun _ s level =>
-    if level < .server then
-      #[]
-    else s.toArray)
+  mkMapDeclarationExtension (exportEntriesFn := fun _ s =>
+    let ents := s.toArray
+    { exported := #[], server := ents, «private» := ents })
 
 def addBuiltinDeclarationRanges (declName : Name) (declRanges : DeclarationRanges) : IO Unit :=
   builtinDeclRanges.modify (·.insert declName declRanges)

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/DocString/Extension.lean

@@ -78,27 +78,21 @@ private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) ← IO.mk
 builtin_initialize docStringExt : MapDeclarationExtension String ←
   mkMapDeclarationExtension
     (asyncMode := .async .asyncEnv)
-    (exportEntriesFn := fun _ s level =>
-      if level < .server then
-        {}
-      else
-        s.toArray)
+    (exportEntriesFn := fun _ s =>
+      let ents := s.toArray
+      { exported := #[], server := ents, «private» := ents })
 private builtin_initialize inheritDocStringExt : MapDeclarationExtension Name ←
-  mkMapDeclarationExtension (exportEntriesFn := fun _ s level =>
-    if level < .server then
-      {}
-    else
-      s.toArray)
+  mkMapDeclarationExtension (exportEntriesFn := fun _ s =>
+    let ents := s.toArray
+    { exported := #[], server := ents, «private» := ents })
 
 private builtin_initialize builtinVersoDocStrings : IO.Ref (NameMap VersoDocString) ← IO.mkRef {}
 builtin_initialize versoDocStringExt : MapDeclarationExtension VersoDocString ←
   mkMapDeclarationExtension
     (asyncMode := .async .asyncEnv)
-    (exportEntriesFn := fun _ s level =>
-      if level < .server then
-        {}
-      else
-        s.toArray)
+    (exportEntriesFn := fun _ s =>
+      let ents := s.toArray
+      { exported := #[], server := ents, «private» := ents })
 
 /--
 Adds a builtin docstring to the compiler.
@@ -196,11 +190,9 @@ private builtin_initialize moduleDocExt :
     SimplePersistentEnvExtension ModuleDoc (PersistentArray ModuleDoc) ← registerSimplePersistentEnvExtension {
   addImportedFn := fun _ => {}
   addEntryFn    := fun s e => s.push e
-  exportEntriesFnEx? := some fun _ _ es level =>
-    if level < .server then
-      #[]
-    else
-      es.toArray
+  exportEntriesFnEx? := some fun _ _ es =>
+    let ents := es.toArray
+    { exported := #[], server := ents, «private» := ents }
 }
 
 def addMainModuleDoc (env : Environment) (doc : ModuleDoc) : Environment :=
@@ -407,11 +399,9 @@ private builtin_initialize versoModuleDocExt :
     SimplePersistentEnvExtension VersoModuleDocs.Snippet VersoModuleDocs ← registerSimplePersistentEnvExtension {
   addImportedFn := fun _ => {}
   addEntryFn    := fun s e => s.add! e
-  exportEntriesFnEx? := some fun _ _ es level =>
-    if level < .server then
-      #[]
-    else
-      es.toArray
+  exportEntriesFnEx? := some fun _ _ es =>
+    let ents := es.toArray
+    { exported := #[], server := ents, «private» := ents }
 }
 
 

src/Lean/Elab.lean

@@ -39,6 +39,7 @@ public import Lean.Elab.Extra
 public import Lean.Elab.GenInjective
 public import Lean.Elab.BuiltinTerm
 public import Lean.Elab.Arg
+public import Lean.Elab.DeprecatedArg
 public import Lean.Elab.PatternVar
 public import Lean.Elab.ElabRules
 public import Lean.Elab.Macro

src/Lean/Elab/App.lean

@@ -11,6 +11,7 @@ public import Lean.Elab.Binders
 public import Lean.Elab.RecAppSyntax
 public import Lean.IdentifierSuggestion
 import all Lean.Elab.ErrorUtils
+import Lean.Elab.DeprecatedArg
 import Init.Omega
 
 public section
@@ -88,6 +89,38 @@ def synthesizeAppInstMVars (instMVars : Array MVarId) (app : Expr) : TermElabM U
 private def findBinderName? (namedArgs : List NamedArg) (binderName : Name) : Option NamedArg :=
   namedArgs.find? fun namedArg => namedArg.name == binderName
 
+/--
+If the function being applied is a constant, search `namedArgs` for an argument whose name is
+a deprecated alias of `binderName`. When `linter.deprecated.arg` is enabled (the default),
+returns `some namedArg` after emitting a deprecation warning with a code action hint. When the
+option is disabled, returns `none` (the old name falls through to the normal "invalid argument"
+error). The returned `namedArg` retains its original (old) name.
+-/
+private def findDeprecatedBinderName? (namedArgs : List NamedArg) (f : Expr) (binderName : Name) :
+    TermElabM (Option NamedArg) := do
+  unless linter.deprecated.arg.get <| ← getOptions do return .none
+  unless f.getAppFn.isConst do return none
+  let declName := f.getAppFn.constName!
+  let env ← getEnv
+  for namedArg in namedArgs do
+    if let some entry := findDeprecatedArg? env declName namedArg.name then
+      if entry.newArg? == some binderName then
+        let msg := formatDeprecatedArgMsg entry
+        let span? := namedArg.ref[1]
+        let hint ←
+          if span?.getHeadInfo matches .original .. then
+            MessageData.hint "Rename this argument:" #[{
+              suggestion := .string entry.newArg?.get!.toString
+              span?
+              toCodeActionTitle? := some fun s =>
+                s!"Rename argument `{entry.oldArg}` to `{s}`"
+            }]
+          else
+            pure .nil
+        logWarningAt namedArg.ref <| .tagged ``deprecatedArgExt msg ++ hint
+        return some namedArg
+  return none
+
 /-- Erase entry for `binderName` from `namedArgs`. -/
 def eraseNamedArg (namedArgs : List NamedArg) (binderName : Name) : List NamedArg :=
   namedArgs.filter (·.name != binderName)
@@ -238,6 +271,23 @@ private def synthesizePendingAndNormalizeFunType : M Unit := do
     else
       for namedArg in s.namedArgs do
         let f := s.f.getAppFn
+        if f.isConst then
+          let env ← getEnv
+          if linter.deprecated.arg.get (← getOptions) then
+            if let some entry := findDeprecatedArg? env f.constName! namedArg.name then
+              if entry.newArg?.isNone then
+                let msg := formatDeprecatedArgMsg entry
+                let hint ←
+                  if namedArg.ref.getHeadInfo matches .original .. then
+                    MessageData.hint "Delete this argument:" #[{
+                      suggestion := .string ""
+                      span? := namedArg.ref
+                      toCodeActionTitle? := some fun _ =>
+                        s!"Delete deprecated argument `{entry.oldArg}`"
+                    }]
+                  else
+                    pure .nil
+                throwErrorAt namedArg.ref (msg ++ hint)
         let validNames ← getFoundNamedArgs
         let fnName? := if f.isConst then some f.constName! else none
         throwInvalidNamedArg namedArg fnName? validNames
@@ -756,13 +806,16 @@ mutual
       let binderName := fType.bindingName!
       let binfo := fType.bindingInfo!
       let s ← get
-      match findBinderName? s.namedArgs binderName with
+      let namedArg? ← match findBinderName? s.namedArgs binderName with
+        | some namedArg => pure (some namedArg)
+        | none => findDeprecatedBinderName? s.namedArgs s.f binderName
+      match namedArg? with
       | some namedArg =>
         propagateExpectedType namedArg.val
-        eraseNamedArg binderName
+        eraseNamedArg namedArg.name
         elabAndAddNewArg binderName namedArg.val
         main
-      | none          =>
+      | none =>
         unless binderName.hasMacroScopes do
           pushFoundNamedArg binderName
         match binfo with
@@ -1779,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
@@ -1825,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}`"
@@ -1866,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
@@ -1881,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.
@@ -2033,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/If.lean

@@ -63,6 +63,6 @@ where
     doElabToSyntax "else branch of if with condition {cond}" (elabDiteBranch false) fun else_ => do
     let mγ ← mkMonadicType (← read).doBlockResultType
     match h with
-    | `(_%$tk) => Term.elabTermEnsuringType (← `(if $(⟨tk⟩):hole : $cond then $then_ else $else_)) mγ
+    | `(_%$tk) => Term.elabTermEnsuringType (← `(if _%$tk : $cond then $then_ else $else_)) mγ
     | `($h:ident) => Term.elabTermEnsuringType (← `(if $h:ident : $cond then $then_ else $else_)) mγ
     | _ => throwUnsupportedSyntax

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

@@ -43,7 +43,7 @@ builtin_initialize
 
   Upon such rewrite, the code for adding flat inductives does not diverge much from the usual
   way its done for inductive declarations, but we omit applying attributes/modifiers and
-  we do not set the syntax references to track those declarations (as this is auxillary piece of
+  we do not set the syntax references to track those declarations (as this is auxiliary piece of
   data hidden from the user).
 
   Then, upon adding such flat inductives for each definition in the mutual block to the environment,
@@ -345,7 +345,7 @@ private def mkCasesOnCoinductive (infos : Array InductiveVal) : MetaM Unit := do
         | throwError "expected to be quantifier"
       let motiveMVar ← mkFreshExprMVar type
       /-
-        We intro all the indices and the occurence of the coinductive predicate
+        We intro all the indices and the occurrence of the coinductive predicate
       -/
       let (fvars, subgoal) ← motiveMVar.mvarId!.introN (info.numIndices + 1)
       subgoal.withContext do
@@ -373,7 +373,7 @@ private def mkCasesOnCoinductive (infos : Array InductiveVal) : MetaM Unit := do
           -/
           let originalCasesOn := mkAppN originalCasesOn indices
           /-
-            The next argument is the occurence of the coinductive predicate.
+            The next argument is the occurrence of the coinductive predicate.
             The original `casesOn` of the flat inductive mentions it in
             unrolled form, so we need to rewrite it.
           -/
@@ -447,7 +447,7 @@ public def elabCoinductive (coinductiveElabData : Array CoinductiveElabData) : T
   let consts := namesAndTypes.map fun (name, _) => (mkConst name levelParams)
   /-
     We create values of each of PreDefinitions, by taking existential (see `Meta.SumOfProducts`)
-    form of the associated flat inductives and applying paramaters, as well as recursive calls
+    form of the associated flat inductives and applying parameters, as well as recursive calls
     (with their parameters passed).
   -/
   let preDefVals ← forallBoundedTelescope infos[0]!.type originalNumParams fun params _ => do

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

@@ -0,0 +1,97 @@
+/-
+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.EnvExtension
+public import Lean.Message
+import Lean.Elab.Term
+
+public section
+
+namespace Lean.Elab
+open Meta
+
+register_builtin_option linter.deprecated.arg : Bool := {
+  defValue := true
+  descr := "if true, generate deprecation warnings and errors for deprecated parameters"
+}
+
+/-- Entry mapping an old parameter name to a new (or no) parameter for a given declaration. -/
+structure DeprecatedArgEntry where
+  declName : Name
+  oldArg : Name
+  newArg? : Option Name := none
+  text? : Option String := none
+  since? : Option String := none
+  deriving Inhabited
+
+/-- State: `declName → (oldArg → entry)` -/
+abbrev DeprecatedArgState := NameMap (NameMap DeprecatedArgEntry)
+
+private def addDeprecatedArgEntry (s : DeprecatedArgState) (e : DeprecatedArgEntry) : DeprecatedArgState :=
+  let inner := (s.find? e.declName).getD {} |>.insert e.oldArg e
+  s.insert e.declName inner
+
+builtin_initialize deprecatedArgExt :
+    SimplePersistentEnvExtension DeprecatedArgEntry DeprecatedArgState ←
+  registerSimplePersistentEnvExtension {
+    addEntryFn := addDeprecatedArgEntry
+    addImportedFn := mkStateFromImportedEntries addDeprecatedArgEntry {}
+  }
+
+/-- Look up a deprecated argument mapping for `(declName, argName)`. -/
+def findDeprecatedArg? (env : Environment) (declName : Name) (argName : Name) :
+    Option DeprecatedArgEntry :=
+  (deprecatedArgExt.getState env |>.find? declName) >>= (·.find? argName)
+
+/-- Format the deprecation warning message for a deprecated argument. -/
+def formatDeprecatedArgMsg (entry : DeprecatedArgEntry) : MessageData :=
+  let base := match entry.newArg? with
+  | some newArg =>
+    m!"parameter `{entry.oldArg}` of `{.ofConstName entry.declName}` has been deprecated, \
+      use `{newArg}` instead"
+  | none =>
+    m!"parameter `{entry.oldArg}` of `{.ofConstName entry.declName}` has been deprecated"
+  match entry.text? with
+  | some text => base ++ m!": {text}"
+  | none => base
+
+builtin_initialize registerBuiltinAttribute {
+  name := `deprecated_arg
+  descr := "mark a parameter as deprecated"
+  add := fun declName stx _kind => do
+    let `(attr| deprecated_arg $oldId $[$newId?]? $[$text?]? $[(since := $since?)]?) := stx
+      | throwError "Invalid `[deprecated_arg]` attribute syntax"
+    let oldArg := oldId.getId
+    let newArg? := newId?.map TSyntax.getId
+    let text? := text?.map TSyntax.getString |>.filter (!·.isEmpty)
+    let since? := since?.map TSyntax.getString
+    let info ← getConstInfo declName
+    let paramNames ← MetaM.run' do
+      forallTelescopeReducing info.type fun xs _ =>
+        xs.mapM fun x => return (← x.fvarId!.getDecl).userName
+    if let some newArg := newArg? then
+      -- We have a replacement provided
+      unless Array.any paramNames (· == newArg) do
+        throwError "`{newArg}` is not a parameter of `{declName}`"
+      if Array.any paramNames (· == oldArg) then
+        throwError "`{oldArg}` is still a parameter of `{declName}`; \
+          rename it to `{newArg}` before adding `@[deprecated_arg]`"
+    else
+      -- We do not have a replacement provided
+      if Array.any paramNames (· == oldArg) then
+        throwError "`{oldArg}` is still a parameter of `{declName}`; \
+          remove it before adding `@[deprecated_arg]`"
+    if since?.isNone then
+      logWarning "`[deprecated_arg]` attribute should specify the date or library version \
+        at which the deprecation was introduced, using `(since := \"...\")`"
+    modifyEnv fun env => deprecatedArgExt.addEntry env {
+      declName, oldArg, newArg?, text?, since?
+    }
+}
+
+end Lean.Elab

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)

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

@@ -26,9 +26,11 @@ public structure EqnInfo where
   deriving Inhabited
 
 public builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ←
-  mkMapDeclarationExtension (exportEntriesFn := fun env s _ =>
-    -- Do not export for non-exposed defs
-    s.filter (fun n _ => env.find? n |>.any (·.hasValue)) |>.toArray)
+  mkMapDeclarationExtension (exportEntriesFn := fun env s =>
+    let all := s.toArray
+    -- Do not export for non-exposed defs at exported/server levels
+    let exported := s.filter (fun n _ => (env.setExporting true).find? n |>.any (·.hasValue)) |>.toArray
+    { exported, server := exported, «private» := all })
 
 public def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name)
     (fixedParamPerms : FixedParamPerms) (fixpointType : Array PartialFixpointType): MetaM Unit := do

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -148,9 +148,11 @@ where
             throwError "no progress at goal\n{MessageData.ofGoal mvarId}"
 
 public builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ←
-  mkMapDeclarationExtension (exportEntriesFn := fun env s _ =>
-    -- Do not export for non-exposed defs
-    s.filter (fun n _ => env.find? n |>.any (·.hasValue)) |>.toArray)
+  mkMapDeclarationExtension (exportEntriesFn := fun env s =>
+    let all := s.toArray
+    -- Do not export for non-exposed defs at exported/server levels
+    let exported := s.filter (fun n _ => (env.setExporting true).find? n |>.any (·.hasValue)) |>.toArray
+    { exported, server := exported, «private» := all })
 
 public def registerEqnsInfo (preDef : PreDefinition) (declNames : Array Name) (recArgPos : Nat)
     (fixedParamPerms : FixedParamPerms) : CoreM Unit := do

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

@@ -24,9 +24,11 @@ public structure EqnInfo where
   deriving Inhabited
 
 public builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ←
-  mkMapDeclarationExtension (exportEntriesFn := fun env s _ =>
-    -- Do not export for non-exposed defs
-    s.filter (fun n _ => env.find? n |>.any (·.hasValue)) |>.toArray)
+  mkMapDeclarationExtension (exportEntriesFn := fun env s =>
+    let all := s.toArray
+    -- Do not export for non-exposed defs at exported/server levels
+    let exported := s.filter (fun n _ => (env.setExporting true).find? n |>.any (·.hasValue)) |>.toArray
+    { exported, server := exported, «private» := all })
 
 public def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedParamPerms : FixedParamPerms)
     (argsPacker : ArgsPacker) : MetaM Unit := do

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

@@ -243,10 +243,6 @@ private def printAxiomsOf (constName : Name) : CommandElabM Unit := do
 
 @[builtin_command_elab «printAxioms»] def elabPrintAxioms : CommandElab
   | `(#print%$tk axioms $id) => withRef tk do
-    if (← getEnv).header.isModule then
-      throwError "cannot use `#print axioms` in a `module`; consider temporarily removing the \
-        `module` header or placing the command in a separate file"
-
     let cs ← liftCoreM <| realizeGlobalConstWithInfos id
     cs.forM printAxiomsOf
   | _ => throwUnsupportedSyntax

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

@@ -31,7 +31,7 @@ open Lean.Parser.Command
 def allRecommendedSpellings : MetaM (Array RecommendedSpelling) := do
   let all := recommendedSpellingExt.toEnvExtension.getState (← getEnv)
       |>.importedEntries
-      |>.push (recommendedSpellingExt.exportEntriesFn (← getEnv) (recommendedSpellingExt.getState (← getEnv)) .exported)
+      |>.push ((recommendedSpellingExt.exportEntriesFn (← getEnv) (recommendedSpellingExt.getState (← getEnv))).exported)
   return all.flatMap id
 
 end Lean.Elab.Term.Doc

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

@@ -256,15 +256,15 @@ Marks a type as an invariant type for the `mvcgen` tactic.
 Goals whose type is an application of a tagged type will be classified
 as invariants rather than verification conditions.
 -/
-builtin_initialize mvcgenInvariantAttr : TagAttribute ←
-  registerTagAttribute `mvcgen_invariant_type
+builtin_initialize specInvariantAttr : TagAttribute ←
+  registerTagAttribute `spec_invariant_type
     "marks a type as an invariant type for the `mvcgen` tactic"
 
 /--
-Returns `true` if `ty` is an application of a type tagged with `@[mvcgen_invariant_type]`.
+Returns `true` if `ty` is an application of a type tagged with `@[spec_invariant_type]`.
 -/
-def isMVCGenInvariantType (env : Environment) (ty : Expr) : Bool :=
+def isSpecInvariantType (env : Environment) (ty : Expr) : Bool :=
   if let .const name .. := ty.getAppFn then
-    mvcgenInvariantAttr.hasTag env name
+    specInvariantAttr.hasTag env name
   else
     false

src/Lean/Elab/Tactic/Do/Spec.lean

@@ -75,7 +75,7 @@ def elabSpec (stx? : Option (TSyntax `term)) (wp : Expr) : TacticM SpecTheorem :
   | none => findSpec (← getSpecTheorems) wp
   | some stx => elabTermIntoSpecTheorem stx expectedTy
 
-variable {n} [Monad n] [MonadControlT MetaM n] [MonadLiftT MetaM n]
+variable {n} [Monad n] [MonadControlT MetaM n] [MonadLiftT MetaM n] [MonadEnv n]
 
 private def mkProj' (n : Name) (i : Nat) (Q : Expr) : MetaM Expr := do
   return (← projectCore? Q i).getD (mkProj n i Q)
@@ -181,11 +181,12 @@ public def mSpec (goal : MGoal) (elabSpecAtWP : Expr → n SpecTheorem) (goalTag
   -- Instantiation creates `.natural` MVars, which possibly get instantiated by the def eq checks
   -- below when they occur in `P` or `Q`.
   -- That's good for many such as MVars ("schematic variables"), but problematic for MVars
-  -- corresponding to `Invariant`s, which should end up as user goals.
-  -- To prevent accidental instantiation, we mark all `Invariant` MVars as synthetic opaque.
+  -- corresponding to invariant types, which should end up as user goals.
+  -- To prevent accidental instantiation, we mark all invariant MVars as synthetic opaque.
+  let env ← getEnv
   for mvar in mvars do
     let ty ← mvar.mvarId!.getType
-    if ty.isAppOf ``Invariant then mvar.mvarId!.setKind .syntheticOpaque
+    if isSpecInvariantType env ty then mvar.mvarId!.setKind .syntheticOpaque
 
   -- Apply the spec to the excess arguments of the `wp⟦e⟧ Q` application
   let T := goal.target.consumeMData

src/Lean/Elab/Tactic/Do/VCGen.lean

@@ -364,7 +364,7 @@ def elabInvariants (stx : Syntax) (invariants : Array MVarId) (suggestInvariant
     for h : n in 0...alts.size do
       let alt := alts[n]
       match alt with
-      | `(goalDotAlt| · $rhs) =>
+      | `(invariantDotAlt| · $rhs) =>
         if dotOrCase matches .false then
           logErrorAt alt m!"Alternation between labelled and bulleted invariants is not supported."
           break
@@ -374,7 +374,7 @@ def elabInvariants (stx : Syntax) (invariants : Array MVarId) (suggestInvariant
           continue
         withRef rhs do
         discard <| evalTacticAt (← `(tactic| exact $rhs)) mv
-      | `(goalCaseAlt| | $tag $args* => $rhs) =>
+      | `(invariantCaseAlt| | $tag $args* => $rhs) =>
         if dotOrCase matches .true then
           logErrorAt alt m!"Alternation between labelled and bulleted invariants is not supported."
           break
@@ -391,7 +391,7 @@ def elabInvariants (stx : Syntax) (invariants : Array MVarId) (suggestInvariant
           continue
         withRef rhs do
         discard <| evalTacticAt (← `(tactic| rename_i $args*; exact $rhs)) mv
-      | _ => logErrorAt alt m!"Expected `goalDotAlt`, got {alt}"
+      | _ => logErrorAt alt m!"Expected `invariantDotAlt`, got {alt}"
 
     if let `(invariantsKW| invariants) := invariantsKW then
       if alts.size < invariants.size then
@@ -405,7 +405,7 @@ def elabInvariants (stx : Syntax) (invariants : Array MVarId) (suggestInvariant
         if ← mv.isAssigned then
           continue
         let invariant ← suggestInvariant mv
-        suggestions := suggestions.push (← `(goalDotAlt| · $invariant))
+        suggestions := suggestions.push (← `(invariantDotAlt| · $invariant))
       let alts' := alts ++ suggestions
       let stx' ← `(invariantAlts|invariants $alts'*)
       if suggestions.size > 0 then

src/Lean/Elab/Tactic/Do/VCGen/Basic.lean

@@ -104,7 +104,7 @@ def addSubGoalAsVC (goal : MVarId) : VCGenM PUnit := do
   -- VC to the user as-is, without abstracting any variables in the local context.
   -- This only makes sense for synthetic opaque metavariables.
   goal.setKind .syntheticOpaque
-  if isMVCGenInvariantType (← getEnv) ty then
+  if isSpecInvariantType (← getEnv) ty then
     modify fun s => { s with invariants := s.invariants.push goal }
   else
     modify fun s => { s with vcs := s.vcs.push goal }

src/Lean/Elab/Tactic/Doc.lean

@@ -52,7 +52,7 @@ def firstTacticTokens [Monad m] [MonadEnv m] : m (NameMap String) := do
   let mut firstTokens : NameMap String :=
     tacticNameExt.toEnvExtension.getState env
       |>.importedEntries
-      |>.push (tacticNameExt.exportEntriesFn env (tacticNameExt.getState env) .exported)
+      |>.push ((tacticNameExt.exportEntriesFn env (tacticNameExt.getState env)).exported)
       |>.foldl (init := {}) fun names inMods =>
         inMods.foldl (init := names) fun names (k, n) =>
           names.insert k n
@@ -108,7 +108,7 @@ Displays all available tactic tags, with documentation.
 @[builtin_command_elab printTacTags] def elabPrintTacTags : CommandElab := fun _stx => do
   let all :=
     tacticTagExt.toEnvExtension.getState (← getEnv)
-      |>.importedEntries |>.push (tacticTagExt.exportEntriesFn (← getEnv) (tacticTagExt.getState (← getEnv)) .exported)
+      |>.importedEntries |>.push ((tacticTagExt.exportEntriesFn (← getEnv) (tacticTagExt.getState (← getEnv))).exported)
   let mut mapping : NameMap NameSet := {}
   for arr in all do
     for (tac, tag) in arr do
@@ -160,7 +160,7 @@ def allTacticDocs (includeUnnamed : Bool := true) : MetaM (Array TacticDoc) := d
   let env ← getEnv
   let allTags :=
     tacticTagExt.toEnvExtension.getState env |>.importedEntries
-      |>.push (tacticTagExt.exportEntriesFn env (tacticTagExt.getState env) .exported)
+      |>.push ((tacticTagExt.exportEntriesFn env (tacticTagExt.getState env)).exported)
   let mut tacTags : NameMap NameSet := {}
   for arr in allTags do
     for (tac, tag) in arr do

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

@@ -26,7 +26,7 @@ structure SimplePersistentEnvExtensionDescr (α σ : Type) where
   addImportedFn : Array (Array α) → σ
   toArrayFn     : List α → Array α := fun es => es.toArray
   exportEntriesFnEx? :
-    Option (Environment → σ → List α → OLeanLevel → Array α) := none
+    Option (Environment → σ → List α → OLeanEntries (Array α)) := none
   asyncMode     : EnvExtension.AsyncMode := .mainOnly
   replay?       : Option ((newEntries : List α) → (newState : σ) → σ → List α × σ) := none
 
@@ -48,9 +48,9 @@ def registerSimplePersistentEnvExtension {α σ : Type} [Inhabited σ] (descr :
     addImportedFn   := fun as => pure ([], descr.addImportedFn as),
     addEntryFn      := fun s e => match s with
       | (entries, s) => (e::entries, descr.addEntryFn s e),
-    exportEntriesFnEx env s level := match descr.exportEntriesFnEx? with
-      | some fn => fn env s.2 s.1.reverse level
-      | none    => descr.toArrayFn s.1.reverse
+    exportEntriesFnEx env s := match descr.exportEntriesFnEx? with
+      | some fn => fn env s.2 s.1.reverse
+      | none    => .uniform (descr.toArrayFn s.1.reverse)
     statsFn := fun s => format "number of local entries: " ++ format s.1.length
     asyncMode := descr.asyncMode
     replay? := descr.replay?.map fun replay oldState newState _ (entries, s) =>
@@ -131,16 +131,18 @@ deriving Inhabited
 
 def mkMapDeclarationExtension (name : Name := by exact decl_name%)
     (asyncMode : EnvExtension.AsyncMode := .async .mainEnv)
-    (exportEntriesFn : Environment → NameMap α → OLeanLevel → Array (Name × α) :=
+    (exportEntriesFn : Environment → NameMap α → OLeanEntries (Array (Name × α)) :=
       -- Do not export info for private defs by default
-      fun env s _ => s.toArray.filter (fun (n, _) => env.contains (skipRealize := false) n)) :
+      fun env s =>
+        let all := s.toArray.filter (fun (n, _) => env.contains (skipRealize := false) n)
+        .uniform all) :
     IO (MapDeclarationExtension α) :=
   .mk <$> registerPersistentEnvExtension {
     name            := name,
     mkInitial       := pure {}
     addImportedFn   := fun _ => pure {}
     addEntryFn      := fun s (n, v) => s.insert n v
-    exportEntriesFnEx env s level := exportEntriesFn env s level
+    exportEntriesFnEx env s := exportEntriesFn env s
     asyncMode
     replay?         := some fun _ newState newConsts s =>
       newConsts.foldl (init := s) fun s c =>

src/Lean/Environment.lean

@@ -1540,6 +1540,23 @@ deriving DecidableEq, Ord, Repr
 instance : LE OLeanLevel := leOfOrd
 instance : LT OLeanLevel := ltOfOrd
 
+/-- Data computed once per extension for all three olean levels. Avoids calling the export function
+    three separate times so that expensive computations can be shared. -/
+structure OLeanEntries (α : Type) where
+  exported : α
+  server   : α
+  «private» : α
+  deriving Inhabited
+
+/-- Create `OLeanEntries` with the same value for all levels. -/
+def OLeanEntries.uniform (a : α) : OLeanEntries α := ⟨a, a, a⟩
+
+/-- Look up the entry for a given level. -/
+def OLeanEntries.get (e : OLeanEntries α) : OLeanLevel → α
+  | .exported => e.exported
+  | .server   => e.server
+  | .private  => e.private
+
 /--
 An environment extension with support for storing/retrieving entries from a .olean file.
  - α is the type of the entries that are stored in .olean files.
@@ -1591,16 +1608,17 @@ structure PersistentEnvExtension (α : Type) (β : Type) (σ : Type) where
   addImportedFn   : Array (Array α) → ImportM σ
   addEntryFn      : σ → β → σ
   /--
-  Function to transform state into data that should be imported into other modules. When using the
+  Function to transform state into data that should be imported into other modules. Returns entries
+  for all three olean levels at once so that expensive computations can be shared. When using the
   module system without `import all`, `OLeanLevel.exported` is imported, else `OLeanLevel.private`.
   Additionally, when using the module system in the language server, the `OLeanLevel.server` data is
   accessible via `getModuleEntries (level := .server)`. By convention, each level should include all
   data of previous levels.
 
-  This function is run after elaborating the file and joining all asynchronous threads. It is run
-  once for each level when the module system is enabled, otherwise once for `private`.
+  This function is run once after elaborating the file and joining all asynchronous threads.
+  For non-module files, only the `private` field is used.
   -/
-  exportEntriesFn : Environment → σ → OLeanLevel → Array α
+  exportEntriesFn : Environment → σ → OLeanEntries (Array α)
   statsFn         : σ → Format
 
 instance {α σ} [Inhabited σ] : Inhabited (PersistentEnvExtensionState α σ) :=
@@ -1612,7 +1630,7 @@ instance {α β σ} [Inhabited σ] : Inhabited (PersistentEnvExtension α β σ)
      name := default,
      addImportedFn := fun _ => default,
      addEntryFn := fun s _ => s,
-     exportEntriesFn := fun _ _ _ => #[],
+     exportEntriesFn := fun _ _ => .uniform #[],
      statsFn := fun _ => Format.nil
   }
 
@@ -1668,7 +1686,7 @@ structure PersistentEnvExtensionDescrCore (α β σ : Type) where
   mkInitial         : IO σ
   addImportedFn     : Array (Array α) → ImportM σ
   addEntryFn        : σ → β → σ
-  exportEntriesFnEx : Environment → σ → OLeanLevel → Array α
+  exportEntriesFnEx : Environment → σ → OLeanEntries (Array α)
   statsFn           : σ → Format := fun _ => Format.nil
   asyncMode         : EnvExtension.AsyncMode := .mainOnly
   replay?           : Option (ReplayFn σ) := none
@@ -1687,11 +1705,11 @@ def useDefaultIfOtherFieldGiven (default : α) (_otherField : β) : α :=
 structure PersistentEnvExtensionDescr (α β σ : Type) extends PersistentEnvExtensionDescrCore α β σ where
   -- The cyclic default values force the user to specify at least one of the two following fields.
   /--
-  Obsolete simpler version of `exportEntriesFnEx`. Its value is ignored if the latter is also
-  specified.
+  Obsolete simpler version of `exportEntriesFnEx` that returns the same entries for all levels.
+  Its value is ignored if the latter is also specified.
   -/
   exportEntriesFn : σ → Array α := useDefaultIfOtherFieldGiven (fun _ => #[]) exportEntriesFnEx
-  exportEntriesFnEx := fun _ s _ => exportEntriesFn s
+  exportEntriesFnEx := fun _ s => .uniform (exportEntriesFn s)
 
 unsafe def registerPersistentEnvExtensionUnsafe {α β σ : Type} [Inhabited σ] (descr : PersistentEnvExtensionDescr α β σ) : IO (PersistentEnvExtension α β σ) := do
   let pExts ← persistentEnvExtensionsRef.get
@@ -1779,19 +1797,40 @@ set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_get_ir_extra_const_names"]
 private opaque getIRExtraConstNames (env : Environment) (level : OLeanLevel) (includeDecls := false) : Array Name
 
-def mkModuleData (env : Environment) (level : OLeanLevel := .private) : IO ModuleData := do
-  let env := env.setExporting (level != .private)
+/--
+Compute extension entries for all levels at once by calling `exportEntriesFn` once per extension.
+Returns an `OLeanEntries` of arrays mapping extension names to their exported data.
+-/
+private def computeExtEntries (env : Environment) :
+    IO (OLeanEntries (Array (Name × Array EnvExtensionEntry))) := do
   let pExts ← persistentEnvExtensionsRef.get
-  let entries := pExts.filterMap fun pExt => do
-    -- get state from `checked` at the end if `async`; it would otherwise panic
-    let mut asyncMode := pExt.toEnvExtension.asyncMode
-    if asyncMode matches .async _ then
-      asyncMode := .sync
+  let allEntries := pExts.map fun pExt =>
+    let asyncMode := match pExt.toEnvExtension.asyncMode with
+      | .async _ => .sync
+      | m => m
     let state := pExt.getState (asyncMode := asyncMode) env
-    let ents := pExt.exportEntriesFn env state level
-    -- no need to export empty entries
-    guard !ents.isEmpty
-    return (pExt.name, ents)
+    let oe := pExt.exportEntriesFn env state
+    (pExt.name, oe)
+  let filterNonEmpty (level : OLeanLevel) :=
+    allEntries.filterMap fun (name, oe) => do
+      let ents := oe.get level
+      guard !ents.isEmpty
+      pure (name, ents)
+  return {
+    exported := filterNonEmpty .exported
+    server   := filterNonEmpty .server
+    «private» := filterNonEmpty .private
+  }
+
+def mkModuleData (env : Environment) (level : OLeanLevel := .private)
+    (extEntries? : Option (OLeanEntries (Array (Name × Array EnvExtensionEntry))) := none) :
+    IO ModuleData := do
+  let env := env.setExporting (level != .private)
+  let entries ← match extEntries? with
+    | some ee => pure (ee.get level)
+    | none => do
+      let ee ← computeExtEntries env
+      pure (ee.get level)
   let kenv := env.toKernelEnv
   let constNames := kenv.constants.foldStage2 (fun names name _ => names.push name) #[]
   -- not all kernel constants may be exported at `level < .private`
@@ -1828,8 +1867,9 @@ private def mkIRData (env : Environment) : ModuleData :=
 
 def writeModule (env : Environment) (fname : System.FilePath) (writeIR := true) : IO Unit := do
   if env.header.isModule then
+    let extEntries ← computeExtEntries env
     let mkPart (level : OLeanLevel) :=
-      return (level.adjustFileName fname, (← mkModuleData env level))
+      return (level.adjustFileName fname, (← mkModuleData env level extEntries))
     saveModuleDataParts env.mainModule #[
       (← mkPart .exported),
       (← mkPart .server),
@@ -2215,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/Expr.lean

@@ -1751,6 +1751,12 @@ def isFalse (e : Expr) : Bool :=
 def isTrue (e : Expr) : Bool :=
   e.cleanupAnnotations.isConstOf ``True
 
+def isBoolFalse (e : Expr) : Bool :=
+  e.cleanupAnnotations.isConstOf ``false
+
+def isBoolTrue (e : Expr) : Bool :=
+  e.cleanupAnnotations.isConstOf ``true
+
 /--
 `getForallArity type` returns the arity of a `forall`-type. This function consumes nested annotations,
 and performs pending beta reductions. It does **not** use whnf.

src/Lean/ExtraModUses.lean

@@ -66,9 +66,8 @@ builtin_initialize extraModUses : SimplePersistentEnvExtension ExtraModUse (PHas
   registerSimplePersistentEnvExtension {
     addEntryFn m k := m.insert k
     addImportedFn _ := {}
-    exportEntriesFnEx? := some fun _ _ entries => fun
-      | .private => entries.toArray
-      | _        => #[]
+    exportEntriesFnEx? := some fun _ _ entries =>
+      { exported := #[], server := #[], «private» := entries.toArray }
     asyncMode := .sync
     replay? := some <| SimplePersistentEnvExtension.replayOfFilter (·.contains ·) (·.insert ·)
   }

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

@@ -91,10 +91,10 @@ end FoldRelevantConstantsImpl
 @[implemented_by FoldRelevantConstantsImpl.foldUnsafe]
 public opaque foldRelevantConstants {α : Type} (e : Expr) (init : α) (f : Name → α → MetaM α) : MetaM α := pure init
 
-/-- Collect the constants occuring in `e` (once each), skipping instance arguments and proofs. -/
+/-- Collect the constants occurring in `e` (once each), skipping instance arguments and proofs. -/
 public def relevantConstants (e : Expr) : MetaM (Array Name) := foldRelevantConstants e #[] (fun n ns => return ns.push n)
 
-/-- Collect the constants occuring in `e` (once each), skipping instance arguments and proofs. -/
+/-- Collect the constants occurring in `e` (once each), skipping instance arguments and proofs. -/
 public def relevantConstantsAsSet (e : Expr) : MetaM NameSet := foldRelevantConstants e ∅ (fun n ns => return ns.insert n)
 
 end Lean.Expr

src/Lean/LibrarySuggestions/SineQuaNon.lean

@@ -105,7 +105,9 @@ builtin_initialize sineQuaNonExt : PersistentEnvExtension (NameMap (List (Name
     addImportedFn   := fun mapss _ => pure mapss
     addEntryFn      := nofun
     -- TODO: it would be nice to avoid the `toArray` here, e.g. via iterators.
-    exportEntriesFnEx := fun env _ _ => unsafe env.unsafeRunMetaM do return #[← prepareTriggers (env.constants.map₂.toArray.map (·.1))]
+    exportEntriesFnEx := fun env _ => unsafe
+      let ents := env.unsafeRunMetaM do return #[← prepareTriggers (env.constants.map₂.toArray.map (·.1))]
+      .uniform ents
     statsFn         := fun _ => "sine qua non premise selection extension"
   }
 

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
@@ -86,7 +90,9 @@ builtin_initialize symbolFrequencyExt : PersistentEnvExtension (NameMap Nat) Emp
     mkInitial       := pure ∅
     addImportedFn   := fun mapss _ => pure mapss
     addEntryFn      := nofun
-    exportEntriesFnEx := fun env _ _ => unsafe env.unsafeRunMetaM do return #[← cachedLocalSymbolFrequencyMap]
+    exportEntriesFnEx := fun env _ => unsafe
+      let ents := env.unsafeRunMetaM do return #[← cachedLocalSymbolFrequencyMap]
+      .uniform ents
     statsFn         := fun _ => "symbol frequency extension"
   }