fix: use cbv in max-step diagnostics

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

@@ -45,7 +45,7 @@ set_option compiler.ignoreBorrowAnnotation true in
 def simpImpl (e₁ : Expr) : SimpM Result := withIncRecDepth do
   let numSteps := (← get).numSteps
   if numSteps >= (← getConfig).maxSteps then
-    throwError "`simp` failed: maximum number of steps exceeded"
+    throwError "`{(← getConfig).name}` failed: maximum number of steps exceeded"
   let key : ExprPtr := { expr := e₁ }
   if let some result := (← get).persistentCache.find? key then
     trace[sym.simp.debug.cache] "persistent cache hit: {e₁}"

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

@@ -106,6 +106,8 @@ structure Config where
   Prevents infinite loops when conditional rewrite rules trigger recursive discharge attempts.
   -/
   maxDischargeDepth : Nat := 2
+  /-- User-facing name used in diagnostics emitted by this simplifier. -/
+  name : String := "simp"
   deriving Inhabited
 
 /--

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

@@ -325,7 +325,7 @@ public def cbvEntry (e : Expr) : MetaM Result := do
       | .ok (Result.rfl ..)     => return m!"cbv: no change{indentExpr e}"
       | .error err              => return m!"cbv: {err.toMessageData}") do
   let simprocs ← getCbvSimprocs
-  let config : Sym.Simp.Config := { maxSteps := cbv.maxSteps.get (← getOptions) }
+  let config : Sym.Simp.Config := { maxSteps := cbv.maxSteps.get (← getOptions), name := "cbv" }
   let methods := mkCbvMethods simprocs
   let e ← Sym.unfoldReducible e
   Sym.SymM.run do
@@ -347,7 +347,7 @@ type is `True`, the goal is closed. Otherwise, the target is replaced.
 
 After all reductions, attempts `refl` to close equation goals of the form `v = v`. -/
 public def cbvGoal (mvarId : MVarId) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) : MetaM (Option MVarId) := do
-  let config : Sym.Simp.Config := { maxSteps := cbv.maxSteps.get (← getOptions) }
+  let config : Sym.Simp.Config := { maxSteps := cbv.maxSteps.get (← getOptions), name := "cbv" }
   Sym.SymM.run do
     let mvarId ← Sym.preprocessMVar mvarId
     mvarId.withContext do
@@ -408,7 +408,7 @@ public def cbvDecideGoal (m : MVarId) : MetaM Unit := do
   withTraceNode `Meta.Tactic.cbv (fun
       | .ok ()   => return m!"decide_cbv: closed goal"
       | .error err => return m!"decide_cbv: {err.toMessageData}") do
-  let config : Sym.Simp.Config := { maxSteps := cbv.maxSteps.get (← getOptions) }
+  let config : Sym.Simp.Config := { maxSteps := cbv.maxSteps.get (← getOptions), name := "decide_cbv" }
   Sym.SymM.run do
     let m ← Sym.preprocessMVar m
     let mType ← m.getType

tests/elab/cbv_max_steps.lean

@@ -4,7 +4,7 @@ example : (List.replicate 10 1).length = 10 := by cbv
 -- Low limit triggers "maximum number of steps exceeded"
 set_option cbv.maxSteps 10 in
 /--
-error: `simp` failed: maximum number of steps exceeded
+error: `cbv` failed: maximum number of steps exceeded
 -/
 #guard_msgs (error) in
 example : (List.replicate 10 1).length = 10 := by cbv