refactor: move reportDbgIssue! from grind to SymM

This PR moves `reportDbgIssue!` and `expandReportDbgIssueMacro` from
`Grind/Types.lean` to `SymM.lean`. The macro now checks `sym.debug`
instead of `grind.debug`, since debug issue reporting is a Sym-level
concern shared across all modules in a `sym =>` block.

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

src/Lean/Meta/Sym/SymM.lean

@@ -15,6 +15,8 @@ register_builtin_option sym.debug : Bool := {
   descr    := "check invariants"
 }
 
+builtin_initialize registerTraceClass `sym.issues
+
 /-!
 ## Sym Extensions
 
@@ -134,9 +136,16 @@ structure SharedExprs where
   ordEqExpr  : Expr
   intExpr    : Expr
 
+/-- Configuration options for the symbolic computation framework. -/
+structure Config where
+  /-- When `true`, issues are collected during proof search and reported on failure. -/
+  verbose : Bool := true
+  deriving Inhabited
+
 /-- Readonly context for the symbolic computation framework. -/
 structure Context where
   sharedExprs : SharedExprs
+  config      : Config := {}
 
 /-- Mutable state for the symbolic computation framework. -/
 structure State where
@@ -177,6 +186,11 @@ structure State where
   defEqI : PHashMap (ExprPtr × ExprPtr) Bool := {}
   /-- State for registered `SymExtension`s, indexed by extension id. -/
   extensions : Array SymExtensionState := #[]
+  /--
+  Issues found during symbolic computation. Accumulated across operations
+  within a `sym =>` block and reported when a tactic fails.
+  -/
+  issues : List MessageData := []
   debug : Bool := false
 
 abbrev SymM := ReaderT Context <| StateRefT State MetaM
@@ -266,6 +280,55 @@ abbrev share (e : Expr) : SymM Expr :=
 @[inline] def isDebugEnabled : SymM Bool :=
   return (← get).debug
 
+def getConfig : SymM Config :=
+  return (← readThe Context).config
+
+/-- Adds an issue message to the issue tracker. -/
+def reportIssue (msg : MessageData) : SymM Unit := do
+  let msg ← addMessageContext msg
+  modify fun s => { s with issues := .trace { cls := `issue } msg #[] :: s.issues }
+  trace[sym.issues] msg
+
+/-- Reports an issue if `verbose` mode is enabled. Does nothing if `verbose` is `false`. -/
+@[inline] def reportIssueIfVerbose (msg : MessageData) : SymM Unit := do
+  if (← getConfig).verbose then
+    reportIssue msg
+
+private meta def expandReportIssueMacro (s : Syntax) : MacroM (TSyntax `doElem) := do
+  let msg ← if s.getKind == interpolatedStrKind then `(m! $(⟨s⟩)) else `(($(⟨s⟩) : MessageData))
+  `(doElem| Sym.reportIssueIfVerbose $msg)
+
+/-- Reports an issue if `verbose` mode is enabled. -/
+macro "reportIssue!" s:(interpolatedStr(term) <|> term) : doElem => do
+  expandReportIssueMacro s.raw
+
+/-- Reports an issue if both `verbose` and `sym.debug` are enabled. Does nothing otherwise. -/
+@[inline] def reportDbgIssue (msg : MessageData) : SymM Unit := do
+  if (← getConfig).verbose then
+    if sym.debug.get (← getOptions) then
+      reportIssue msg
+
+meta def expandReportDbgIssueMacro (s : Syntax) : MacroM (TSyntax `doElem) := do
+  let msg ← if s.getKind == interpolatedStrKind then `(m! $(⟨s⟩)) else `(($(⟨s⟩) : MessageData))
+  `(doElem| Sym.reportDbgIssue $msg)
+
+/-- Similar to `reportIssue!`, but only reports issue if `sym.debug` is set to `true`. -/
+macro "reportDbgIssue!" s:(interpolatedStr(term) <|> term) : doElem => do
+  expandReportDbgIssueMacro s.raw
+
+/-- Returns all accumulated issues without clearing them. -/
+def getIssues : SymM (List MessageData) :=
+  return (← get).issues
+
+/--
+Runs `x` with a fresh issue context. Issues reported during `x` are
+prepended to the issues that existed before the call.
+-/
+def withNewIssueContext (x : SymM α) : SymM α := do
+  let saved := (← get).issues
+  modify fun s => { s with issues := [] }
+  try x finally modify fun s => { s with issues := s.issues ++ saved }
+
 /-- Similar to `Meta.isDefEqI`, but the result is cache using pointer equality. -/
 def isDefEqI (s t : Expr) : SymM Bool := do
   let key := (⟨s⟩, ⟨t⟩)

src/Lean/Meta/Tactic/Grind.lean

@@ -63,7 +63,6 @@ builtin_initialize registerTraceClass `grind.ematch.instance
 builtin_initialize registerTraceClass `grind.ematch.instance.assignment
 builtin_initialize registerTraceClass `grind.ematch.instance.delayed
 builtin_initialize registerTraceClass `grind.eqResolution
-builtin_initialize registerTraceClass `grind.issues
 builtin_initialize registerTraceClass `grind.simp
 builtin_initialize registerTraceClass `grind.split
 builtin_initialize registerTraceClass `grind.split.candidate

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

@@ -53,7 +53,7 @@ def mkEqCnstr (p : Poly) (h : EqCnstrProof) : RingM EqCnstr := do
 Returns the ring expression denoting the given Lean expression.
 Recall that we compute the ring expressions during internalization.
 -/
-private def toRingExpr? [Monad m] [MonadLiftT GrindM m] [MonadRing m] (e : Expr) : m (Option RingExpr) := do
+private def toRingExpr? [Monad m] [MonadLiftT GrindM m] [MonadLiftT Sym.SymM m] [MonadRing m] (e : Expr) : m (Option RingExpr) := do
   let ring ← getRing
   if let some re := ring.denote.find? { expr := e } then
     return some re
@@ -67,7 +67,7 @@ private def toRingExpr? [Monad m] [MonadLiftT GrindM m] [MonadRing m] (e : Expr)
 Returns the semiring expression denoting the given Lean expression.
 Recall that we compute the semiring expressions during internalization.
 -/
-private def toSemiringExpr? [Monad m] [MonadLiftT GrindM m] [MonadSemiring m] (e : Expr) : m (Option SemiringExpr) := do
+private def toSemiringExpr? [Monad m] [MonadLiftT GrindM m] [MonadLiftT Sym.SymM m] [MonadSemiring m] (e : Expr) : m (Option SemiringExpr) := do
   let semiring ← getSemiring
   if let some re := semiring.denote.find? { expr := e } then
     return some re

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

@@ -456,7 +456,7 @@ private def getUnassignedLevelMVars (e : Expr) : MetaM (Array LMVarId) := do
 -- **Note**: issues reported by the E-matching module are too distractive. We only
 -- report them if `set_option grind.debug true`
 macro "reportEMatchIssue!" s:(interpolatedStr(term) <|> term) : doElem => do
-  expandReportDbgIssueMacro s.raw
+  Sym.expandReportDbgIssueMacro s.raw
 
 /--
 Stores new theorem instance in the state.

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

@@ -104,6 +104,8 @@ private def discharge? (e : Expr) : SimpM (Option Expr) := do
 open Sym
 
 def GrindM.run (x : GrindM α) (params : Params) (evalTactic? : Option EvalTactic := none) : MetaM α := Sym.SymM.run do
+  withNewIssueContext do
+  withReader (fun ctx => { ctx with config.verbose := params.config.verbose }) do
   /- **Note**: Consider using `Sym.simp` in the future. -/
   let simprocs  := params.normProcs
   let simpMethods := Simp.mkMethods simprocs discharge? (wellBehavedDischarge := true)
@@ -332,7 +334,7 @@ private def initCore (mvarId : MVarId) : GrindM Goal := do
     processHypotheses goal
 
 def mkResult (params : Params) (failure? : Option Goal) : GrindM Result := do
-  let issues     := (← get).issues
+  let issues     ← Sym.getIssues
   let counters   := (← get).counters
   let splitDiags := (← get).splitDiags
   let simp       := { (← get).simp with }

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

@@ -214,11 +214,6 @@ structure State where
   and implement the macro `trace_goal`.
   -/
   lastTag    : Name := .anonymous
-  /--
-  Issues found during the proof search. These issues are reported to
-  users when `grind` fails.
-  -/
-  issues     : List MessageData := []
   /-- Performance counters -/
   counters   : Counters := {}
   /-- Split diagnostic information. This information is only collected when `set_option diagnostics true` -/
@@ -401,35 +396,6 @@ def mkHCongrWithArity (f : Expr) (numArgs : Nat) : GrindM CongrTheorem := do
   modify fun s => { s with congrThms := s.congrThms.insert key result }
   return result
 
-def reportIssue (msg : MessageData) : GrindM Unit := do
-  let msg ← addMessageContext msg
-  modify fun s => { s with issues := .trace { cls := `issue } msg #[] :: s.issues }
-  /-
-  We also add a trace message because we may want to know when
-  an issue happened relative to other trace messages.
-  -/
-  trace[grind.issues] msg
-
-private meta def expandReportIssueMacro (s : Syntax) : MacroM (TSyntax `doElem) := do
-  let msg ← if s.getKind == interpolatedStrKind then `(m! $(⟨s⟩)) else `(($(⟨s⟩) : MessageData))
-  `(doElem| do
-    if (← getConfig).verbose then
-      reportIssue $msg)
-
-macro "reportIssue!" s:(interpolatedStr(term) <|> term) : doElem => do
-  expandReportIssueMacro s.raw
-
-/-- Similar to `expandReportIssueMacro`, but only reports issue if `grind.debug` is set to `true` -/
-meta def expandReportDbgIssueMacro (s : Syntax) : MacroM (TSyntax `doElem) := do
-  let msg ← if s.getKind == interpolatedStrKind then `(m! $(⟨s⟩)) else `(($(⟨s⟩) : MessageData))
-  `(doElem| do
-    if (← getConfig).verbose then
-      if grind.debug.get (← getOptions) then
-        reportIssue $msg)
-
-/-- Similar to `reportIssue!`, but only reports issue if `grind.debug` is set to `true` -/
-macro "reportDbgIssue!" s:(interpolatedStr(term) <|> term) : doElem => do
-  expandReportDbgIssueMacro s.raw
 
 /--
 Each E-node may have "solver terms" attached to them.

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

@@ -130,7 +130,7 @@ def foldProjs (e : Expr) : MetaM Expr := do
   let post (e : Expr) := do
     let .proj structName idx s := e | return .done e
     let some info := getStructureInfo? (← getEnv) structName |
-      trace[grind.issues] "found `Expr.proj` but `{structName}` is not marked as structure{indentExpr e}"
+      trace[sym.issues] "found `Expr.proj` but `{structName}` is not marked as structure{indentExpr e}"
       return .done e
     if h : idx < info.fieldNames.size then
       let fieldName := info.fieldNames[idx]
@@ -149,7 +149,7 @@ def foldProjs (e : Expr) : MetaM Expr := do
       -/
       return .visit (← withDefault <| mkProjection s fieldName)
     else
-      trace[grind.issues] "found `Expr.proj` with invalid field index `{idx}`{indentExpr e}"
+      trace[sym.issues] "found `Expr.proj` with invalid field index `{idx}`{indentExpr e}"
       return .done e
   Meta.transform e (post := post)
 

tests/elab/grind_9427.lean

@@ -30,10 +30,10 @@ example (x y z : BitVec 100000) : x * y - z*z = 0 → z*z = y * x := by
   grind -lia
 
 /--
-trace: [grind.issues] exponent 1024 exceeds threshold for exponentiation `(exp := 16)`
-[grind.issues] exponent 1024 exceeds threshold for exponentiation `(exp := 16)`
+trace: [sym.issues] exponent 1024 exceeds threshold for exponentiation `(exp := 16)`
+[sym.issues] exponent 1024 exceeds threshold for exponentiation `(exp := 16)`
 -/
 #guard_msgs in
-set_option trace.grind.issues true in
+set_option trace.sym.issues true in
 example (x y : BitVec 1024) : x * y = y * x := by
   grind (exp := 16)

tests/elab/grind_big_poly.lean

@@ -1,10 +1,10 @@
 module
 /--
-trace: [grind.issues] maximum recursion depth has been reached
+trace: [sym.issues] maximum recursion depth has been reached
     use `set_option maxRecDepth <num>` to increase limit
     use `set_option diagnostics true` to get diagnostic information
 -/
 #guard_msgs (drop error, trace) in
-set_option trace.grind.issues true in
+set_option trace.sym.issues true in
 example (x y z w : Int) : (x + y + z + w)^5000 - 1 = 0 := by
   grind -- should not crash

tests/elab/grind_hashmap_list.lean

@@ -7,6 +7,6 @@ open Std
 attribute [grind →] List.length_pos_of_mem
 attribute [grind] HashMap.size_insert
 
-set_option trace.grind.issues true in
+set_option trace.sym.issues true in
 example (m : HashMap Nat Nat) : ((m.insert 1 2).insert 3 4).size ≥ m.size := by
   grind

tests/elab/grind_heartbeats.lean

@@ -13,13 +13,13 @@ macro_rules
 -- This test has been commented out as it is nondeterministic:
 -- sometimes it fails with a timeout at `whnf` rather than `isDefEq`.
 -- /--
--- trace: [grind.issues] (deterministic) timeout at `isDefEq`, maximum number of heartbeats (5000) has been reached
+-- trace: [sym.issues] (deterministic) timeout at `isDefEq`, maximum number of heartbeats (5000) has been reached
 --     Use `set_option maxHeartbeats <num>` to set the limit.
 --     ⏎
 --     Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -- -/
 -- #guard_msgs (trace, drop error) in
--- set_option trace.grind.issues true in
+-- set_option trace.sym.issues true in
 -- set_option maxHeartbeats 5000 in
 -- example : gen! 10 = 0 ∧ True := by
 --   set_option trace.Meta.debug true in

tests/elab/grind_issue_9187.lean

@@ -18,7 +18,7 @@ structure Iso (x y : C) where
 attribute [grind =] Iso.hom_inv_id Iso.inv_hom_id
 
 #guard_msgs in -- Should not produce any issues
-set_option trace.grind.issues true in
+set_option trace.sym.issues true in
 example (F G : Foo ℭ₁ ℭ₂) (e : ∀ (x : C), Iso (F.obj x) (G.obj x)) (x : C) :
     ℭ₂.comp (e x).hom (e x).inv = ℭ₂.id _ := by
   grind

tests/elab/grind_linarith_1.lean

@@ -1,6 +1,6 @@
 module
 open Std Lean.Grind
-set_option grind.debug true
+set_option sym.debug true
 
 example [IntModule α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedAdd α] (a b : α)
     : (2:Int) • a + b < b + a + a → False := by
@@ -66,23 +66,23 @@ example [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [Ordere
 
 -- Test misconfigured instances
 /--
-trace: [grind.issues] type has `LE`, but is not a partial order, failed to synthesize
+trace: [sym.issues] type has `LE`, but is not a partial order, failed to synthesize
       IsPartialOrder α
-[grind.issues] type has `LE`, but is not a linear preorder, failed to synthesize
+[sym.issues] type has `LE`, but is not a linear preorder, failed to synthesize
       IsLinearPreorder α
-[grind.issues] type has `LE` and `LT`, but the `LT` instance is not lawful, failed to synthesize
+[sym.issues] type has `LE` and `LT`, but the `LT` instance is not lawful, failed to synthesize
       LawfulOrderLT α
-[grind.issues] type has `LE` and `LT`, but the `LT` instance is not lawful, failed to synthesize
+[sym.issues] type has `LE` and `LT`, but the `LT` instance is not lawful, failed to synthesize
       LawfulOrderLT α
-[grind.issues] type has `LE`, but is not a partial order, failed to synthesize
+[sym.issues] type has `LE`, but is not a partial order, failed to synthesize
       IsPartialOrder α
-[grind.issues] type has `LE`, but is not a linear order, failed to synthesize
+[sym.issues] type has `LE`, but is not a linear order, failed to synthesize
       IsLinearOrder α
-[grind.issues] type has a `Preorder` and is a `Semiring`, but is not an ordered ring, failed to synthesize
+[sym.issues] type has a `Preorder` and is a `Semiring`, but is not an ordered ring, failed to synthesize
       OrderedRing α
 -/
 #guard_msgs (drop error, trace) in
-set_option trace.grind.issues true in
+set_option trace.sym.issues true in
 example [CommRing α] [LE α] [LT α] [IsPreorder α] [OrderedAdd α] (a b c : α)
     : a < b → b + b < c → c < a → False := by
   grind

tests/elab/grind_linarith_spurious_issues.lean

@@ -3,6 +3,6 @@ open Lean Grind
 
 -- Should not produced spurious issues.
 #guard_msgs (drop error, trace) in
-set_option trace.grind.issues true in
+set_option trace.sym.issues true in
 example [Field α] (a b : α) : a*b + b*c = 2 → b = a⁻¹ := by
   grind

tests/elab/grind_mvar.lean

@@ -5,7 +5,7 @@ attribute [grind →] Array.eq_empty_of_append_eq_empty eq_nil_of_length_eq_zero
 attribute [grind] Vector.getElem?_append getElem?_dropLast
 
 #guard_msgs (trace) in -- should not report any issues
-set_option trace.grind.issues true
+set_option trace.sym.issues true
 theorem dropLast_concat : dropLast (l₁ ++ [b]) = l₁ := by
    fail_if_success grind
    grind -ext only [List.dropLast_append_cons, List.dropLast_singleton, List.append_nil]

tests/elab/grind_pre.lean

@@ -171,14 +171,14 @@ example (a : α) (p q r : Prop) : (h₁ : p ≍ a) → (h₂ : q ≍ a) → (h
   grind
 
 /--
-trace: [grind.issues] found congruence between
+trace: [sym.issues] found congruence between
       g b
     and
       f a
     but functions have different types
 -/
 #guard_msgs (trace) in
-set_option trace.grind.issues true in
+set_option trace.sym.issues true in
 set_option trace.grind.debug.proof false in
 example (f : Nat → Bool) (g : Int → Bool) (a : Nat) (b : Int) : f ≍ g → a ≍ b → f a = g b := by
   fail_if_success grind

tests/elab/grind_ring_op_sanity_checks.lean

@@ -34,7 +34,7 @@ when only reducible definitions and instances are reduced
 -/
 #guard_msgs in
 example [CommRing α] [Sub α] (a b : α) : a = OfNat.ofNat (α := α) 5 → b = 5 → a - b = 0 := by
-  set_option trace.grind.issues true in
+  set_option trace.sym.issues true in
   grind
 
 /--

tests/elab/grind_t1.lean

@@ -389,7 +389,7 @@ example (b : Bool) : (if b then 10 else 20) = a → b = true → False := by
 
 -- Should not generate a trace message about canonicalization issues
 #guard_msgs (trace) in
-set_option trace.grind.issues true in
+set_option trace.sym.issues true in
 example : (if n + 2 < m then a else b) = (if n + 1 < m then c else d) := by
   fail_if_success grind (splits := 0)
   sorry