fix: handle propositional and decidable instances in sym canonicalizer

This PR refactors instance canonicalization in the sym canonicalizer to
properly handle `Grind.nestedProof` and `Grind.nestedDecidable` markers.
Previously, the canonicalizer would report an issue when it failed to
resynthesize propositional instances that were provided by `grind`
itself or by the user via `haveI`. Now, resynthesis failure gracefully
falls back to the original instance in value positions, while remaining
strict inside types. This also removes the separate `cacheInsts` cache
in favor of the existing type/value caches via `withCaching`.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

.claude/commands/release.md

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

.github/workflows/ci.yml

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

.gitpod.yml

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

CMakeLists.txt

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

CMakePresets.json

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

doc/make/index.md

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

script/release_checklist.py

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

src/CMakeLists.txt

@@ -8,7 +8,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4 CACHE STRING "")
-set(LEAN_VERSION_MINOR 30 CACHE STRING "")
+set(LEAN_VERSION_MINOR 31 CACHE STRING "")
 set(LEAN_VERSION_PATCH 0 CACHE STRING "")
 set(LEAN_VERSION_IS_RELEASE 0 CACHE STRING "") # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
@@ -80,6 +80,7 @@ option(CCACHE "use ccache" ON)
 option(SPLIT_STACK "SPLIT_STACK" OFF)
 # When OFF we disable LLVM support
 option(LLVM "LLVM" OFF)
+option(STRIP_BINARIES "Strip produced binaries" ON)
 
 # When ON we include githash in the version string
 option(USE_GITHASH "GIT_HASH" ON)

src/Init/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/Lean/Compiler/LCNF/Check.lean

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

src/Lean/Compiler/LCNF/Main.lean

@@ -188,6 +188,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

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/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

src/Lean/DeprecatedModule.lean

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

src/Lean/Elab/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
 
@@ -512,6 +514,15 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
   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 +717,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/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?) =>

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/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/PreDefinition/WF/Unfold.lean

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

src/Lean/Elab/Quotation/Precheck.lean

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

src/Lean/Elab/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/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?) =>

src/Lean/Exception.lean

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

src/Lean/Language/Lean.lean

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

src/Lean/Level.lean

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

src/Lean/LibrarySuggestions/SymbolFrequency.lean

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

src/Lean/Message.lean

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

src/Lean/Meta.lean

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

src/Lean/Meta/AbstractNestedProofs.lean

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

src/Lean/Meta/AppBuilder.lean

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

src/Lean/Meta/HasAssignableMVar.lean

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

src/Lean/Meta/LevelDefEq.lean

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

src/Lean/Meta/Sym/Canon.lean

@@ -27,6 +27,10 @@ applications, foralls, lambdas, and let-bindings, classifying each argument as a
 implicit, or value using `shouldCanon`. Values are recursively visited but not normalized.
 Types and instances receive targeted reductions.
 
+**Note about types:** `grind` is not built for reasoning about types that are not propositions.
+We assume that definitionally equal types will be structurally identical after we apply the
+canonicalizer. We also erase most of the subsingleton markers occurring inside types.
+
 ## Reductions (applied only in type positions)
 
 - **Eta**: `fun x => f x` → `f`
@@ -39,7 +43,19 @@ Types and instances receive targeted reductions.
 
 Instances are re-synthesized via `synthInstance`. The instance type is first normalized
 using the type-level reductions above, so that `OfNat (Fin (2+1)) 0` and `OfNat (Fin 3) 0`
-produce the same canonical instance.
+produce the same canonical instance. Two special cases:
+
+- **`Decidable` instances** (`Grind.nestedDecidable`): the proposition is recursively
+  canonicalized, then the `Decidable` instance is re-synthesized. If resynthesis fails,
+  the original instance is kept (users often provide these via `haveI`).
+  A `checkDefEqInst` guard is required because structurally different `Decidable` instances
+  are not necessarily definitionally equal.
+
+- **Propositional instances** (`Grind.nestedProof`): the proposition is recursively
+  canonicalized, then the proof is re-synthesized. If resynthesis fails, the original
+  proof is kept. No definitional-equality check is needed thanks to proof irrelevance.
+
+Inside types, both cases are strict: resynthesis failure is reported as an issue.
 
 ## Two caches
 
@@ -246,23 +262,81 @@ where
     else
       withReader (fun ctx => { ctx with insideType := true }) <| canon e
 
