feat: add extensible state mechanism for SymM

This PR add `SymExtension`, a typed extensible state mechanism for `SymM`,
following the same pattern as `Grind.SolverExtension`. Extensions are
registered at initialization time via `registerSymExtension` and provide
typed `getState`/`modifyState` accessors. Extension state persists across
`simp` invocations within a `sym =>` block and is re-initialized on each
`SymM.run`.

This enables modules (e.g., the upcoming arithmetic normalizer) to
register persistent state without modifying `Sym.State` directly.

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

.github/workflows/build-template.yml

@@ -78,7 +78,7 @@ jobs:
       # (needs to be after "Install *" to use the right shell)
       - name: CI Merge Checkout
         run: |
-          git fetch --depth=1 origin ${{ github.sha }}
+          git fetch --depth=${{ matrix.name == 'Linux Lake (Cached)' && '10' || '1' }} origin ${{ github.sha }}
           git checkout FETCH_HEAD flake.nix flake.lock script/prepare-* tests/elab/importStructure.lean
         if: github.event_name == 'pull_request'
       # (needs to be after "Checkout" so files don't get overridden)
@@ -125,7 +125,7 @@ jobs:
           else
             echo "TARGET_STAGE=stage1" >> $GITHUB_ENV
           fi
-      - name: Build
+      - name: Configure Build
         run: |
           ulimit -c unlimited  # coredumps
           [ -d build ] || mkdir build
@@ -162,7 +162,21 @@ jobs:
           fi
           # contortion to support empty OPTIONS with old macOS bash
           cmake .. --preset ${{ matrix.CMAKE_PRESET || 'release' }} -B . ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
-          time make $TARGET_STAGE -j$NPROC
+      - name: Build Stage 0 & Configure Stage 1
+        run: |
+          ulimit -c unlimited  # coredumps
+          time make -C build stage1-configure -j$NPROC
+      - name: Download Lake Cache
+        if: matrix.name == 'Linux Lake (Cached)'
+        run: |
+          cd src
+          ../build/stage0/bin/lake cache get --repo=${{ github.repository }}
+        timeout-minutes: 20 # prevent excessive hanging from network issues
+        continue-on-error: true
+      - name: Build Target Stage
+        run: |
+          ulimit -c unlimited  # coredumps
+          time make -C build $TARGET_STAGE -j$NPROC
       # Should be done as early as possible and in particular *before* "Check rebootstrap" which
       # changes the state of stage1/
       - name: Save Cache
@@ -181,6 +195,21 @@ jobs:
             build/stage1/**/*.c
             build/stage1/**/*.c.o*' || '' }}
           key: ${{ steps.restore-cache.outputs.cache-primary-key }}
+      - name: Upload Lake Cache
+        # Caching on cancellation created some mysterious issues perhaps related to improper build
+        # shutdown. Also, since this needs access to secrets, it cannot be run on forks.
+        if: matrix.name == 'Linux Lake' && !cancelled() && (github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository)
+        run: |
+          curl --version
+          cd src
+          time ../build/stage0/bin/lake build -o ../build/lake-mappings.jsonl
+          time ../build/stage0/bin/lake cache put ../build/lake-mappings.jsonl --repo=${{ github.repository }}
+        env:
+          LAKE_CACHE_KEY: ${{ secrets.LAKE_CACHE_KEY }}
+          LAKE_CACHE_ARTIFACT_ENDPOINT: ${{ vars.LAKE_CACHE_ENDPOINT }}/a1
+          LAKE_CACHE_REVISION_ENDPOINT: ${{ vars.LAKE_CACHE_ENDPOINT }}/r1
+        timeout-minutes: 20 # prevent excessive hanging from network issues
+        continue-on-error: true
       - name: Install
         run: |
           make -C build/$TARGET_STAGE install

.github/workflows/ci.yml

@@ -244,7 +244,7 @@ jobs:
                 // portable release build: use channel with older glibc (2.26)
                 "name": "Linux release",
                 // usually not a bottleneck so make exclusive to `fast-ci`
-                "os": large && fast ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
+                "os": large && fast ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "release": true,
                 // Special handling for release jobs. We want:
                 // 1. To run it in PRs so developers get PR toolchains (so secondary without tests is sufficient)
