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

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

tests/elab/12897.lean

@@ -1,12 +1,25 @@
--- Tests that `inferInstanceAs` auxiliary definitions are properly marked `meta`
--- when used inside a `meta` section.
+-- Tests that `normalizeInstance` auxiliary definitions work correctly
+-- when used inside a `meta` section, for both `inferInstanceAs` and `deriving`.
 
 module
 
-meta section
+public meta import Lean.Elab.Command
 
-def Foo := List Nat
+public meta section
 
-instance : EmptyCollection Foo := inferInstanceAs (EmptyCollection (List Nat))
+namespace Test
 
-end
+open Lean
+
+-- `@[expose]` forces `normalizeInstance` to create aux wrapper definitions,
+-- which is where the meta marking matters.
+@[expose] def Foo := Unit
+deriving Inhabited
+
+@[expose] def Bar := Name
+deriving Inhabited
+
+@[expose] def Baz := List Nat
+instance : EmptyCollection Baz := inferInstanceAs (EmptyCollection (List Nat))
+
+end Test

tests/elab/13043.lean

@@ -0,0 +1,20 @@
+-- Tests that `deriving` instances inside a `meta section` are properly marked `meta`.
+-- Regression test for https://github.com/leanprover/lean4/pull/13043
+
+module
+
+public meta import Lean.Elab.Command
+
+public meta section
+
+namespace Test
+
+open Lean
+
+@[expose] def Foo := Unit
+deriving Inhabited
+
+@[expose] def Bar := Name
+deriving Inhabited
+
+end Test

tests/elab/inferInstanceAs.lean

@@ -13,6 +13,12 @@ def D := I
 
 instance : C D := inferInstanceAs (C I)
 
+-- We can still use it as an `inferInstance` synonym in the old mode
+set_option backward.inferInstanceAs.wrap false in
+/-- info: «inferInstanceAs» (C D) : C D -/
+#guard_msgs in
+#check inferInstanceAs (C D)
+
 /--
 info: @[implicit_reducible] private def instCD : C D :=
 { c := instCD._aux_1 }

tests/elab/lcnf_borrow_expected_type.lean

@@ -139,8 +139,6 @@ structure Quad where
 /-- Only traverses → parameter stays borrowed. -/
 @[noinline] def measuree (xs : List Nat) : Nat := xs.length
 
-/-
-
 /--
 trace: [Compiler.explicitRc] size: 22
     def cascadeDemo @&t : tobj :=
@@ -257,5 +255,3 @@ def preserveTailCall (x : @&Prod Nat Nat) (a : Nat) : Nat :=
   match a with
   | 0 => x.fst
   | a + 1 => preserveTailCall (mkNewProd x a) a
-
--/

tests/pkg/sym_ext/SymExt.lean

@@ -0,0 +1,28 @@
+/-
+Tests for `SymExtension` mechanism.
+-/
+module
+public meta import SymExt.Decl
+meta import Lean.Meta.Sym
+
+open Lean Elab Tactic Meta Sym
+
+run_meta SymM.run do
+  let c0 ← getMyCounter
+  assert! c0 == 0
+  incrementMyCounter
+  let c1 ← getMyCounter
+  assert! c1 == 1
+  incrementMyCounter
+  let c2 ← getMyCounter
+  assert! c2 == 2
+
+run_meta do
+  SymM.run do
+    incrementMyCounter
+    let c ← getMyCounter
+    assert! c == 1
+  -- Should reset the counter
+  SymM.run do
+    let c ← getMyCounter
+    assert! c == 0

tests/pkg/sym_ext/SymExt/Decl.lean

@@ -0,0 +1,20 @@
+/-
+Declare a SymExtension and register it.
+-/
+module
+public import Lean.Meta.Sym.SymM
+open Lean Meta Sym
+
+/-- Simple counter state for testing. -/
+public structure MyExtState where
+  counter : Nat := 0
+  deriving Inhabited
+
+initialize myExt : SymExtension MyExtState ←
+  registerSymExtension (return {})
+
+public def getMyCounter : SymM Nat := do
+  return (← myExt.getState).counter
+
+public def incrementMyCounter : SymM Unit := do
+  myExt.modifyState fun s => { s with counter := s.counter + 1 }

tests/pkg/sym_ext/lakefile.lean

@@ -0,0 +1,5 @@
+import Lake
+open System Lake DSL
+
+package sym_ext
+@[default_target] lean_lib SymExt

tests/pkg/sym_ext/lean-toolchain

@@ -0,0 +1 @@
+../../../build/release/stage1

tests/pkg/sym_ext/run_test.sh

@@ -0,0 +1,2 @@
+rm -rf .lake/build
+lake build