-  canonInst (e : Expr) : CanonM Expr := do
-    if let some inst := (← get).canon.cacheInsts.get? e then
-      checkDefEqInst e inst
+  /--
+  Canonicalize `e : type` where `e` is an instance by trying to resynthesize `type`.
+  We report an issue if the instance cannot be resynthesized.
+  -/
+  canonInstCore (e : Expr) (type : Expr) : CanonM Expr := do
+    let some inst ← Sym.synthInstance? type |
+      reportIssue! "failed to canonicalize instance{indentExpr e}\nfailed to synthesize{indentExpr type}"
+      return e
+    checkDefEqInst e inst
+
+  /--
+  Canonicalize an instance by trying to resynthesize it without caching.
+  Recall that we have special support for `Decidable` and propositional instances.
+  -/
+  canonInst' (e : Expr) : CanonM Expr := do
+    /-
+    We normalize the type to make sure `OfNat (Fin (2+1)) 1` and `OfNat (Fin 3) 1` will produce
+    the same instances.
+    -/
+    let type ← inferType e
+    let type' ← canonInsideType' type
+    canonInstCore e type'
+
+  /-- `withCaching` + `canonInst'` -/
+  canonInst (e : Expr) : CanonM Expr := withCaching e do
+    canonInst' e
+
+  /--
+  Canonicalize a proposition that is also a term instance.
+  Given a term `e` of the form `@Grind.nestedProof prop h`, where `g` is the constant `Grind.nestedProof`,
+  we canonicalize it as follows:
+  1- We recursively canonicalize the proposition `prop`.
+  2- Try to resynthesize the instance, but keep the original one in case of failure since users often
+  provide them using `haveI`.
+  -/
+  canonInstProp (g : Expr) (prop : Expr) (h : Expr) (e : Expr) : CanonM Expr := withCaching e do
+    let prop' ← canon prop
+    if (← read).insideType then
+      canonInstCore h prop'
     else
       /-
-      We normalize the type to make sure `OfNat (Fin (2+1)) 1` and `OfNat (Fin 3) 1` will produce
-      the same instances.
+      **Note**: We try to resynthesize the proposition, but if it fails we keep the current one.
+      This may happen because propositional instances are often provided manually using `haveI`.
       -/
-      let type ← inferType e
-      let type' ← canonInsideType' type
-      let some inst ← Sym.synthInstance? type' |
-        reportIssue! "failed to canonicalize instance{indentExpr e}\nfailed to synthesize{indentExpr type'}"
-        return e
-      let inst ← checkDefEqInst e inst
-      -- Remark: we cache result using the type **before** canonicalization.
-      modify fun s => { s with canon.cacheInsts := s.canon.cacheInsts.insert e inst }
-      return inst
+      let h' := (← Sym.synthInstance? prop').getD h
+      /- **Note**: We don't need to check whether `h` and `h'` are definitionally equal because of proof irrelevance. -/
+      return if isSameExpr prop prop' && isSameExpr h h' then e else mkApp2 g prop' h'
+
+  /--
+  Canonicalize a decidable instance without checking the cache.
+  Given a term `e` of the form `@Grind.nestedDecidable prop inst`, where `g` is the constant `Grind.nestedDecidable`,
+  we canonicalize it as follows:
+  1- We recursively canonicalize the proposition `prop`.
+  2- Try to resynthesize the instance, but keep the original one in case of failure since users often
+  provide them using `haveI`.
+  -/
+  canonInstDec' (g : Expr) (prop : Expr) (inst : Expr) (e : Expr) : CanonM Expr := do
+    let prop' ← canon prop
+    let type := mkApp (mkConst ``Decidable) prop'
+    if (← read).insideType then
+      canonInstCore inst type
+    else
+      /-
+      **Note**: We try to resynthesize the instance, but if it fails we keep the current one.
+      We use `checkDefEqInst` here because two structurally different decidable instances are not necessarily
+      definitionally equal.
+      This may happen because propositional instances are often provided manually using `haveI`.
+      -/
+      let inst' := (← Sym.synthInstance? type).getD inst
+      let inst' ← checkDefEqInst inst inst'
+      return if isSameExpr prop prop' && isSameExpr inst inst' then e else mkApp2 g prop' inst'
+
+  /-- `withCaching` + `canonInstDec'` -/
+  canonInstDec (g : Expr) (prop : Expr) (h : Expr) (e : Expr) : CanonM Expr := withCaching e do
+    canonInstDec' g prop h e
 
   canonLambda (e : Expr) : CanonM Expr := do
     if (← read).insideType then
@@ -295,54 +369,50 @@ where
       mkLetFVars (generalizeNondepLet := false) fvars (← canon (e.instantiateRev fvars))
 
   canonAppDefault (e : Expr) : CanonM Expr := e.withApp fun f args => do