@@ -265,7 +265,7 @@ jobs:
               },
               {
                 "name": "Linux Lake",
-                "os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
+                "os": large ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "enabled": true,
                 "check-rebootstrap": level >= 1,
                 "check-stage3": level >= 2,
@@ -273,7 +273,19 @@ jobs:
                 // NOTE: `test-bench` currently seems to be broken on `ubuntu-latest`
                 "test-bench": large && level >= 2,
                 // We are not warning-free yet on all platforms, start here
-                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror",
+                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror -DUSE_LAKE_CACHE=ON",
+              },
+              {
+                "name": "Linux Lake (Cached)",
+                "os": large ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
+                "enabled": true,
+                "check-rebootstrap": level >= 1,
+                "check-stage3": level >= 2,
+                "test": true,
+                "secondary": true,
+                // NOTE: `test-bench` currently seems to be broken on `ubuntu-latest`
+                "test-bench": large && level >= 2,
+                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror -DUSE_LAKE_CACHE=ON",
               },
               {
                 "name": "Linux Reldebug",
@@ -287,7 +299,7 @@ jobs:
               {
                 "name": "Linux fsanitize",
                 // Always run on large if available, more reliable regarding timeouts
-                "os": large ? "nscloud-ubuntu-22.04-amd64-16x32-with-cache" : "ubuntu-latest",
+                "os": large ? "nscloud-ubuntu-24.04-amd64-16x32-with-cache" : "ubuntu-latest",
                 "enabled": level >= 2,
                 // do not fail nightlies on this for now
                 "secondary": level <= 2,

src/Init/Data/String/Basic.lean

@@ -852,6 +852,10 @@ theorem Slice.rawEndPos_copy {s : Slice} : s.copy.rawEndPos = s.rawEndPos := by
 theorem copy_toSlice {s : String} : s.toSlice.copy = s := by
   simp [← toByteArray_inj, Slice.toByteArray_copy, ← size_toByteArray]
 
+@[simp]
+theorem copy_comp_toSlice : String.Slice.copy ∘ String.toSlice = id := by
+  ext; simp
+
 theorem Slice.getUTF8Byte_eq_getUTF8Byte_copy {s : Slice} {p : Pos.Raw} {h : p < s.rawEndPos} :
     s.getUTF8Byte p h = s.copy.getUTF8Byte p (by simpa) := by
   simp [getUTF8Byte, String.getUTF8Byte, toByteArray_copy, ByteArray.getElem_extract]

src/Init/Data/String/Lemmas/Pattern/Split/Char.lean

@@ -23,6 +23,7 @@ import Init.Data.String.OrderInstances
 import Init.Data.String.Lemmas.Order
 import Init.Data.String.Lemmas.Intercalate
 import Init.Data.List.SplitOn.Lemmas
+import Init.Data.String.Lemmas.Slice
 
 public section
 
@@ -70,6 +71,11 @@ theorem Slice.toList_split_intercalate {c : Char} {l : List Slice} (hl : ∀ s
   · simp_all
   · rw [List.splitOn_intercalate] <;> simp_all
 
+theorem Slice.toList_split_intercalate_beq {c : Char} {l : List Slice} (hl : ∀ s ∈ l, c ∉ s.copy.toList) :
+    ((Slice.intercalate (String.singleton c) l).split c).toList ==
+      if l = [] then ["".toSlice] else l := by
+  split <;> simp_all [toList_split_intercalate hl, beq_list_iff]
+
 theorem toList_split_intercalate {c : Char} {l : List String} (hl : ∀ s ∈ l, c ∉ s.toList) :
     ((String.intercalate (String.singleton c) l).split c).toList.map (·.copy) =
       if l = [] then [""] else l := by
@@ -78,4 +84,9 @@ theorem toList_split_intercalate {c : Char} {l : List String} (hl : ∀ s ∈ l,
   · simp_all
   · rw [List.splitOn_intercalate] <;> simp_all
 
+theorem toList_split_intercalate_beq {c : Char} {l : List String} (hl : ∀ s ∈ l, c ∉ s.toList) :
+    ((String.intercalate (String.singleton c) l).split c).toList ==
+      if l = [] then ["".toSlice] else l.map String.toSlice := by
+  split <;> simp_all [toList_split_intercalate hl, Slice.beq_list_iff]
+
 end String

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

@@ -33,12 +33,23 @@ theorem beq_eq_true_iff {s t : Slice} : s == t ↔ s.copy = t.copy := by
 theorem beq_eq_false_iff {s t : Slice} : (s == t) = false ↔ s.copy ≠ t.copy := by
   simp [← Bool.not_eq_true]
 
-theorem beq_eq_decide {s t : Slice} : (s == t) = decide (s.copy = t.copy) := by
-  cases h : s == t <;> simp_all
+theorem beq_eq_decide {s t : Slice} : (s == t) = decide (s.copy = t.copy) :=
+  Bool.eq_iff_iff.2 (by simp)
 
 instance : EquivBEq String.Slice :=
   equivBEq_of_iff_apply_eq copy (by simp)
 
+theorem beq_list_iff {l l' : List String.Slice} : l == l' ↔ l.map copy = l'.map copy := by
+  induction l generalizing l' <;> cases l' <;> simp_all
+
+theorem beq_list_eq_false_iff {l l' : List String.Slice} :
+    (l == l') = false ↔ l.map copy ≠ l'.map copy := by
+  simp [← Bool.not_eq_true, beq_list_iff]
+
+theorem beq_list_eq_decide {l l' : List String.Slice} :
+    (l == l') = decide (l.map copy = l'.map copy) :=
+  Bool.eq_iff_iff.2 (by simp [beq_list_iff])
+
 end BEq
 
 end String.Slice

src/Init/Prelude.lean

@@ -4082,7 +4082,7 @@ Actions in the resulting monad are functions that take the local value as a para
 ordinary actions in `m`.
 -/
 def ReaderT (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
-  ρ → m α
+  (a : @&ρ) → m α
 
 /--
 Interpret `ρ → m α` as an element of `ReaderT ρ m α`.

src/Lean/Compiler/IR/AddExtern.lean

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

src/Lean/Compiler/LCNF/ExplicitRC.lean

@@ -97,6 +97,7 @@ partial def collectCode (code : Code .impure) : M Unit := do
     match decl.value with
     | .oproj _ parent =>
       addDerivedValue parent decl.fvarId
+    -- Keep in sync with PropagateBorrow, InferBorrow
     | .fap ``Array.getInternal args =>
       if let .fvar parent := args[1]! then
         addDerivedValue parent decl.fvarId

src/Lean/Compiler/LCNF/InferBorrow.lean

@@ -243,13 +243,19 @@ def OwnReason.isForced (reason : OwnReason) : Bool :=
   -- All of these reasons propagate through ABI decisions and can thus safely be ignored as they
   -- will be accounted for by the reference counting pass.
   | .constructorArg .. | .functionCallArg .. | .fvarCall .. | .partialApplication ..
-  | .jpArgPropagation .. => false
+  | .jpArgPropagation ..
+  -- forward propagation can never affect a user-annotated parameter
+  | .forwardProjectionProp ..
+  -- backward propagation on a user-annotated parameter is only necessary if the projected value
+  -- directly flows into a reset-reuse. However, the borrow annotation propagator ensures this
+  -- situation never arises
+  | .backwardProjectionProp .. => false
   -- Results of functions and constructors are naturally owned.
   | .constructorResult .. | .functionCallResult ..
   -- We cannot pass borrowed values to reset or have borrow annotations destroy tail calls for
   -- correctness reasons.
-  | .resetReuse .. | .tailCallPreservation .. | .jpTailCallPreservation .. | .ownedAnnotation
-  | .forwardProjectionProp .. | .backwardProjectionProp .. => true
+  | .resetReuse .. | .tailCallPreservation .. | .jpTailCallPreservation ..
+  | .ownedAnnotation => true
 
 /--
 Infer the borrowing annotations in a SCC through dataflow analysis.
@@ -373,6 +379,16 @@ where
     | .oproj _ x _ =>
       if ← isOwned x then ownFVar z (.forwardProjectionProp z)
       if ← isOwned z then ownFVar x (.backwardProjectionProp z)
+    -- Keep in sync with ExplicitRC, PropagateBorrow
+    | .fap ``Array.getInternal args =>
+      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[2]! then
+        if ← isOwned parent then ownFVar z (.forwardProjectionProp z)
+    | .fap ``Array.uget args =>
+      if let .fvar parent := args[1]! then
+        if ← isOwned parent then ownFVar z (.forwardProjectionProp z)
     | .fap f args =>
       let ps ← getParamInfo (.decl f)
       ownFVar z (.functionCallResult z)

src/Lean/Compiler/LCNF/PropagateBorrow.lean

@@ -105,9 +105,22 @@ where
 
   collectLetValue (z : FVarId) (v : LetValue .impure) : InferM Unit := do
     match v with
-    | .oproj _ x _ =>
-      let xVal ← getOwnedness x
-      join z xVal
+    | .oproj _ parent _ =>
+      let parentVal ← getOwnedness parent
+      join z parentVal
+    -- Keep in sync with ExplicitRC, InferBorrow
+    | .fap ``Array.getInternal args =>
+      if let .fvar parent := args[1]! then
+        let parentVal ← getOwnedness parent
+        join z parentVal
+    | .fap ``Array.get!Internal args =>
+      if let .fvar parent := args[2]! then
+        let parentVal ← getOwnedness parent
+        join z parentVal
+    | .fap ``Array.uget args =>
+      if let .fvar parent := args[1]! then
+        let parentVal ← getOwnedness parent
+        join z parentVal
     | .ctor .. | .fap .. | .fvar .. | .pap .. | .sproj .. | .uproj .. | .erased .. | .lit .. =>
       join z .own
     | _ => unreachable!

src/Lean/CoreM.lean

@@ -343,13 +343,13 @@ def instantiateTypeLevelParams (c : ConstantVal) (us : List Level) : CoreM Expr
   modifyInstLevelTypeCache fun s => s.insert c.name (us, r)
   return r
 
-def instantiateValueLevelParams (c : ConstantInfo) (us : List Level) : CoreM Expr := do
+def instantiateValueLevelParams (c : ConstantInfo) (us : List Level) (allowOpaque := false) : CoreM Expr := do
   if let some (us', r) := (← get).cache.instLevelValue.find? c.name then
     if us == us' then
       return r
-  unless c.hasValue do
+  unless c.hasValue (allowOpaque := allowOpaque) do
     throwError "Not a definition or theorem: {.ofConstName c.name}"
-  let r := c.instantiateValueLevelParams! us
+  let r := c.instantiateValueLevelParams! us (allowOpaque := allowOpaque)
   modifyInstLevelValueCache fun s => s.insert c.name (us, r)
   return r
 

src/Lean/Declaration.lean

@@ -14,29 +14,35 @@ public section
 
 namespace Lean
 /--
-Reducibility hints are used in the convertibility checker.
-When trying to solve a constraint such a
+Reducibility hints guide the kernel's *lazy delta reduction* strategy. When the kernel encounters a
+definitional equality constraint
 
            (f ...) =?= (g ...)
 
-where f and g are definitions, the checker has to decide which one will be unfolded.
-  If      f (g) is opaque,     then g (f) is unfolded if it is also not marked as opaque,
-  Else if f (g) is abbrev,     then f (g) is unfolded if g (f) is also not marked as abbrev,
-  Else if f and g are regular, then we unfold the one with the biggest definitional height.
-  Otherwise both are unfolded.
+where `f` and `g` are definitions, it must decide which side to unfold. The rules (implemented in
+`lazy_delta_reduction_step` in `src/kernel/type_checker.cpp`) are:
 
-The arguments of the `regular` Constructor are: the definitional height and the flag `selfOpt`.
+* If `f` and `g` have the **same hint kind**:
+  - Both `.opaque` or both `.abbrev`: unfold both.
+  - Both `.regular`: unfold the one with the **greater** height first. If their heights are equal
+    (in particular, if `f` and `g` are the same definition), first try to compare their arguments
+    for definitional equality (short-circuiting the unfolding if they match), then unfold both.
+* If `f` and `g` have **different hint kinds**: unfold the one that is *not* `.opaque`, preferring to
+  unfold `.abbrev` over `.regular`.
 
-The definitional height is by default computed by the kernel. It only takes into account
-other regular definitions used in a definition. When creating declarations using meta-programming,
-we can specify the definitional depth manually.
+The `.regular` constructor carries a `UInt32` *definitional height*, which is computed by the
+elaborator as one plus the maximum height of all `.regular` constants appearing in the definition's
+body (see `getMaxHeight`). This means `.abbrev` and `.opaque` constants do not contribute to the
+height. When creating declarations via meta-programming, the height can be specified manually.
 
-Remark: the hint only affects performance. None of the hints prevent the kernel from unfolding a
-declaration during Type checking.
+The hints only affect performance — they control the order in which definitions are unfolded, but
+never prevent the kernel from unfolding a definition during type checking.
 
-Remark: the ReducibilityHints are not related to the attributes: reducible/irrelevance/semireducible.
-These attributes are used by the Elaborator. The ReducibilityHints are used by the kernel (and Elaborator).
-Moreover, the ReducibilityHints cannot be changed after a declaration is added to the kernel. -/
+The `ReducibilityHints` are not related to the `@[reducible]`/`@[irreducible]`/`@[semireducible]`
+attributes. Those attributes are used by the elaborator to control which definitions tactics like
+`simp`, `rfl`, and `dsimp` will unfold; they do not affect the kernel. Conversely,
+`ReducibilityHints` are set when a declaration is added to the kernel and cannot be changed
+afterwards. -/
 inductive ReducibilityHints where
   | opaque  : ReducibilityHints
   | abbrev  : ReducibilityHints
@@ -469,24 +475,37 @@ def numLevelParams (d : ConstantInfo) : Nat :=
 def type (d : ConstantInfo) : Expr :=
   d.toConstantVal.type
 
+/--
+Returns the value of a definition. With `allowOpaque := true`, values
+of theorems and opaque declarations are also returned.
+-/
 def value? (info : ConstantInfo) (allowOpaque := false) : Option Expr :=
   match info with
   | .defnInfo {value, ..}   => some value
-  | .thmInfo  {value, ..}   => some value
+  | .thmInfo  {value, ..}   => if allowOpaque then some value else none
   | .opaqueInfo {value, ..} => if allowOpaque then some value else none
   | _                       => none
 
+/--
+Returns `true` if this declaration as a value for the purpose of reduction
+and type-checking, i.e. is a definition.
+With `allowOpaque := true`, theorems and opaque declarations are also considered to have values.
+-/
 def hasValue (info : ConstantInfo) (allowOpaque := false) : Bool :=
   match info with
   | .defnInfo _   => true
-  | .thmInfo  _   => true
+  | .thmInfo  _   => allowOpaque
   | .opaqueInfo _ => allowOpaque
   | _             => false
 
+/--
+Returns the value of a definition. With `allowOpaque := true`, values
+of theorems and opaque declarations are also returned.
+-/
 def value! (info : ConstantInfo) (allowOpaque := false) : Expr :=
   match info with
   | .defnInfo {value, ..}   => value
-  | .thmInfo  {value, ..}   => value
+  | .thmInfo  {value, ..}   => if allowOpaque then value else panic! "declaration with value expected"
   | .opaqueInfo {value, ..} => if allowOpaque then value else panic! "declaration with value expected"
   | _                       => panic! s!"declaration with value expected, but {info.name} has none"
 
@@ -510,6 +529,10 @@ def isDefinition : ConstantInfo → Bool
   | .defnInfo _ => true
   | _           => false
 
+def isTheorem : ConstantInfo → Bool
+  | .thmInfo _ => true
+  | _          => false
+
 def inductiveVal! : ConstantInfo → InductiveVal
   | .inductInfo val => val
   | _ => panic! "Expected a `ConstantInfo.inductInfo`."

src/Lean/DefEqAttrib.lean

@@ -101,7 +101,7 @@ def inferDefEqAttr (declName : Name) : MetaM Unit := do
   withoutExporting do
     let info ← getConstInfo declName
     let isRfl ←
-      if let some value := info.value? then
+      if let some value := info.value? (allowOpaque := true) then
         isRflProofCore info.type value
       else
         pure false

src/Lean/Elab/BuiltinTerm.lean

@@ -315,9 +315,16 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
   | _ => panic! "resolveId? returned an unexpected expression"
 
 @[builtin_term_elab Lean.Parser.Term.inferInstanceAs] def elabInferInstanceAs : TermElab := fun stx expectedType? => do
-  let expectedType ← tryPostponeIfHasMVars expectedType? "`inferInstanceAs` failed"
   -- The type argument is the last child (works for both `inferInstanceAs T` and `inferInstanceAs <| T`)
   let typeStx := stx[stx.getNumArgs - 1]!
+  if !backward.inferInstanceAs.wrap.get (← getOptions) then
+    return (← elabTerm (← `(_root_.inferInstanceAs $(⟨typeStx⟩))) expectedType?)
+
+  let some expectedType ← tryPostponeIfHasMVars? expectedType? |
+    throwError (m!"`inferInstanceAs` failed, expected type contains metavariables{indentD expectedType?}" ++
+      .note "`inferInstanceAs` requires full knowledge of the expected (\"target\") type to do its \
+        instance translation. If you do not intend to transport instances between two types, \
+        consider using `inferInstance` or `(inferInstance : expectedType)` instead.")
   let type ← withSynthesize (postpone := .yes) <| elabType typeStx
   -- Unify with expected type to resolve metavariables (e.g., `_` placeholders)
   discard <| isDefEq type expectedType
@@ -329,7 +336,7 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
   let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
     -- Normalize to instance normal form.
     let logCompileErrors := !(← read).isNoncomputableSection && !(← read).declName?.any (Lean.isNoncomputable (← getEnv))
-    let isMeta := (← read).isMetaSection
+    let isMeta := (← read).declName?.any (isMarkedMeta (← getEnv))
     withNewMCtxDepth <| normalizeInstance inst expectedType (logCompileErrors := logCompileErrors) (isMeta := isMeta)
   else
     pure inst

src/Lean/Elab/Deriving/Basic.lean

@@ -220,7 +220,7 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
             instName ← liftMacroM <| mkUnusedBaseName instName
             if isPrivateName declName then
               instName := mkPrivateName env instName
-            let isMeta := (← read).isMetaSection
+            let isMeta := (← read).declName?.any (isMarkedMeta (← getEnv))
             let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
               withDeclNameForAuxNaming instName <| withNewMCtxDepth <|
                 normalizeInstance result.instVal result.instType

src/Lean/Elab/PreDefinition/Mutual.lean

@@ -63,10 +63,11 @@ def addPreDefAttributes (preDefs : Array PreDefinition) : TermElabM Unit := do
   a wrong setting and creates bad `defEq` equations.
   -/
   for preDef in preDefs do
-    unless preDef.modifiers.attrs.any fun a =>
-        a.name = `reducible || a.name = `semireducible ||
-        a.name = `instance_reducible || a.name = `implicit_reducible do
-      setIrreducibleAttribute preDef.declName
+    unless preDef.kind.isTheorem do
+      unless preDef.modifiers.attrs.any fun a =>
+          a.name = `reducible || a.name = `semireducible ||
+          a.name = `instance_reducible || a.name = `implicit_reducible do
+        setIrreducibleAttribute preDef.declName
 
   /-
   `enableRealizationsForConst` must happen before `generateEagerEqns`

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

@@ -184,6 +184,7 @@ def getUnfoldFor? (declName : Name) : MetaM (Option Name) := do
   else
     return none
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_get_structural_rec_arg_pos]
 def getStructuralRecArgPosImp? (declName : Name) : CoreM (Option Nat) := do
   let some info := eqnInfoExt.find? (← getEnv) declName | return none

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

@@ -80,6 +80,32 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (fixedParamPerms
       withRecFunsAsAxioms preDefs do
         mkBRecOnF recArgInfos positions r values[idx]! FTypes[idx]!
   trace[Elab.definition.structural] "FArgs: {FArgs}"
+
+  -- Extract the functionals into named `_f` helper definitions (e.g. `foo._f`) so they show up
+  -- with a helpful name in kernel diagnostics. The `_f` definitions are `.abbrev` so the kernel
+  -- unfolds them eagerly; their body heights are registered via `setDefHeightOverride` so that
+  -- `getMaxHeight` computes the correct height for parent definitions.
+  -- For inductive predicates, the previous inline behavior is kept.
+  let FArgs ←
+    if isIndPred then
+      pure FArgs
+    else
+      let us := preDefs[0]!.levelParams.map mkLevelParam
+      FArgs.mapIdxM fun idx fArg => do
+        let fName := preDefs[idx]!.declName ++ `_f
+        let fValue ← eraseRecAppSyntaxExpr (← mkLambdaFVars xs fArg)
+        let fType ← Meta.letToHave (← inferType fValue)
+        let fHeight := getMaxHeight (← getEnv) fValue
+        addDecl (.defnDecl {
+          name := fName, levelParams := preDefs[idx]!.levelParams,
+          type := fType, value := fValue,
+          hints := .abbrev,
+          safety := if preDefs[idx]!.modifiers.isUnsafe then .unsafe else .safe,
+          all := [fName] })
+        modifyEnv (setDefHeightOverride · fName fHeight)
+        setReducibleAttribute fName
+        return mkAppN (mkConst fName us) xs
+
   let brecOn := brecOnConst 0
   -- the indices and the major premise are not mentioned in the minor premises
   -- so using `default` is fine here

src/Lean/Elab/Tactic/Try.lean

@@ -787,6 +787,7 @@ where
           throw ex
 
 -- `evalSuggest` implementation
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_eval_suggest_tactic]
 private partial def evalSuggestImpl : TryTactic := fun tac => do
   trace[try.debug] "{tac}"

src/Lean/Environment.lean

@@ -1193,8 +1193,8 @@ namespace ConstantInfo
 def instantiateTypeLevelParams (c : ConstantInfo) (ls : List Level) : Expr :=
   c.toConstantVal.instantiateTypeLevelParams ls
 
-def instantiateValueLevelParams! (c : ConstantInfo) (ls : List Level) : Expr :=
-  c.value!.instantiateLevelParams c.levelParams ls
+def instantiateValueLevelParams! (c : ConstantInfo) (ls : List Level) (allowOpaque := false) : Expr :=
+  (c.value! (allowOpaque := allowOpaque)).instantiateLevelParams c.levelParams ls
 
 end ConstantInfo
 
@@ -2755,13 +2755,28 @@ def mkThmOrUnsafeDef [Monad m] [MonadEnv m] (thm : TheoremVal) : m Declaration :
   else
     return .thmDecl thm
 
+/-- Environment extension for overriding the height that `getMaxHeight` assigns to a definition.
+This is consulted for all definitions regardless of their reducibility hints. Currently used by
+structural recursion to ensure that parent definitions get the correct height even though the
+`_f` helper definitions are marked as `.abbrev` (which `getMaxHeight` would otherwise ignore). -/
+builtin_initialize defHeightOverrideExt : EnvExtension (NameMap UInt32) ←
+  registerEnvExtension (pure {}) (asyncMode := .local)
+
+/-- Register a height override for a definition so that `getMaxHeight` uses it. -/
+def setDefHeightOverride (env : Environment) (declName : Name) (height : UInt32) : Environment :=
+  defHeightOverrideExt.modifyState env fun m => m.insert declName height
+
 def getMaxHeight (env : Environment) (e : Expr) : UInt32 :=
+  let overrides := defHeightOverrideExt.getState env
   e.foldConsts 0 fun constName max =>
-    match env.findAsync? constName with
-    | some { kind := .defn, constInfo := info, .. } =>
-      match info.get.hints with
-      | ReducibilityHints.regular h => if h > max then h else max
-      | _                           => max
-    | _ => max
+    match overrides.find? constName with
+    | some h => if h > max then h else max
+    | none =>
+      match env.findAsync? constName with
+      | some { kind := .defn, constInfo := info, .. } =>
+        match info.get.hints with
+        | ReducibilityHints.regular h => if h > max then h else max
+        | _                           => max
+      | _ => max
 
 end Lean

src/Lean/Meta/Basic.lean

@@ -1321,7 +1321,7 @@ private def getDefInfoTemp (info : ConstantInfo) : MetaM (Option ConstantInfo) :
    `constName` is an instance. This difference should be irrelevant for `isClassQuickConst?`. -/
 private def getConstTemp? (constName : Name) : MetaM (Option ConstantInfo) := do
   match (← getEnv).find? constName with
-  | some (info@(ConstantInfo.thmInfo _))  => getTheoremInfo info
+  | some (ConstantInfo.thmInfo _)          => return none
   | some (info@(ConstantInfo.defnInfo _)) => getDefInfoTemp info
   | some info                             => pure (some info)
   | none                                  => throwUnknownConstantAt (← getRef) constName

src/Lean/Meta/ExprDefEq.lean

@@ -1126,6 +1126,7 @@ def checkAssignment (mvarId : MVarId) (fvars : Array Expr) (v : Expr) : MetaM (O
       return none
     return some v
 
+set_option compiler.ignoreBorrowAnnotation true in
 -- Implementation for `_root_.Lean.MVarId.checkedAssign`
 @[export lean_checked_assign]
 def checkedAssignImpl (mvarId : MVarId) (val : Expr) : MetaM Bool := do
@@ -2233,6 +2234,7 @@ private def whnfCoreAtDefEq (e : Expr) : MetaM Expr := do
   else
     whnfCore e
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_is_expr_def_eq]
 partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecDepth do
   withTraceNodeBefore `Meta.isDefEq (fun _ => return m!"{t} =?= {s}") do

src/Lean/Meta/GetUnfoldableConst.lean

@@ -46,11 +46,7 @@ External users wanting to look up names should be using `Lean.getConstInfo`.
 def getUnfoldableConst? (constName : Name) : MetaM (Option ConstantInfo) := do
   let some ainfo := (← getEnv).findAsync? constName | throwUnknownConstantAt (← getRef) constName
   match ainfo.kind with
-  | .thm =>
-    if (← shouldReduceAll) then
-      return some ainfo.toConstantInfo
-    else
-      return none
+  | .thm => return none
   | .defn => if (← canUnfold ainfo.toConstantInfo) then return ainfo.toConstantInfo else return none
   | _ => return none
 
@@ -59,7 +55,7 @@ As with `getUnfoldableConst?` but return `none` instead of failing if the consta
 -/
 def getUnfoldableConstNoEx? (constName : Name) : MetaM (Option ConstantInfo) := do
   match (← getEnv).find? constName with
-  | some (info@(.thmInfo _))  => getTheoremInfo info
+  | some (.thmInfo _)          => return none
   | some (info@(.defnInfo _)) => if (← canUnfold info) then return info else return none
   | some (.axiomInfo _)       => recordUnfoldAxiom constName; return none
   | _                         => return none

src/Lean/Meta/InferType.lean

@@ -206,6 +206,7 @@ because it overrides unrelated configurations.
     else
       withConfig (fun cfg => { cfg with beta := true, iota := true, zeta := true, zetaHave := true, zetaDelta := true, proj := .yesWithDelta, etaStruct := .all }) x
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_infer_type]
 def inferTypeImp (e : Expr) : MetaM Expr :=
   let rec infer (e : Expr) :  MetaM Expr := do

src/Lean/Meta/LevelDefEq.lean

@@ -85,6 +85,7 @@ private def isMVarWithGreaterDepth (v : Level) (mvarId : LMVarId) : MetaM Bool :
   | Level.mvar mvarId' => return (← mvarId'.getLevel) > (← mvarId.getLevel)
   | _ => return false
 
+set_option compiler.ignoreBorrowAnnotation true in
 mutual
 
   private partial def solve (u v : Level) : MetaM LBool := do

src/Lean/Meta/Match/MatchEqs.lean

@@ -138,6 +138,7 @@ Creates conditional equations and splitter for the given match auxiliary declara
 
 See also `getEquationsFor`.
 -/
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_get_match_equations_for]
 def getEquationsForImpl (matchDeclName : Name) : MetaM MatchEqns := do
   /-
@@ -246,6 +247,7 @@ where go baseName splitterName := withConfig (fun c => { c with etaStruct := .no
     let result := { eqnNames, splitterName, splitterMatchInfo }
     registerMatchEqns matchDeclName result
 
+set_option compiler.ignoreBorrowAnnotation true in
 /--
 Generate the congruence equations for the given match auxiliary declaration.
 The congruence equations have a completely unrestricted left-hand side (arbitrary discriminants),

src/Lean/Meta/Sym/Pattern.lean

@@ -785,6 +785,7 @@ def isDefEqApp (tFn : Expr) (t : Expr) (s : Expr) (_ : tFn = t.getAppFn) : DefEq
   let numArgs := t.getAppNumArgs
   isDefEqAppWithInfo t s (numArgs - 1) info
 
+set_option compiler.ignoreBorrowAnnotation true in
 /--
 `isDefEqMain` implementation.
 -/

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

@@ -40,6 +40,7 @@ abbrev cacheResult (e : Expr) (r : Result) : SimpM Result := do
     modify fun s => { s with persistentCache := s.persistentCache.insert { expr := e } r }
   return r
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_sym_simp]
 def simpImpl (e₁ : Expr) : SimpM Result := withIncRecDepth do
   let numSteps := (← get).numSteps

src/Lean/Meta/Sym/SymM.lean

@@ -15,6 +15,48 @@ register_builtin_option sym.debug : Bool := {
   descr    := "check invariants"
 }
 
+/-!
+## Sym Extensions
+
+Extensible state mechanism for `SymM`, allowing modules to register persistent state
+that lives across `simp` invocations within a `sym =>` block. Follows the same pattern
+as `Grind.SolverExtension` in `Lean/Meta/Tactic/Grind/Types.lean`.
+-/
+
+/-- Opaque extension state type used to store type-erased extension values. -/
+opaque SymExtensionStateSpec : (α : Type) × Inhabited α := ⟨Unit, ⟨()⟩⟩
+@[expose] def SymExtensionState : Type := SymExtensionStateSpec.fst
+instance : Inhabited SymExtensionState := SymExtensionStateSpec.snd
+
+/--
+A registered extension for `SymM`. Each extension gets a unique index into the
+extensions array in `Sym.State`. Can only be created via `registerSymExtension`.
+-/
+structure SymExtension (σ : Type) where private mk ::
+  id        : Nat
+  mkInitial : IO σ
+  deriving Inhabited
+
+private builtin_initialize symExtensionsRef : IO.Ref (Array (SymExtension SymExtensionState)) ← IO.mkRef #[]
+
+/--
+Registers a new `SymM` state extension. Extensions can only be registered during initialization.
+Returns a handle for typed access to the extension's state.
+-/
+def registerSymExtension {σ : Type} (mkInitial : IO σ) : IO (SymExtension σ) := do
+  unless (← initializing) do
+    throw (IO.userError "failed to register `Sym` extension, extensions can only be registered during initialization")
+  let exts ← symExtensionsRef.get
+  let id := exts.size
+  let ext : SymExtension σ := { id, mkInitial }
+  symExtensionsRef.modify fun exts => exts.push (unsafe unsafeCast ext)
+  return ext
+
+/-- Returns initial state for all registered extensions. -/
+def SymExtensions.mkInitialStates : IO (Array SymExtensionState) := do
+  let exts ← symExtensionsRef.get
+  exts.mapM fun ext => ext.mkInitial
+
 /--
 Information about a single argument position in a function's type signature.
 
@@ -133,6 +175,8 @@ structure State where
   congrInfo : PHashMap ExprPtr CongrInfo := {}
   /-- Cache for `isDefEqI` results -/
   defEqI : PHashMap (ExprPtr × ExprPtr) Bool := {}
+  /-- State for registered `SymExtension`s, indexed by extension id. -/
+  extensions : Array SymExtensionState := #[]
   debug : Bool := false
 
 abbrev SymM := ReaderT Context <| StateRefT State MetaM
@@ -150,7 +194,8 @@ private def mkSharedExprs : AlphaShareCommonM SharedExprs := do
 def SymM.run (x : SymM α) : MetaM α := do
   let (sharedExprs, share) := mkSharedExprs |>.run {}
   let debug := sym.debug.get (← getOptions)
-  x { sharedExprs } |>.run' { debug, share }
+  let extensions ← SymExtensions.mkInitialStates
+  x { sharedExprs } |>.run' { debug, share, extensions }
 
 /-- Returns maximally shared commonly used terms -/
 def getSharedExprs : SymM SharedExprs :=
@@ -230,4 +275,26 @@ def isDefEqI (s t : Expr) : SymM Bool := do
   modify fun s => { s with defEqI := s.defEqI.insert key result }
   return result
 
+instance : Inhabited (SymM α) where
+  default := throwError "<SymM default value>"
+
+/-! ### SymExtension accessors -/
+
+private unsafe def SymExtension.getStateCoreImpl (ext : SymExtension σ) (extensions : Array SymExtensionState) : IO σ :=
+  return unsafeCast extensions[ext.id]!
+
+@[implemented_by SymExtension.getStateCoreImpl]
+opaque SymExtension.getStateCore (ext : SymExtension σ) (extensions : Array SymExtensionState) : IO σ
+
+def SymExtension.getState (ext : SymExtension σ) : SymM σ := do
+  ext.getStateCore (← get).extensions
+
+private unsafe def SymExtension.modifyStateImpl (ext : SymExtension σ) (f : σ → σ) : SymM Unit := do
+  modify fun s => { s with
+    extensions := s.extensions.modify ext.id fun state => unsafeCast (f (unsafeCast state))
+  }
+
+@[implemented_by SymExtension.modifyStateImpl]
+opaque SymExtension.modifyState (ext : SymExtension σ) (f : σ → σ) : SymM Unit
+
 end Lean.Meta.Sym

src/Lean/Meta/SynthInstance.lean

@@ -944,6 +944,7 @@ def synthInstance (type : Expr) (maxResultSize? : Option Nat := none) : MetaM Ex
       | none        => throwFailedToSynthesize type)
     (fun _ => throwFailedToSynthesize type)
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_synth_pending]
 private def synthPendingImp (mvarId : MVarId) : MetaM Bool := withIncRecDepth <| mvarId.withContext do
   let mvarDecl ← mvarId.getDecl

src/Lean/Meta/Tactic/Delta.lean

@@ -10,18 +10,18 @@ import Lean.Meta.Transform
 public section
 namespace Lean.Meta
 
-def delta? (e : Expr) (p : Name → Bool := fun _ => true) : CoreM (Option Expr) :=
+def delta? (e : Expr) (p : Name → Bool := fun _ => true) (allowOpaque := false) : CoreM (Option Expr) :=
   matchConst e.getAppFn (fun _ => return none) fun fInfo fLvls => do
-    if p fInfo.name && fInfo.hasValue && fInfo.levelParams.length == fLvls.length then
-      let f ← instantiateValueLevelParams fInfo fLvls
+    if p fInfo.name && fInfo.hasValue (allowOpaque := allowOpaque) && fInfo.levelParams.length == fLvls.length then
+      let f ← instantiateValueLevelParams fInfo fLvls (allowOpaque := allowOpaque)
       return some (f.betaRev e.getAppRevArgs (useZeta := true))
     else
       return none
 
 /-- Low-level delta expansion. It is used to implement equation lemmas and elimination principles for recursive definitions. -/
-def deltaExpand (e : Expr) (p : Name → Bool) : CoreM Expr :=
+def deltaExpand (e : Expr) (p : Name → Bool) (allowOpaque := false) : CoreM Expr :=
   Core.transform e fun e => do
-    match (← delta? e p) with
+    match (← delta? e p (allowOpaque := allowOpaque)) with
     | some e' => return .visit e'
     | none    => return .continue
 

src/Lean/Meta/Tactic/FunInd.lean

@@ -347,11 +347,13 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
 
     if e.getAppArgs.any (·.isFVarOf oldIH) then
       -- Sometimes Fix.lean abstracts over oldIH in a proof definition.
-      -- So beta-reduce that definition. We need to look through theorems here!
-      if let some e' ← withTransparency .all do unfoldDefinition? e then
-        return ← foldAndCollect oldIH newIH isRecCall e'
-      else
-        throwError "Internal error in `foldAndCollect`: Cannot reduce application of `{e.getAppFn}` in:{indentExpr e}"
+      -- So delta-beta-reduce that definition. We need to look through theorems here!
+      if let .const declName lvls := e.getAppFn then
+        if let some cinfo := (← getEnv).find? declName then
+          if let some val := cinfo.value? (allowOpaque := true) then
+            let e' := (val.instantiateLevelParams cinfo.levelParams lvls).betaRev e.getAppRevArgs
+            return ← foldAndCollect oldIH newIH isRecCall e'
+      throwError "Internal error in `foldAndCollect`: Cannot reduce application of `{e.getAppFn}` in:{indentExpr e}"
 
     match e with
     | .app e1 e2 =>
@@ -742,6 +744,13 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
         let b' ← buildInductionBody toErase toClear goal' oldIH newIH isRecCall (b.instantiate1 x)
         mkLambdaFVars #[x] b'
 
+  -- Unfold constant applications that take `oldIH` as an argument (e.g. `_f` auxiliary
+  -- definitions from structural recursion), so that we can see their body structure.
+  -- Similar to the case in `foldAndCollect`.
+  if e.getAppFn.isConst && e.getAppArgs.any (·.isFVarOf oldIH) then
+    if let some e' ← withTransparency .all (unfoldDefinition? e) then
+      return ← buildInductionBody toErase toClear goal oldIH newIH isRecCall e'
+
   liftM <| buildInductionCase oldIH newIH isRecCall toErase toClear goal e
 
 /--

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean

@@ -276,6 +276,7 @@ private def propagateNonlinearPow (x : Var) : GoalM Bool := do
   c'.assert
   return true
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_cutsat_propagate_nonlinear]
 def propagateNonlinearTermImpl (y : Var) (x : Var) : GoalM Bool := do
   unless (← isVarEqConst? y).isSome do return false
@@ -338,6 +339,7 @@ partial def _root_.Int.Linear.Poly.updateOccsForElimEq (p : Poly) (x : Var) : Go
     go p
   go p
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_cutsat_assert_eq]
 def EqCnstr.assertImpl (c : EqCnstr) : GoalM Unit := do
   if (← inconsistent) then return ()

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean

@@ -99,6 +99,7 @@ where
         return some { p := c.p.addConst 1, h := .ofLeDiseq c c' }
     return none
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_cutsat_assert_le]
 def LeCnstr.assertImpl (c : LeCnstr) : GoalM Unit := do
   if (← inconsistent) then return ()

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean

@@ -325,7 +325,9 @@ private def mkPowEqProof (ka : Int) (ca? : Option EqCnstr) (kb : Nat) (cb? : Opt
   let h := mkApp8 (mkConst ``Int.Linear.pow_eq) a b (toExpr ka) (toExpr kbInt) (toExpr k) h₁ h₂ eagerReflBoolTrue
   return mkApp6 (mkConst ``Int.Linear.of_var_eq) (← getContext) (← mkVarDecl x) (toExpr k) (← mkPolyDecl c'.p) eagerReflBoolTrue h
 
+set_option compiler.ignoreBorrowAnnotation true in
 mutual
+
 @[export lean_cutsat_eq_cnstr_to_proof]
 private partial def EqCnstr.toExprProofImpl (c' : EqCnstr) : ProofM Expr := caching c' do
   trace[grind.debug.lia.proof] "{← c'.pp}"

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean

@@ -64,6 +64,7 @@ where
         registerNonlinearOcc e x
     | _ => registerNonlinearOcc e x
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_cutsat_mk_var]
 def mkVarImpl (expr : Expr) : GoalM Var := do
   if let some var := (← get').varMap.find? { expr } then

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

@@ -239,6 +239,7 @@ private def normOfNatArgs? (args : Array Expr) : MetaM (Option (Array Expr)) :=
       return some args.toArray
   return none
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_canon]
 partial def canonImpl (e : Expr) : GoalM Expr := do profileitM Exception "grind canon" (← getOptions) do
   trace_goal[grind.debug.canon] "{e}"

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

@@ -348,6 +348,7 @@ where
       internalize rhs generation p
       addEqCore lhs rhs proof isHEq
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_process_new_facts]
 private def processNewFactsImpl : GoalM Unit := do
   repeat

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

@@ -535,6 +535,7 @@ private def internalizeOfNatFinBitVecLiteral (e : Expr) (generation : Nat) (pare
   updateIndicesFound (.const ``OfNat.ofNat)
   activateTheorems ``OfNat.ofNat generation
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_internalize]
 private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Unit := withIncRecDepth do
   if (← alreadyInternalized e) then

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

@@ -328,6 +328,7 @@ mutual
 
 end
 
+set_option compiler.ignoreBorrowAnnotation true in
 /--
 Returns a proof that `a = b`.
 It assumes `a` and `b` are in the same equivalence class.
@@ -338,6 +339,7 @@ def mkEqProofImpl (a b : Expr) : GoalM Expr := do
     throwError "internal `grind` error, `mkEqProof` invoked with terms of different types{indentExpr a}\nhas type{indentExpr (← inferType a)}\nbut{indentExpr b}\nhas type{indentExpr (← inferType b)}"
   mkEqProofCore a b (heq := false)
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_mk_heq_proof]
 def mkHEqProofImpl (a b : Expr) : GoalM Expr :=
   mkEqProofCore a b (heq := true)

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

@@ -42,6 +42,7 @@ def dsimpCore (e : Expr) : GrindM Expr := do profileitM Exception "grind dsimp"
   modify fun s => { s with simp }
   return r
 
+set_option compiler.ignoreBorrowAnnotation true in
 /--
 Preprocesses `e` using `grind` normalization theorems and simprocs,
 and then applies several other preprocessing steps.

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

@@ -202,6 +202,7 @@ protected def getSimpContext (config : Grind.Config) : MetaM Simp.Context := do
     (simpTheorems := #[thms])
     (congrTheorems := (← getSimpCongrTheorems))
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_normalize]
 def normalizeImp (e : Expr) (config : Grind.Config) : MetaM Expr := do
   let (r, _) ← Meta.simp e (← Grind.getSimpContext config) (← Grind.getSimprocs)

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

@@ -512,6 +512,7 @@ Auxiliary `dsimproc` for not visiting `Char` literal subterms.
 -/
 private def doNotVisitCharLit : DSimproc := doNotVisit isCharLit ``Char.ofNat
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_dsimp]
 private partial def dsimpImpl (e : Expr) : SimpM Expr := do
   let cfg ← getConfig
@@ -710,6 +711,7 @@ where
       r ← r.mkEqTrans (← simpLoop r.expr)
     cacheResult e cfg r
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_simp]
 def simpImpl (e : Expr) : SimpM Result := withIncRecDepth do
   checkSystem "simp"

src/Lean/Meta/Transform.lean

@@ -240,8 +240,8 @@ def unfoldDeclsFrom (biggerEnv : Environment) (e : Expr) : CoreM Expr := do
       if env.contains declName then
         return .done e
       let some info := biggerEnv.find? declName | return .done e
-      if info.hasValue then
-        return .visit (← instantiateValueLevelParams info us)
+      if info.hasValue (allowOpaque := true) then
+        return .visit (← instantiateValueLevelParams info us (allowOpaque := true))
       else
         return .done e
     Core.transform e (pre := pre)
@@ -282,7 +282,7 @@ def unfoldIfArgIsAppOf (fnNames : Array Name) (numSectionVars : Nat) (e : Expr)
         -/
         if revArgs.any isInterestingArg then
           if let some info@(.thmInfo _) := env.find? f.constName! then
-            return .visit <| (← instantiateValueLevelParams info f.constLevels!).betaRev revArgs
+            return .visit <| (← instantiateValueLevelParams info f.constLevels! (allowOpaque := true)).betaRev revArgs
       return .continue)
   where
     isInterestingArg (a : Expr) : Bool := a.withApp fun af axs =>

src/Lean/Meta/WHNF.lean

@@ -1100,6 +1100,7 @@ private def cache (useCache : Bool) (e r : Expr) : MetaM Expr := do
     modify fun s => { s with cache.whnf := s.cache.whnf.insert key r }
   return r
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_whnf]
 partial def whnfImp (e : Expr) : MetaM Expr :=
   withIncRecDepth <| whnfEasyCases e fun e => do

src/Lean/Parser.lean

@@ -65,6 +65,7 @@ end Parser
 namespace PrettyPrinter
 namespace Parenthesizer
 
+set_option compiler.ignoreBorrowAnnotation true in
 -- Close the mutual recursion loop; see corresponding `[extern]` in the parenthesizer.
 @[export lean_mk_antiquot_parenthesizer]
 def mkAntiquot.parenthesizer (name : String) (kind : SyntaxNodeKind) (anonymous := true) (isPseudoKind := true) : Parenthesizer :=
@@ -80,6 +81,7 @@ def mkAntiquot.parenthesizer (name : String) (kind : SyntaxNodeKind) (anonymous
 
 open Lean.Parser
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_pretty_printer_parenthesizer_interpret_parser_descr]
 unsafe def interpretParserDescr : ParserDescr → CoreM Parenthesizer
   | ParserDescr.const n                             => getConstAlias parenthesizerAliasesRef n
@@ -101,6 +103,7 @@ end Parenthesizer
 
 namespace Formatter
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_mk_antiquot_formatter]
 def mkAntiquot.formatter (name : String) (kind : SyntaxNodeKind) (anonymous := true) (isPseudoKind := true) : Formatter :=
   Parser.mkAntiquot.formatter name kind anonymous isPseudoKind
@@ -113,6 +116,7 @@ def mkAntiquot.formatter (name : String) (kind : SyntaxNodeKind) (anonymous := t
 
 open Lean.Parser
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_pretty_printer_formatter_interpret_parser_descr]
 unsafe def interpretParserDescr : ParserDescr → CoreM Formatter
   | ParserDescr.const n                             => getConstAlias formatterAliasesRef n

src/Lean/Util/FoldConsts.lean

@@ -64,11 +64,10 @@ namespace ConstantInfo
 
 /-- Return all names appearing in the type or value of a `ConstantInfo`. -/
 def getUsedConstantsAsSet (c : ConstantInfo) : NameSet :=
-  c.type.getUsedConstantsAsSet ++ match c.value? with
+  c.type.getUsedConstantsAsSet ++ match c.value? (allowOpaque := true) with
   | some v => v.getUsedConstantsAsSet
   | none => match c with
     | .inductInfo val => .ofList val.ctors
-    | .opaqueInfo val => val.value.getUsedConstantsAsSet
     | .ctorInfo val => ({} : NameSet).insert val.name
     | .recInfo val => .ofList val.all
     | _ => {}

src/kernel/declaration.h

@@ -224,7 +224,10 @@ public:
     bool is_mutual() const { return kind() == declaration_kind::MutualDefinition; }
     bool is_inductive() const { return kind() == declaration_kind::Inductive; }
     bool is_unsafe() const;
-    bool has_value() const { return is_theorem() || is_definition(); }
+    /** \brief Only definitions have values for the purpose of reduction and
+        type checking. Theorems used to be like that; now they are treated like
+        opaque declations. */
+    bool has_value() const { return is_definition(); }
 
     axiom_val const & to_axiom_val() const { lean_assert(is_axiom()); return static_cast<axiom_val const &>(cnstr_get_ref(raw(), 0)); }
     definition_val const & to_definition_val() const { lean_assert(is_definition()); return static_cast<definition_val const &>(cnstr_get_ref(raw(), 0)); }

src/lake/Lake/Load/Lean/Eval.lean

@@ -111,6 +111,18 @@ public def Package.loadFromEnv
         but then redefined as a '{decl.kind}'"
     else
       return m.insert decl.name (.mk decl rfl)
+  -- Check that executables have distinct root module names
+  let _ ← targetDecls.foldlM (init := ({} : Lean.NameMap Name)) fun exeRoots decl => do
+    if let some exeConfig := decl.config? LeanExe.configKind then
+      let root := exeConfig.root
+      if let some origExe := exeRoots.get? root then
+        error s!"\
+          {self.prettyName}: executable '{decl.name}' has the same root module '{root}' \
+          as executable '{origExe}'"
+      else
+        return exeRoots.insert root decl.name
+    else
+      return exeRoots
   let defaultTargets ← defaultTargetAttr.getAllEntries env |>.mapM fun name =>
     if let some decl := constTargetMap.find? name then pure decl.name else
       error s!"{self.prettyName}: package is missing target '{name}' marked as a default"

src/lake/Lake/Load/Toml.lean

@@ -415,35 +415,57 @@ local macro "gen_toml_decoders%" : command => do
 
 gen_toml_decoders%
 
+private structure DecodeTargetState (pkg : Name) where
+  decls : Array (PConfigDecl pkg) := #[]
+  map : DNameMap (NConfigDecl pkg) := {}
+  exeRoots : Lean.NameMap Name := {}
+
 private def decodeTargetDecls
-  (pkg : Name) (t : Table)
+  (pkg : Name) (prettyName : String) (t : Table)
 : DecodeM (Array (PConfigDecl pkg) × DNameMap (NConfigDecl pkg)) := do
-  let r := (#[], {})
+  let r : DecodeTargetState pkg := {}
   let r ← go r LeanLib.keyword LeanLib.configKind LeanLibConfig.decodeToml
   let r ← go r LeanExe.keyword LeanExe.configKind LeanExeConfig.decodeToml
   let r ← go r InputFile.keyword InputFile.configKind InputFileConfig.decodeToml
   let r ← go r InputDir.keyword InputDir.configKind InputDirConfig.decodeToml
-  return r
+  return (r.decls, r.map)
 where
-  go r kw kind (decode : {n : Name} → Table → DecodeM (ConfigType kind pkg n)) := do
+  go (r : DecodeTargetState pkg) kw kind
+      (decode : {n : Name} → Table → DecodeM (ConfigType kind pkg n)) := do
     let some tableArrayVal := t.find? kw | return r
     let some vals ← tryDecode? tableArrayVal.decodeValueArray | return r
     vals.foldlM (init := r) fun r val => do
       let some t ← tryDecode? val.decodeTable | return r
       let some name ← tryDecode? <| stringToLegalOrSimpleName <$> t.decode `name
         | return r
-      let (decls, map) := r
-      if let some orig := map.get? name then
-        modify fun es => es.push <| .mk val.ref s!"\
-          {pkg}: target '{name}' was already defined as a '{orig.kind}', \
+      if let some orig := r.map.get? name then
+        logDecodeErrorAt val.ref s!"{prettyName}: \
+          target '{name}' was already defined as a '{orig.kind}', \
           but then redefined as a '{kind}'"
-        return (decls, map)
+        return r
       else
         let config ← @decode name t
         let decl : NConfigDecl pkg name :=
           -- Safety: By definition, config kind = facet kind for declarative configurations.
           unsafe {pkg, name, kind, config, wf_data := lcProof}
-        return (decls.push decl.toPConfigDecl, map.insert name decl)
+        -- Check that executables have distinct root module names
+        let exeRoots ← id do
+          if h : kind = LeanExe.configKind then
+            let exeConfig : LeanExeConfig name := cast (by rw [h]; rfl) config
+            if let some origExe := r.exeRoots.get? exeConfig.root then
+              logDecodeErrorAt val.ref s!"{prettyName}: \
+                executable '{name}' has the same root module '{exeConfig.root}' as \
+                executable '{origExe}'"
+              return r.exeRoots
+            else
+              return r.exeRoots.insert exeConfig.root name
+          else
+            return r.exeRoots
+        return {
+          decls := r.decls.push decl.toPConfigDecl
+          map := r.map.insert name decl
+          exeRoots
+        }
 
 /-! ## Root Loader -/
 
@@ -458,8 +480,9 @@ public def loadTomlConfig (cfg: LoadConfig) : LogIO Package := do
       let wsIdx := cfg.pkgIdx
       let baseName := if cfg.pkgName.isAnonymous then origName else cfg.pkgName
       let keyName := baseName.num wsIdx
+      let prettyName := baseName.toString (escape := false)
       let config ← @PackageConfig.decodeToml keyName origName table
-      let (targetDecls, targetDeclMap) ← decodeTargetDecls keyName table
+      let (targetDecls, targetDeclMap) ← decodeTargetDecls keyName prettyName table
       let defaultTargets ← table.tryDecodeD `defaultTargets #[]
       let defaultTargets := defaultTargets.map stringToLegalOrSimpleName
       let depConfigs ← table.tryDecodeD `require #[]

src/lake/Lake/Toml/Decode.lean

@@ -96,6 +96,9 @@ public def mergeErrors (x₁ : EDecodeM α) (x₂ : EDecodeM β) (f : α → β
     | .error _ es => .error () es
   | .error _ es => .error () es
 
+@[inline] public def logDecodeErrorAt (ref : Syntax) (msg : String) : DecodeM Unit :=
+  fun es => .ok () (es.push {ref, msg})
+
 @[inline] public def throwDecodeErrorAt (ref : Syntax) (msg : String) : EDecodeM α :=
   fun es => .error () (es.push {ref, msg})