From aeb470d11dcbd625ace121e9d2e0a74dd91eb2f2 Mon Sep 17 00:00:00 2001
From: Noptus <raphael.caillon@solace.com>
Date: Mon, 25 May 2026 13:47:38 +0200
Subject: [PATCH] fix: report cbv in max-step diagnostics

---
 src/Lean/Meta/Sym/Simp/Main.lean   | 2 +-
 src/Lean/Meta/Sym/Simp/SimpM.lean  | 2 ++
 src/Lean/Meta/Tactic/Cbv/Main.lean | 6 +++---
 tests/elab/cbv_max_steps.lean      | 2 +-
 4 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Meta/Sym/Simp/Main.lean b/src/Lean/Meta/Sym/Simp/Main.lean
index 39cb34fe30cb..9613b52f6837 100644
--- a/src/Lean/Meta/Sym/Simp/Main.lean
+++ b/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₁}"
diff --git a/src/Lean/Meta/Sym/Simp/SimpM.lean b/src/Lean/Meta/Sym/Simp/SimpM.lean
index a4166d7e56bc..974fd85912ef 100644
--- a/src/Lean/Meta/Sym/Simp/SimpM.lean
+++ b/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
 
 /--
diff --git a/src/Lean/Meta/Tactic/Cbv/Main.lean b/src/Lean/Meta/Tactic/Cbv/Main.lean
index 6fd7b1ff518b..c741fc7eede8 100644
--- a/src/Lean/Meta/Tactic/Cbv/Main.lean
+++ b/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
diff --git a/tests/elab/cbv_max_steps.lean b/tests/elab/cbv_max_steps.lean
index 6b3a9d5665a9..fae88b45cd52 100644
--- a/tests/elab/cbv_max_steps.lean
+++ b/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