-    if f.isConstOf ``Grind.nestedProof && args.size == 2 then
-      let prop := args[0]!
-      let prop' ← canon prop
-      let e' := if isSameExpr prop prop' then e else mkAppN f (args.set! 0 prop')
-      return e'
-    else if f.isConstOf ``Grind.nestedDecidable && args.size == 2 then
-      let prop := args[0]!
-      let prop' ← canon prop
-      let e' := if isSameExpr prop prop' then e else mkAppN f (args.set! 0 prop')
-      return e'
+    if args.size == 2 then
+      if f.isConstOf ``Grind.nestedProof then
+        /- **Note**: We don't have special treatment if `e` inside a type. -/
+        let prop := args[0]!
+        let prop' ← canon prop
+        let e' := if isSameExpr prop prop' then e else mkApp2 f prop' args[1]!
+        return e'
+      else if f.isConstOf ``Grind.nestedDecidable then
+        return (← canonInstDec' f args[0]! args[1]! e)
+    let mut modified := false
+    let args ← if f.isConstOf ``OfNat.ofNat then
+      let some args ← normOfNatArgs? args | pure args
+      modified := true
+      pure args
     else
-      let mut modified := false
-      let args ← if f.isConstOf ``OfNat.ofNat then
-        let some args ← normOfNatArgs? args | pure args
+      pure args
+    let mut f := f
+    let f' ← canon f
+    unless isSameExpr f f' do
+      f := f'
+      modified := true
+    let pinfos := (← getFunInfo f).paramInfo
+    let mut args := args.toVector
+    for h : i in *...args.size do
+      let arg := args[i]
+      trace[sym.debug.canon] "[{repr (← shouldCanon pinfos i arg)}]: {arg} : {← inferType arg}"
+      let arg' ← match (← shouldCanon pinfos i arg) with
+        | .canonType =>
+          /-
+          The type may have nested propositions and terms that may need to be canonicalized too.
+          So, we must recurse over it. See issue #10232
+          -/
+          canonInsideType' arg
+        | .canonImplicit => canon arg
+        | .visit => canon arg
+        | .canonInst =>
+          match_expr arg with
+          | g@Grind.nestedDecidable prop h => canonInstDec g prop h arg
+          | g@Grind.nestedProof prop h => canonInstProp g prop h arg
+          | _ => canonInst arg
+      unless isSameExpr arg arg' do
+        args := args.set i arg'
         modified := true
-        pure args
-      else
-        pure args
-      let mut f := f
-      let f' ← canon f
-      unless isSameExpr f f' do
-        f := f'
-        modified := true
-      let pinfos := (← getFunInfo f).paramInfo
-      let mut args := args.toVector
-      for h : i in *...args.size do
-        let arg := args[i]
-        trace[sym.debug.canon] "[{repr (← shouldCanon pinfos i arg)}]: {arg} : {← inferType arg}"
-        let arg' ← match (← shouldCanon pinfos i arg) with
-          | .canonType =>
-            /-
-            The type may have nested propositions and terms that may need to be canonicalized too.
-            So, we must recurse over it. See issue #10232
-            -/
-            canonInsideType' arg
-          | .canonImplicit => canon arg
-          | .visit => canon arg
-          | .canonInst =>
-            if arg.isAppOfArity ``Grind.nestedDecidable 2 then
-              let prop := arg.appFn!.appArg!
-              let prop' ← canon prop
-              if isSameExpr prop prop' then pure arg else pure (mkApp2 arg.appFn!.appFn! prop' arg.appArg!)
-            else
-              canonInst arg
-        unless isSameExpr arg arg' do
-          args := args.set i arg'
-          modified := true
-      return if modified then mkAppN f args.toArray else e
+    return if modified then mkAppN f args.toArray else e
 
   canonIte (f : Expr) (α c inst a b : Expr) : CanonM Expr := do
     let c ← canon c
@@ -412,7 +482,7 @@ where
       return e
 
 /--
-Returns `true` if `shouldCannon pinfos i arg` is not `.visit`.
+Returns `true` if `shouldCanon pinfos i arg` is not `.visit`.
 This is a helper function used to implement mbtc.
 -/
 public def isSupport (pinfos : Array ParamInfo) (i : Nat) (arg : Expr) : MetaM Bool := do

src/Lean/Meta/Sym/Pattern.lean

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

src/Lean/Meta/Sym/SymM.lean

@@ -152,8 +152,6 @@ structure Canon.State where
   cache       : Std.HashMap Expr Expr := {}
   /-- Cache for type-level canonicalization (reductions applied). -/
   cacheInType : Std.HashMap Expr Expr := {}
-  /-- Cache mapping instances to their canonical synthesized instances. -/
-  cacheInsts  : Std.HashMap Expr Expr := {}
 
 /-- Mutable state for the symbolic computation framework. -/
 structure State where

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

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

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

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

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

@@ -12,6 +12,7 @@ public import Lean.Meta.Tactic.Simp.Arith
 public import Lean.Meta.Tactic.Simp.Attr
 public import Lean.Meta.BinderNameHint
 import Lean.Meta.WHNF
+public import Lean.Meta.HasAssignableMVar
 public section
 namespace Lean.Meta.Simp
 /--
@@ -218,6 +219,7 @@ where
     else
       let candidates := candidates.insertionSort fun e₁ e₂ => e₁.1.priority > e₂.1.priority
       for (thm, numExtraArgs) in candidates do
+        checkSystem "simp"
         if inErasedSet thm then continue
         if rflOnly then
           unless thm.rfl do
@@ -245,6 +247,7 @@ where
     else
       let candidates := candidates.insertionSort fun e₁ e₂ => e₁.priority > e₂.priority
       for thm in candidates do
+        checkSystem "simp"
         unless inErasedSet thm || (rflOnly && !thm.rfl) do
           let result? ← withNewMCtxDepth do
             let val  ← thm.getValue

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

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

src/Lean/Meta/Transform.lean

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

src/Lean/Meta/WHNF.lean

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

src/Lean/MetavarContext.lean

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

src/Lean/Parser/Command.lean

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

src/Lean/Parser/Types.lean

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

src/Lean/PrettyPrinter.lean

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

src/Lean/PrettyPrinter/Delaborator/Basic.lean

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

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -91,10 +91,9 @@ def delabSort : Delab := do
   | Level.zero => `(Prop)
   | Level.succ .zero => `(Type)
   | _ =>
-    let mvars ← getPPOption getPPMVarsLevels
     match l.dec with
-    | some l' => `(Type $(Level.quote l' (prec := max_prec) (mvars := mvars)))
-    | none    => `(Sort $(Level.quote l (prec := max_prec) (mvars := mvars)))
+    | some l' => `(Type $(← delabLevel l' (prec := max_prec)))
+    | none    => `(Sort $(← delabLevel l (prec := max_prec)))
 
 /--
 Delaborator for `const` expressions.
@@ -131,8 +130,8 @@ def delabConst : Delab := do
 
   let stx ←
     if !ls.isEmpty && (← getPPOption getPPUniverses) then
-      let mvars ← getPPOption getPPMVarsLevels
-      `($(mkIdent c).{$[$(ls.toArray.map (Level.quote · (prec := 0) (mvars := mvars)))],*})
+      let ls' ← ls.toArray.mapM fun l => delabLevel l (prec := 0)
+      `($(mkIdent c).{$ls',*})
     else
       pure <| mkIdent c
 

src/Lean/Util/PPExt.lean

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

src/Lean/Util/RecDepth.lean

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

src/Std/Internal/UV/System.lean

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

src/include/lean/lean.h

@@ -976,6 +976,13 @@ static inline void lean_sarray_set_size(u_lean_obj_arg o, size_t sz) {
 }
 static inline uint8_t* lean_sarray_cptr(lean_object * o) { return lean_to_sarray(o)->m_data; }
 
+LEAN_EXPORT bool lean_sarray_eq_cold(b_lean_obj_arg a1, b_lean_obj_arg a2);
+static inline bool lean_sarray_eq(b_lean_obj_arg a1, b_lean_obj_arg a2) {
+    assert(lean_sarray_elem_size(a1) == lean_sarray_elem_size(a2));
+    return a1 == a2 || (lean_sarray_size(a1) == lean_sarray_size(a2) && lean_sarray_eq_cold(a1, a2));
+}
+static inline uint8_t lean_sarray_dec_eq(b_lean_obj_arg a1, b_lean_obj_arg a2) { return lean_sarray_eq(a1, a2); }
+
 /* Remark: expand sarray API after we add better support in the compiler */
 
 /* ByteArray (special case of Array of Scalars) */

src/lakefile.toml.in

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

src/runtime/object.cpp

@@ -2078,6 +2078,11 @@ extern "C" LEAN_EXPORT bool lean_string_eq_cold(b_lean_obj_arg s1, b_lean_obj_ar
     return std::memcmp(lean_string_cstr(s1), lean_string_cstr(s2), lean_string_size(s1)) == 0;
 }
 
+extern "C" LEAN_EXPORT bool lean_sarray_eq_cold(b_lean_obj_arg a1, b_lean_obj_arg a2) {
+    size_t len = lean_sarray_elem_size(a1) * lean_sarray_size(a1);
+    return std::memcmp(lean_sarray_cptr(a1), lean_sarray_cptr(a2), len) == 0;
+}
+
 bool string_eq(object * s1, char const * s2) {
     if (lean_string_size(s1) != strlen(s2) + 1)
         return false;

src/runtime/uv/system.cpp

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

src/stdlib.make.in

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