perf: use .local asyncMode for eqnOptionsExt (#13477)

This PR fixes a benchmark regression introduced in #13475:
`eqnOptionsExt`
was using `.async .asyncEnv` asyncMode, which accumulates state in the
`checked` environment and can block. Switching to `.local` — consistent
with the neighbouring `eqnsExt` and the other declaration caches in
`src/Lean/Meta` — restores performance (the
`build/profile/blocked (unaccounted) wall-clock` bench moves from +33%
back to baseline). `.local` is safe here because
`saveEqnAffectingOptions`
is only called during top-level `def` elaboration and downstream readers
see the imported state; modifications on non-main branches are merged
into the main branch on completion.

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

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

src/Lean/Elab/PreDefinition/Basic.lean

@@ -222,8 +222,8 @@ private def addNonRecAux (docCtx : LocalContext × LocalInstances) (preDef : Pre
     if compile && shouldGenCodeFor preDef then
       compileDecl decl
     if applyAttrAfterCompilation then
+      saveEqnAffectingOptions preDef.declName
       enableRealizationsForConst preDef.declName
-      generateEagerEqns preDef.declName
     addPreDefDocs docCtx preDef
     if applyAttrAfterCompilation then
       applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation

src/Lean/Elab/PreDefinition/EqUnfold.lean

@@ -28,7 +28,7 @@ def getConstUnfoldEqnFor? (declName : Name) : MetaM (Option Name) := do
     trace[ReservedNameAction] "getConstUnfoldEqnFor? {declName} failed, no unfold theorem available"
     return none
   let name := mkEqLikeNameFor (← getEnv) declName eqUnfoldThmSuffix
-  realizeConst declName name do
+  realizeConst declName name <| withEqnOptions declName do
     -- we have to call `getUnfoldEqnFor?` again to make `unfoldEqnName` available in this context
     let some unfoldEqnName ← getUnfoldEqnFor? (nonRec := true) declName | unreachable!
     let info ← getConstInfo unfoldEqnName

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -367,7 +367,7 @@ def mkEqns (declName : Name) (declNames : Array Name) : MetaM (Array Name) := do
     thmNames := thmNames.push name
     -- determinism: `type` should be independent of the environment changes since `baseName` was
     -- added
-    realizeConst declName name (doRealize name info type)
+    realizeConst declName name (withEqnOptions declName (doRealize name info type))
   return thmNames
 where
   doRealize name info type := withOptions (tactic.hygienic.set · false) do

src/Lean/Elab/PreDefinition/Mutual.lean

@@ -69,8 +69,10 @@ def addPreDefAttributes (preDefs : Array PreDefinition) : TermElabM Unit := do
           a.name = `instance_reducible || a.name = `implicit_reducible do
         setIrreducibleAttribute preDef.declName
 
+  for preDef in preDefs do
+    saveEqnAffectingOptions preDef.declName
+
   /-
-  `enableRealizationsForConst` must happen before `generateEagerEqns`
   It must happen in reverse order so that constants realized as part of the first decl
   have realizations for the other ones enabled
   -/
@@ -78,7 +80,6 @@ def addPreDefAttributes (preDefs : Array PreDefinition) : TermElabM Unit := do
     enableRealizationsForConst preDef.declName
 
   for preDef in preDefs do
-    generateEagerEqns preDef.declName
     applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
 
 end Lean.Elab.Mutual

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

@@ -163,7 +163,7 @@ public def registerEqnsInfo (preDef : PreDefinition) (declNames : Array Name) (r
 /-- Generate the "unfold" lemma for `declName`. -/
 def mkUnfoldEq (declName : Name) (info : EqnInfo) : MetaM Name := do
   let name := mkEqLikeNameFor (← getEnv) info.declName unfoldThmSuffix
-  realizeConst info.declNames[0]! name (doRealize name)
+  realizeConst info.declNames[0]! name (withEqnOptions declName (doRealize name))
   return name
 where
   doRealize name := withOptions (tactic.hygienic.set · false) do

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

@@ -208,11 +208,11 @@ def structuralRecursion
         -/
         registerEqnsInfo preDef (preDefs.map (·.declName)) recArgPos fixedParamPerms
     addSmartUnfoldingDef docCtx preDef recArgPos
+  for preDef in preDefs do
+    saveEqnAffectingOptions preDef.declName
   for preDef in preDefs do
     -- must happen in separate loop so realizations can see eqnInfos of all other preDefs
     enableRealizationsForConst preDef.declName
-    -- must happen after `enableRealizationsForConst`
-    generateEagerEqns preDef.declName
   applyAttributesOf preDefsNonRec AttributeApplicationTime.afterCompilation
 
 

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -497,14 +497,21 @@ def forEachVar (hs : Array Syntax) (tac : MVarId → FVarId → MetaM MVarId) :
 /--
   Searches for a metavariable `g` s.t. `tag` is its exact name.
   If none then searches for a metavariable `g` s.t. `tag` is a suffix of its name.
-  If none, then it searches for a metavariable `g` s.t. `tag` is a prefix of its name. -/
+  If none, then it searches for a metavariable `g` s.t. `tag` is a prefix of its name.
+
+  We erase macro scopes from the metavariable's user name before comparing, so that
+  user-written tags match even when a previous tactic left hygienic macro scopes at
+  the end of the tag (e.g. `e_a.yield._@._internal._hyg.0`, where `yield` is not the
+  literal last component of the name). Case tags written by the user are never
+  macro-scoped, so erasing scopes on the mvar side is sufficient.
+-/
 private def findTag? (mvarIds : List MVarId) (tag : Name) : TacticM (Option MVarId) := do
-  match (← mvarIds.findM? fun mvarId => return tag == (← mvarId.getDecl).userName) with
+  match (← mvarIds.findM? fun mvarId => return tag == (← mvarId.getDecl).userName.eraseMacroScopes) with
   | some mvarId => return mvarId
   | none =>
-  match (← mvarIds.findM? fun mvarId => return tag.isSuffixOf (← mvarId.getDecl).userName) with
+  match (← mvarIds.findM? fun mvarId => return tag.isSuffixOf (← mvarId.getDecl).userName.eraseMacroScopes) with
   | some mvarId => return mvarId
-  | none => mvarIds.findM? fun mvarId => return tag.isPrefixOf (← mvarId.getDecl).userName
+  | none => mvarIds.findM? fun mvarId => return tag.isPrefixOf (← mvarId.getDecl).userName.eraseMacroScopes
 
 private def getCaseGoals (tag : TSyntax ``binderIdent) : TacticM (MVarId × List MVarId) := do
   let gs ← getUnsolvedGoals

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

@@ -68,7 +68,10 @@ def setGoals (goals : List Goal) : GrindTacticM Unit :=
 
 def pruneSolvedGoals : GrindTacticM Unit := do
   let gs ← getGoals
-  let gs := gs.filter fun g => !g.inconsistent
+  let gs ← gs.filterM fun g => do
+    if g.inconsistent then return false
+    -- The metavariable may have been assigned by `isDefEq`
+    return !(← g.mvarId.isAssigned)
   setGoals gs
 
 def getUnsolvedGoals : GrindTacticM (List Goal) := do

src/Lean/Meta/Eqns.lean

@@ -37,12 +37,17 @@ register_builtin_option backward.eqns.deepRecursiveSplit : Bool := {
 These options affect the generation of equational theorems in a significant way. For these, their
 value at definition time, not realization time, should matter.
 
-This is implemented by
- * eagerly realizing the equations when they are set to a non-default value
- * when realizing them lazily, reset the options to their default
+This is implemented by storing their values at definition time (when non-default) in an environment
+extension, and restoring them when the equations are lazily realized.
 -/
 def eqnAffectingOptions : Array (Lean.Option Bool) := #[backward.eqns.nonrecursive, backward.eqns.deepRecursiveSplit]
 
+/-- Environment extension that stores the values of `eqnAffectingOptions` at definition time,
+keyed by declaration name. Only populated when at least one option has a non-default value.
+Stores an association list of (option name, value) pairs for options that differ from defaults. -/
+builtin_initialize eqnOptionsExt : MapDeclarationExtension (Array (Name × DataValue)) ←
+  mkMapDeclarationExtension (asyncMode := .local)
+
 def eqnThmSuffixBase := "eq"
 def eqnThmSuffixBasePrefix := eqnThmSuffixBase ++ "_"
 def eqn1ThmSuffix := eqnThmSuffixBasePrefix ++ "1"
@@ -153,12 +158,30 @@ structure EqnsExtState where
 builtin_initialize eqnsExt : EnvExtension EqnsExtState ←
   registerEnvExtension (pure {}) (asyncMode := .local)
 
+/--
+Runs `act` with the equation-affecting options restored to the values stored for `declName`
+at definition time (or reset to their defaults if none were stored). Use this inside
+`realizeConst` callbacks, which otherwise see the caller-independent `ctx.opts` rather than
+the outer `getEqnsFor?` context. -/
+def withEqnOptions (declName : Name) (act : MetaM α) : MetaM α := do
+  let env ← getEnv
+  let setOpts : Options → Options :=
+    if let some values := eqnOptionsExt.find? env declName then
+      fun os => Id.run do
+        let mut os := eqnAffectingOptions.foldl (fun os o => o.set os o.defValue) os
+        for (name, v) in values do
+          os := os.insert name v
+        return os
+    else
+      fun os => eqnAffectingOptions.foldl (fun os o => o.set os o.defValue) os
+  withOptions setOpts act
+
 /--
 Simple equation theorem for nonrecursive definitions.
 -/
 def mkSimpleEqThm (declName : Name) (name : Name) : MetaM (Option Name) := do
   if let some (.defnInfo info) := (← getEnv).find? declName then
-    realizeConst declName name (doRealize name info)
+    realizeConst declName name (withEqnOptions declName (doRealize name info))
     return some name
   else
     return none
@@ -229,19 +252,22 @@ private def getEqnsFor?Core (declName : Name) : MetaM (Option (Array Name)) := w
 Returns equation theorems for the given declaration.
 -/
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := withLCtx {} {} do
-  -- This is the entry point for lazy equation generation. Ignore the current value
-  -- of the options, and revert to the default.
-  withOptions (eqnAffectingOptions.foldl fun os o => o.set os o.defValue) do
+  withEqnOptions declName do
     getEqnsFor?Core declName
 
 /--
-If any equation theorem affecting option is not the default value, create the equations now.
+If any equation theorem affecting option is not the default value, store the option values
+for later use during lazy equation generation.
 -/
-def generateEagerEqns (declName : Name) : MetaM Unit := do
+def saveEqnAffectingOptions (declName : Name) : MetaM Unit := do
   let opts ← getOptions
-  if eqnAffectingOptions.any fun o => o.get opts != o.defValue then
-    trace[Elab.definition.eqns] "generating eager equations for {declName}"
-    let _ ← getEqnsFor?Core declName
+  let mut nonDefaults : Array (Name × DataValue) := #[]
+  for o in eqnAffectingOptions do
+    if o.get opts != o.defValue then
+      nonDefaults := nonDefaults.push (o.name, KVMap.Value.toDataValue (o.get opts))
+  unless nonDefaults.isEmpty do
+    trace[Elab.definition.eqns] "saving equation-affecting options for {declName}"
+    modifyEnv (eqnOptionsExt.insert · declName nonDefaults)
 
 @[expose] def GetUnfoldEqnFn := Name → MetaM (Option Name)
 

src/Lean/Meta/Tactic/Apply.lean

@@ -128,7 +128,6 @@ def postprocessAppMVars (tacticName : Name) (mvarId : MVarId) (newMVars : Array
     (synthAssignedInstances := true) (allowSynthFailures := false) : MetaM Unit := do
   synthAppInstances tacticName mvarId newMVars binderInfos synthAssignedInstances allowSynthFailures
   -- TODO: default and auto params
-  appendParentTag mvarId newMVars binderInfos
 
 private def dependsOnOthers (mvar : Expr) (otherMVars : Array Expr) : MetaM Bool :=
   otherMVars.anyM fun otherMVar => do
@@ -223,6 +222,7 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig :=
     let e ← instantiateMVars e
     mvarId.assign (mkAppN e newMVars)
     let newMVars ← newMVars.filterM fun mvar => not <$> mvar.mvarId!.isAssigned
+    appendParentTag mvarId newMVars binderInfos
     let otherMVarIds ← getMVarsNoDelayed e
     let newMVarIds ← reorderGoals newMVars cfg.newGoals
     let otherMVarIds := otherMVarIds.filter fun mvarId => !newMVarIds.contains mvarId

src/Lean/Meta/Tactic/Rewrite.lean

@@ -82,6 +82,7 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
           postprocessAppMVars `rewrite mvarId newMVars binderInfos
             (synthAssignedInstances := !tactic.skipAssignedInstances.get (← getOptions))
           let newMVarIds ← newMVars.map Expr.mvarId! |>.filterM fun mvarId => not <$> mvarId.isAssigned
+          appendParentTag mvarId newMVars binderInfos
           let otherMVarIds ← getMVarsNoDelayed heqIn
           let otherMVarIds := otherMVarIds.filter (!newMVarIds.contains ·)
           let newMVarIds := newMVarIds ++ otherMVarIds

tests/elab/1856.lean.out.expected

@@ -1,4 +1,3 @@
-case h
 α : Type ?u
 inst✝ : DecidableEq α
 i : α

tests/elab/2042.lean

@@ -2,8 +2,7 @@
   2 * a
 
 /--
-trace: case h
-x : Nat
+trace: x : Nat
 ⊢ 2 * x = x + x
 -/
 #guard_msgs in
@@ -19,8 +18,7 @@ by
   | a => 2 * a
 
 /--
-trace: case h
-x : Nat
+trace: x : Nat
 ⊢ 2 * x = x + x
 -/
 #guard_msgs in

tests/elab/apply_subgoal_name_issue.lean

@@ -0,0 +1,18 @@
+/-!
+Regression test: `case <ctor>` must keep working after `congr; ext _; cases _`
+even though the subgoal tags produced by `apply`-family tactics now inherit
+the parent tag (without appending the binder name) when only one subgoal is
+left. The case-tag matcher erases macro scopes so that `case yield` still
+matches tags like `e_a.yield._@._internal._hyg.0`.
+-/
+
+example {δ : Type} {m : Type → Type} [Monad m] [LawfulMonad m]
+    (x : m (ForInStep δ))
+    (f g : ForInStep δ → m (ForInStep δ))
+    (h : ∀ a, f a = g a) :
+    (x >>= f) = (x >>= g) := by
+  congr
+  ext step
+  cases step
+  case yield => apply h
+  case done  => apply h

tests/elab/consumePPHint.lean.out.expected

@@ -1,5 +1,4 @@
 consumePPHint.lean:8:8-8:14: warning: declaration uses `sorry`
-case a
 ⊢ q
     (have x := 0;
     x + 1)

tests/elab/convInConv.lean.out.expected

@@ -10,7 +10,6 @@ y : Nat
 | (fun x => x + y = 0) = fun x => False
 y : Nat
 | fun x => x + y = 0
-case h
 y x : Nat
 | y + x = 0
 y : Nat

tests/elab/inductionCheckAltNames.lean

@@ -10,7 +10,7 @@ axiom elimEx (motive : Nat → Nat → Sort u) (x y : Nat)
 error: Invalid alternative name `lower2`: Expected `lower`
 ---
 error: unsolved goals
-case upper.h
+case upper
 q d : Nat
 ⊢ q + d.succ > q
 ---
@@ -62,7 +62,7 @@ theorem invalidWildCard (p: Nat) : p ≤ q ∨ p > q := by
 error: Invalid alternative name `lower2`: There are no unhandled alternatives
 ---
 error: unsolved goals
-case lower.h
+case lower
 p delta✝ : Nat
 ⊢ p > p + delta✝.succ
 -/

tests/elab/meta.lean

@@ -100,7 +100,6 @@ x y : Nat
 h : x = y
 ⊢ y = x
 -----
-case h
 x y : Nat
 h : x = y
 ⊢ x = y

tests/elab/rflTacticErrors.lean

@@ -505,28 +505,24 @@ is not definitionally equal to the right-hand side
 example : S true false  := by with_reducible apply_rfl -- Error
 /--
 error: unsolved goals
-case a
 ⊢ true = true
 -/
 #guard_msgs in
 example : S true true   := by apply_rfl -- Error (left-over goal)
 /--
 error: unsolved goals
-case a
 ⊢ true = true
 -/
 #guard_msgs in
 example : S true true   := by with_reducible apply_rfl -- Error (left-over goal)
 /--
 error: unsolved goals
-case a
 ⊢ false = true
 -/
 #guard_msgs in
 example : S false false := by apply_rfl -- Error (left-over goal)
 /--
 error: unsolved goals
-case a
 ⊢ false = true
 -/
 #guard_msgs in

tests/elab/sym_interactive_bugs.lean

@@ -14,3 +14,8 @@ example (x y : Nat) (h : x ≤ y) : (1 - 1) + x  ≤ y + (1 + 0) := by
     simp chainSimp
     -- In the following tactic the goal is closed while preprocessing the target
     lia
+
+example : ∃ x, x = a := by
+  sym =>
+    apply Exists.intro
+    apply Eq.refl

tests/elab_fail/conv1.lean.out.expected

@@ -9,14 +9,13 @@ x y : Nat
 case x
 x y : Nat
 ⊢ x + y = y.add x
-case a
 a b : Nat
 | foo (0 + a) (b + 0)
-case a.x
+case x
 a b : Nat
 | 0 + a
 
-case a.y
+case y
 a b : Nat
 | b + 0
 a b : Nat
@@ -55,13 +54,10 @@ x y : Nat
 ⊢ f x (x.add y) y = y + x
 x y : Nat
 | x + y
-case h.h
 a b : Nat
 | 0 + a + b
-case h.h
 a b : Nat
 | a + b
-case h.h
 a b : Nat
 | 0 + a + b
 p : Nat → Prop
@@ -83,7 +79,6 @@ x : Nat
 p : Prop
 x : Nat
 ⊢ (True → p) → p
-case h
 x : Nat
 | 0 + x
 p : Prop

tests/elab_fail/decreasing_by.lean.out.expected

@@ -19,7 +19,6 @@ n m : Nat
 n m : Nat
 ⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (dec1 n, 100) (n, m)
 decreasing_by.lean:85:0-85:22: error: unsolved goals
-case a
 n m : Nat
 ⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (n, dec2 m) (n, m)
 

tests/elab_fail/inductionErrors.lean.out.expected

@@ -1,9 +1,9 @@
 inductionErrors.lean:11:12-11:27: error: unsolved goals
-case lower.h
+case lower
 p d : Nat
 ⊢ p ≤ p + d.succ
 inductionErrors.lean:12:12-12:27: error: unsolved goals
-case upper.h
+case upper
 q d : Nat
 ⊢ q + d.succ > q
 inductionErrors.lean:16:19-16:26: error(lean.unknownIdentifier): Unknown identifier `elimEx2`

tests/elab_fail/mutwf1.lean.out.expected

@@ -1,5 +1,4 @@
 mutwf1.lean:21:2-21:6: error: unsolved goals
-case h.a
 n : Nat
 h : n ≠ 0
 ⊢ n.sub 0 ≠ 0
@@ -7,6 +6,5 @@ mutwf1.lean:31:22-31:29: error: failed to prove termination, possible solutions:
   - Use `have`-expressions to prove the remaining goals
   - Use `termination_by` to specify a different well-founded relation
   - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
-case h
 n : Nat
 ⊢ n + 1 < n

tests/server_interactive/6594.lean.out.expected

@@ -4,12 +4,11 @@
  "goals": ["case right\n⊢ True"]}
 {"textDocument": {"uri": "file:///6594.lean"},
  "position": {"line": 9, "character": 2}}
-{"rendered": "```lean\ncase a\n⊢ True ∧ True\n```",
- "goals": ["case a\n⊢ True ∧ True"]}
+{"rendered": "```lean\n⊢ True ∧ True\n```", "goals": ["⊢ True ∧ True"]}
 {"textDocument": {"uri": "file:///6594.lean"},
  "position": {"line": 13, "character": 2}}
-{"rendered": "```lean\ncase a.right\n⊢ True\n```",
- "goals": ["case a.right\n⊢ True"]}
+{"rendered": "```lean\ncase right\n⊢ True\n```",
+ "goals": ["case right\n⊢ True"]}
 {"textDocument": {"uri": "file:///6594.lean"},
  "position": {"line": 20, "character": 2}}
 {"rendered": "```lean\ncase right\n⊢ True\n```",