chore: fix tests

src/Init/Prelude.lean

@@ -4372,7 +4372,7 @@ def defaultMaxRecDepth := 512
 
 /-- The message to display on stack overflow. -/
 def maxRecDepthErrorMessage : String :=
-  "maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)"
+  "maximum recursion depth has been reached\nuse `set_option maxRecDepth <num>` to increase limit\nuse `set_option diagnostics true` to get diagnostic information"
 
 namespace Syntax
 

src/Lean/CoreM.lean

@@ -236,7 +236,7 @@ protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m
     throw <| Exception.error .missing "elaboration interrupted"
 
 def throwMaxHeartbeat (moduleName : Name) (optionName : Name) (max : Nat) : CoreM Unit := do
-  let msg := s!"(deterministic) timeout at '{moduleName}', maximum number of heartbeats ({max/1000}) has been reached (use 'set_option {optionName} <num>' to set the limit)"
+  let msg := s!"(deterministic) timeout at `{moduleName}`, maximum number of heartbeats ({max/1000}) has been reached\nuse `set_option {optionName} <num>` to set the limit\nuse `set_option {diagnostics.name} true` to get diagnostic information"
   throw <| Exception.error (← getRef) (MessageData.ofFormat (Std.Format.text msg))
 
 def checkMaxHeartbeatsCore (moduleName : String) (optionName : Name) (max : Nat) : CoreM Unit := do

src/Lean/Elab/Tactic/Simp.lean

@@ -15,7 +15,6 @@ import Lean.Elab.Tactic.Config
 namespace Lean.Elab.Tactic
 open Meta
 open TSyntax.Compat
-open Simp (UsedSimps)
 
 declare_config_elab elabSimpConfigCore    Meta.Simp.Config
 declare_config_elab elabSimpConfigCtxCore Meta.Simp.ConfigCtx
@@ -327,7 +326,7 @@ If `stx` is the syntax of a `simp`, `simp_all` or `dsimp` tactic invocation, and
 creates the syntax of an equivalent `simp only`, `simp_all only` or `dsimp only`
 invocation.
 -/
-def mkSimpOnly (stx : Syntax) (usedSimps : UsedSimps) : MetaM Syntax := do
+def mkSimpOnly (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Syntax := do
   let isSimpAll := stx.isOfKind ``Parser.Tactic.simpAll
   let mut stx := stx
   if stx[3].isNone then
@@ -379,7 +378,7 @@ def mkSimpOnly (stx : Syntax) (usedSimps : UsedSimps) : MetaM Syntax := do
   let argsStx := if args.isEmpty then #[] else #[mkAtom "[", (mkAtom ",").mkSep args, mkAtom "]"]
   return stx.setArg 4 (mkNullNode argsStx)
 
-def traceSimpCall (stx : Syntax) (usedSimps : UsedSimps) : MetaM Unit := do
+def traceSimpCall (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Unit := do
   logInfoAt stx[0] m!"Try this: {← mkSimpOnly stx usedSimps}"
 
 /--
@@ -396,7 +395,7 @@ For many tactics other than the simplifier,
 one should use the `withLocation` tactic combinator
 when working with a `location`.
 -/
-def simpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (discharge? : Option Simp.Discharge := none) (loc : Location) : TacticM UsedSimps := do
+def simpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (discharge? : Option Simp.Discharge := none) (loc : Location) : TacticM Simp.Stats := do
   match loc with
   | Location.targets hyps simplifyTarget =>
     withMainContext do
@@ -406,33 +405,41 @@ def simpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (discharge
     withMainContext do
       go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true)
 where
-  go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM UsedSimps := do
+  go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Simp.Stats := do
     let mvarId ← getMainGoal
-    let (result?, usedSimps) ← simpGoal mvarId ctx (simprocs := simprocs) (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp)
+    let (result?, stats) ← simpGoal mvarId ctx (simprocs := simprocs) (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp)
     match result? with
     | none => replaceMainGoal []
     | some (_, mvarId) => replaceMainGoal [mvarId]
-    return usedSimps
+    return stats
+
+def withSimpDiagnostics (x : TacticM Simp.Diagnostics) : TacticM Unit := do
+  let origDiag := (← getThe Meta.State).diag
+  let stats ← x
+  Simp.reportDiag stats origDiag
+  return ()
 
 /-
   "simp" (config)? (discharger)? (" only")? (" [" ((simpStar <|> simpErase <|> simpLemma),*,?) "]")?
   (location)?
 -/
-@[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => withMainContext do
+@[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => withMainContext do withSimpDiagnostics do
   let { ctx, simprocs, dischargeWrapper } ← mkSimpContext stx (eraseLocal := false)
-  let usedSimps ← dischargeWrapper.with fun discharge? =>
+  let stats ← dischargeWrapper.with fun discharge? =>
     simpLocation ctx simprocs discharge? (expandOptLocation stx[5])
   if tactic.simp.trace.get (← getOptions) then
-    traceSimpCall stx usedSimps
+    traceSimpCall stx stats.usedTheorems
+  return stats.diag
 
-@[builtin_tactic Lean.Parser.Tactic.simpAll] def evalSimpAll : Tactic := fun stx => withMainContext do
+@[builtin_tactic Lean.Parser.Tactic.simpAll] def evalSimpAll : Tactic := fun stx => withMainContext do withSimpDiagnostics do
   let { ctx, simprocs, .. } ← mkSimpContext stx (eraseLocal := true) (kind := .simpAll) (ignoreStarArg := true)
-  let (result?, usedSimps) ← simpAll (← getMainGoal) ctx (simprocs := simprocs)
+  let (result?, stats) ← simpAll (← getMainGoal) ctx (simprocs := simprocs)
   match result? with
   | none => replaceMainGoal []
   | some mvarId => replaceMainGoal [mvarId]
   if tactic.simp.trace.get (← getOptions) then
-    traceSimpCall stx usedSimps
+    traceSimpCall stx stats.usedTheorems
+  return stats.diag
 
 def dsimpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (loc : Location) : TacticM Unit := do
   match loc with
@@ -444,14 +451,15 @@ def dsimpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (loc : Lo
     withMainContext do
       go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true)
 where
-  go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Unit := do
+  go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Unit := withSimpDiagnostics do
     let mvarId ← getMainGoal
-    let (result?, usedSimps) ← dsimpGoal mvarId ctx simprocs (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp)
+    let (result?, stats) ← dsimpGoal mvarId ctx simprocs (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp)
     match result? with
     | none => replaceMainGoal []
     | some mvarId => replaceMainGoal [mvarId]
     if tactic.simp.trace.get (← getOptions) then
-      mvarId.withContext <| traceSimpCall (← getRef) usedSimps
+      mvarId.withContext <| traceSimpCall (← getRef) stats.usedTheorems
+    return stats.diag
 
 @[builtin_tactic Lean.Parser.Tactic.dsimp] def evalDSimp : Tactic := fun stx => do
   let { ctx, simprocs, .. } ← withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)

src/Lean/Elab/Tactic/SimpTrace.lean

@@ -25,39 +25,41 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
 @[builtin_tactic simpTrace] def evalSimpTrace : Tactic := fun stx =>
   match stx with
   | `(tactic|
-      simp?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => withMainContext do
+      simp?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => withMainContext do withSimpDiagnostics do
     let stx ← if bang.isSome then
       `(tactic| simp!%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
     else
       `(tactic| simp%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
     let { ctx, simprocs, dischargeWrapper } ← mkSimpContext stx (eraseLocal := false)
-    let usedSimps ← dischargeWrapper.with fun discharge? =>
+    let stats ← dischargeWrapper.with fun discharge? =>
       simpLocation ctx (simprocs := simprocs) discharge? <|
         (loc.map expandLocation).getD (.targets #[] true)
-    let stx ← mkSimpCallStx stx usedSimps
+    let stx ← mkSimpCallStx stx stats.usedTheorems
     addSuggestion tk stx (origSpan? := ← getRef)
+    return stats.diag
   | _ => throwUnsupportedSyntax
 
 @[builtin_tactic simpAllTrace] def evalSimpAllTrace : Tactic := fun stx =>
   match stx with
-  | `(tactic| simp_all?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?) => do
+  | `(tactic| simp_all?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?) => withSimpDiagnostics do
     let stx ← if bang.isSome then
       `(tactic| simp_all!%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?)
     else
       `(tactic| simp_all%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?)
     let { ctx, .. } ← mkSimpContext stx (eraseLocal := true)
       (kind := .simpAll) (ignoreStarArg := true)
-    let (result?, usedSimps) ← simpAll (← getMainGoal) ctx
+    let (result?, stats) ← simpAll (← getMainGoal) ctx
     match result? with
     | none => replaceMainGoal []
     | some mvarId => replaceMainGoal [mvarId]
-    let stx ← mkSimpCallStx stx usedSimps
+    let stx ← mkSimpCallStx stx stats.usedTheorems
     addSuggestion tk stx (origSpan? := ← getRef)
+    return stats.diag
   | _ => throwUnsupportedSyntax
 
 /-- Implementation of `dsimp?`. -/
 def dsimpLocation' (ctx : Simp.Context) (simprocs : SimprocsArray) (loc : Location) :
-    TacticM Simp.UsedSimps := do
+    TacticM Simp.Stats := do
   match loc with
   | Location.targets hyps simplifyTarget =>
     withMainContext do
@@ -68,25 +70,26 @@ def dsimpLocation' (ctx : Simp.Context) (simprocs : SimprocsArray) (loc : Locati
       go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true)
 where
   /-- Implementation of `dsimp?`. -/
-  go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Simp.UsedSimps := do
+  go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Simp.Stats := do
     let mvarId ← getMainGoal
-    let (result?, usedSimps) ← dsimpGoal mvarId ctx simprocs (simplifyTarget := simplifyTarget)
+    let (result?, stats) ← dsimpGoal mvarId ctx simprocs (simplifyTarget := simplifyTarget)
       (fvarIdsToSimp := fvarIdsToSimp)
     match result? with
     | none => replaceMainGoal []
     | some mvarId => replaceMainGoal [mvarId]
-    pure usedSimps
+    pure stats
 
 @[builtin_tactic dsimpTrace] def evalDSimpTrace : Tactic := fun stx =>
   match stx with
-  | `(tactic| dsimp?%$tk $[!%$bang]? $(config)? $[only%$o]? $[[$args,*]]? $(loc)?) => do
+  | `(tactic| dsimp?%$tk $[!%$bang]? $(config)? $[only%$o]? $[[$args,*]]? $(loc)?) => withSimpDiagnostics do
     let stx ← if bang.isSome then
       `(tactic| dsimp!%$tk $(config)? $[only%$o]? $[[$args,*]]? $(loc)?)
     else
       `(tactic| dsimp%$tk $(config)? $[only%$o]? $[[$args,*]]? $(loc)?)
     let { ctx, simprocs, .. } ←
       withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
-    let usedSimps ← dsimpLocation' ctx simprocs <| (loc.map expandLocation).getD (.targets #[] true)
-    let stx ← mkSimpCallStx stx usedSimps
+    let stats ← dsimpLocation' ctx simprocs <| (loc.map expandLocation).getD (.targets #[] true)
+    let stx ← mkSimpCallStx stx stats.usedTheorems
     addSuggestion tk stx (origSpan? := ← getRef)
+    return stats.diag
   | _ => throwUnsupportedSyntax

src/Lean/Elab/Tactic/Simpa.lean

@@ -31,7 +31,7 @@ deriving instance Repr for UseImplicitLambdaResult
 @[builtin_tactic Lean.Parser.Tactic.simpa] def evalSimpa : Tactic := fun stx => do
   match stx with
   | `(tactic| simpa%$tk $[?%$squeeze]? $[!%$unfold]? $(cfg)? $(disch)? $[only%$only]?
-        $[[$args,*]]? $[using $usingArg]?) => Elab.Tactic.focus do
+        $[[$args,*]]? $[using $usingArg]?) => Elab.Tactic.focus do withSimpDiagnostics do
     let stx ← `(tactic| simp $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]?)
     let { ctx, simprocs, dischargeWrapper } ←
       withMainContext <| mkSimpContext stx (eraseLocal := false)
@@ -39,12 +39,13 @@ deriving instance Repr for UseImplicitLambdaResult
     -- TODO: have `simpa` fail if it doesn't use `simp`.
     let ctx := { ctx with config := { ctx.config with failIfUnchanged := false } }
     dischargeWrapper.with fun discharge? => do
-      let (some (_, g), usedSimps) ← simpGoal (← getMainGoal) ctx (simprocs := simprocs)
+      let (some (_, g), stats) ← simpGoal (← getMainGoal) ctx (simprocs := simprocs)
           (simplifyTarget := true) (discharge? := discharge?)
         | if getLinterUnnecessarySimpa (← getOptions) then
             logLint linter.unnecessarySimpa (← getRef) "try 'simp' instead of 'simpa'"
+          return {}
       g.withContext do
-      let usedSimps ← if let some stx := usingArg then
+      let stats ← if let some stx := usingArg then
         setGoals [g]
         g.withContext do
         let e ← Tactic.elabTerm stx none (mayPostpone := true)
@@ -52,8 +53,8 @@ deriving instance Repr for UseImplicitLambdaResult
           pure (h, g)
         else
           (← g.assert `h (← inferType e) e).intro1
-        let (result?, usedSimps) ← simpGoal g ctx (simprocs := simprocs) (fvarIdsToSimp := #[h])
-          (simplifyTarget := false) (usedSimps := usedSimps) (discharge? := discharge?)
+        let (result?, stats) ← simpGoal g ctx (simprocs := simprocs) (fvarIdsToSimp := #[h])
+          (simplifyTarget := false) (stats := stats) (discharge? := discharge?)
         match result? with
         | some (xs, g) =>
           let h := match xs with | #[h] | #[] => h | _ => unreachable!
@@ -66,18 +67,18 @@ deriving instance Repr for UseImplicitLambdaResult
             if (← getLCtx).getRoundtrippingUserName? h |>.isSome then
               logLint linter.unnecessarySimpa (← getRef)
                 m!"try 'simp at {Expr.fvar h}' instead of 'simpa using {Expr.fvar h}'"
-        pure usedSimps
+        pure stats
       else if let some ldecl := (← getLCtx).findFromUserName? `this then
-        if let (some (_, g), usedSimps) ← simpGoal g ctx (simprocs := simprocs)
-            (fvarIdsToSimp := #[ldecl.fvarId]) (simplifyTarget := false) (usedSimps := usedSimps)
+        if let (some (_, g), stats) ← simpGoal g ctx (simprocs := simprocs)
+            (fvarIdsToSimp := #[ldecl.fvarId]) (simplifyTarget := false) (stats := stats)
             (discharge? := discharge?) then
-          g.assumption; pure usedSimps
+          g.assumption; pure stats
         else
-          pure usedSimps
+          pure stats
       else
-        g.assumption; pure usedSimps
+        g.assumption; pure stats
       if tactic.simp.trace.get (← getOptions) || squeeze.isSome then
-        let stx ← match ← mkSimpOnly stx usedSimps with
+        let stx ← match ← mkSimpOnly stx stats.usedTheorems with
           | `(tactic| simp $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]?) =>
             if unfold.isSome then
               `(tactic| simpa! $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
@@ -85,6 +86,7 @@ deriving instance Repr for UseImplicitLambdaResult
               `(tactic| simpa $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
           | _ => unreachable!
         TryThis.addSuggestion tk stx (origSpan? := ← getRef)
+      return stats.diag
     | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Tactic.Simpa

src/Lean/Meta/Diagnostics.lean

@@ -10,57 +10,82 @@ import Lean.Meta.Instances
 
 namespace Lean.Meta
 
-private def collectAboveThreshold (counters : PHashMap Name Nat) (threshold : Nat) (p : Name → Bool) : Array (Name × Nat) := Id.run do
+def collectAboveThreshold [BEq α] [Hashable α] (counters : PHashMap α Nat) (threshold : Nat) (p : α → Bool) (lt : α → α → Bool) : Array (α × Nat) := Id.run do
   let mut r := #[]
   for (declName, counter) in counters do
     if counter > threshold then
     if p declName then
       r := r.push (declName, counter)
-  return r.qsort fun (d₁, c₁) (d₂, c₂) => if c₁ == c₂ then d₁.lt d₂ else c₁ > c₂
+  return r.qsort fun (d₁, c₁) (d₂, c₂) => if c₁ == c₂ then lt d₁ d₂ else c₁ > c₂
 
-private def mkMessageBodyFor? (counters : PHashMap Name Nat) (threshold : Nat) (p : Name → Bool := fun _ => true) : MetaM (Option MessageData) := do
-  let entries := collectAboveThreshold counters threshold p
-  if entries.isEmpty then
-    return none
-  else
-    let mut m := MessageData.nil
-    for (declName, counter) in entries do
-      unless m matches .nil do
-        m := m ++ "\n"
-      m := m ++ m!"{MessageData.ofConst (← mkConstWithLevelParams declName)} ↦ {counter}"
-    return some m
-
-private def appendOptMessageData (m : MessageData) (header : String) (m? : Option MessageData) : MessageData :=
-  if let some m' := m? then
-    if m matches .nil then
-      header ++ indentD m'
+def subCounters [BEq α] [Hashable α] (newCounters oldCounters : PHashMap α Nat) : PHashMap α Nat := Id.run do
+  let mut result := {}
+  for (a, counterNew) in newCounters do
+    if let some counterOld := oldCounters.find? a then
+      result := result.insert a (counterNew - counterOld)
     else
-      m ++ "\n" ++ header ++ indentD m'
+      result := result.insert a counterNew
+  return result
+
+structure DiagSummary where
+  data  : Array MessageData := #[]
+  max   : Nat := 0
+  deriving Inhabited
+
+def DiagSummary.isEmpty (s : DiagSummary) : Bool :=
+  s.data.isEmpty
+
+def mkDiagSummary (counters : PHashMap Name Nat) (threshold : Nat) (p : Name → Bool := fun _ => true) : MetaM DiagSummary := do
+  let entries := collectAboveThreshold counters threshold p Name.lt
+  if entries.isEmpty then
+    return {}
   else
+    let mut data := #[]
+    for (declName, counter) in entries do
+      data := data.push m!"{if data.isEmpty then "  " else "\n"}{MessageData.ofConst (← mkConstWithLevelParams declName)} ↦ {counter}"
+    return { data, max := entries[0]!.2 }
+
+def mkDiagSummaryForUnfolded (counters : PHashMap Name Nat) (instances := false) : MetaM DiagSummary := do
+  let threshold := diagnostics.threshold.get (← getOptions)
+  let env ← getEnv
+  mkDiagSummary counters threshold fun declName =>
+    getReducibilityStatusCore env declName matches .semireducible
+    && isInstanceCore env declName == instances
+
+def mkDiagSummaryForUnfoldedReducible (counters : PHashMap Name Nat) : MetaM DiagSummary := do
+  let threshold := diagnostics.threshold.get (← getOptions)
+  let env ← getEnv
+  mkDiagSummary counters threshold fun declName =>
+    getReducibilityStatusCore env declName matches .reducible
+
+def mkDiagSummaryForUsedInstances : MetaM DiagSummary := do
+  let threshold := diagnostics.threshold.get (← getOptions)
+  mkDiagSummary (← get).diag.heuristicCounter threshold
+
+def appendSection (m : MessageData) (cls : Name) (header : String) (s : DiagSummary) : MessageData :=
+  if s.isEmpty then
     m
+  else
+    let header := s!"{header} (max: {s.max}, num: {s.data.size}):"
+    m ++ .trace { cls } header s.data
 
 def reportDiag : MetaM Unit := do
   if (← isDiagnosticsEnabled) then
     let threshold := diagnostics.threshold.get (← getOptions)
-    let mut m := MessageData.nil
-    let env ← getEnv
-    let unfoldDefault? ← mkMessageBodyFor? (← get).diag.unfoldCounter threshold fun declName =>
-      getReducibilityStatusCore env declName matches .semireducible
-      && !isInstanceCore env declName
-    let unfoldInstance? ← mkMessageBodyFor? (← get).diag.unfoldCounter threshold fun declName =>
-      getReducibilityStatusCore env declName matches .semireducible
-      && isInstanceCore env declName
-    let unfoldReducible? ← mkMessageBodyFor? (← get).diag.unfoldCounter threshold fun declName =>
-      getReducibilityStatusCore env declName matches .reducible
-    let heu? ← mkMessageBodyFor? (← get).diag.heuristicCounter threshold
-    let inst? ← mkMessageBodyFor? (← get).diag.instanceCounter threshold
-    if unfoldDefault?.isSome || unfoldInstance?.isSome || unfoldReducible?.isSome || heu?.isSome || inst?.isSome then
-      m := appendOptMessageData m "unfolded declarations:" unfoldDefault?
-      m := appendOptMessageData m "unfolded instances:" unfoldInstance?
-      m := appendOptMessageData m "unfolded reducible declarations:" unfoldReducible?
-      m := appendOptMessageData m "used instances:" inst?
-      m := appendOptMessageData m "`isDefEq` heuristic:" heu?
-      m := m ++ "\nuse `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
+    let unfoldCounter := (← get).diag.unfoldCounter
+    let unfoldDefault ← mkDiagSummaryForUnfolded unfoldCounter
+    let unfoldInstance ← mkDiagSummaryForUnfolded unfoldCounter (instances := true)
+    let unfoldReducible ← mkDiagSummaryForUnfoldedReducible unfoldCounter
+    let heu ← mkDiagSummary (← get).diag.heuristicCounter threshold
+    let inst ← mkDiagSummaryForUsedInstances
+    unless unfoldDefault.isEmpty && unfoldInstance.isEmpty && unfoldReducible.isEmpty && heu.isEmpty && inst.isEmpty do
+      let m := MessageData.nil
+      let m := appendSection m `reduction "unfolded declarations" unfoldDefault
+      let m := appendSection m `reduction "unfolded instances" unfoldInstance
+      let m := appendSection m `reduction "unfolded reducible declarations" unfoldReducible
+      let m := appendSection m `type_class "used instances" inst
+      let m := appendSection m `def_eq "heuristic for solving `f a =?= f b`" heu
+      let m := m ++ "use `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
       logInfo m
 
 end Lean.Meta

src/Lean/Meta/Tactic/Simp.lean

@@ -14,6 +14,7 @@ import Lean.Meta.Tactic.Simp.Simproc
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs
 import Lean.Meta.Tactic.Simp.RegisterCommand
 import Lean.Meta.Tactic.Simp.Attr
+import Lean.Meta.Tactic.Simp.Diagnostics
 
 namespace Lean
 

src/Lean/Meta/Tactic/Simp/Diagnostics.lean

@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Diagnostics
+import Lean.Meta.Tactic.Simp.Types
+
+namespace Lean.Meta.Simp
+
+def mkSimpDiagSummary (counters : PHashMap Origin Nat) (usedCounters? : Option (PHashMap Origin Nat) := none) : MetaM DiagSummary := do
+  let threshold := diagnostics.threshold.get (← getOptions)
+  let entries := collectAboveThreshold counters threshold (fun _ => true) (lt := (· < ·))
+  if entries.isEmpty then
+    return {}
+  else
+    let mut data := #[]
+    for (thmId, counter) in entries do
+      let key ← match thmId with
+        | .decl declName _ _ =>
+          if (← getEnv).contains declName then
+            pure m!"{MessageData.ofConst (← mkConstWithLevelParams declName)}"
+          else
+            pure m!"{declName} (builtin simproc)"
+        | .fvar fvarId => pure m!"{mkFVar fvarId}"
+        | _ => pure thmId.key
+      let usedMsg ← if let some usedCounters := usedCounters? then
+        if let some c := usedCounters.find? thmId then pure s!", succeeded: {c}" else pure s!" {crossEmoji}" -- not used
+      else
+        pure ""
+      data := data.push m!"{if data.isEmpty then "  " else "\n"}{key} ↦ {counter}{usedMsg}"
+    return { data, max := entries[0]!.2 }
+
+def reportDiag (diag : Simp.Diagnostics) (diagOrig : Meta.Diagnostics) : MetaM Unit := do
+  if (← isDiagnosticsEnabled) then
+    let used ← mkSimpDiagSummary diag.usedThmCounter
+    let tried ← mkSimpDiagSummary diag.triedThmCounter diag.usedThmCounter
+    let unfoldCounter := subCounters (← get).diag.unfoldCounter diagOrig.unfoldCounter
+    let unfoldDefault ← mkDiagSummaryForUnfolded unfoldCounter
+    let unfoldInstance ← mkDiagSummaryForUnfolded unfoldCounter (instances := true)
+    let unfoldReducible ← mkDiagSummaryForUnfoldedReducible unfoldCounter
+    unless used.isEmpty && tried.isEmpty && unfoldDefault.isEmpty && unfoldInstance.isEmpty && unfoldReducible.isEmpty do
+      let m := MessageData.nil
+      let m := appendSection m `simp "used theorems" used
+      let m := appendSection m `simp "tried theorems" tried
+      let m := appendSection m `reduction "unfolded declarations" unfoldDefault
+      let m := appendSection m `reduction "unfolded instances" unfoldInstance
+      let m := appendSection m `reduction "unfolded reducible declarations" unfoldReducible
+      let m := m ++ "use `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
+      logInfo m
+
+end Lean.Meta.Simp

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

@@ -8,6 +8,7 @@ import Lean.Meta.Transform
 import Lean.Meta.Tactic.Replace
 import Lean.Meta.Tactic.UnifyEq
 import Lean.Meta.Tactic.Simp.Rewrite
+import Lean.Meta.Tactic.Simp.Diagnostics
 import Lean.Meta.Match.Value
 
 namespace Lean.Meta
@@ -655,60 +656,74 @@ where
 @[inline] def withSimpConfig (ctx : Context) (x : MetaM α) : MetaM α :=
   withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible x
 
-def main (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods : Methods := {}) : MetaM (Result × UsedSimps) := do
+def main (e : Expr) (ctx : Context) (stats : Stats := {}) (methods : Methods := {}) : MetaM (Result × Stats) := do
   let ctx := { ctx with config := (← ctx.config.updateArith) }
-  withSimpConfig ctx do withCatchingRuntimeEx do
+  withSimpConfig ctx do
+    let (r, s) ← simpMain e methods.toMethodsRef ctx |>.run { stats with }
+    trace[Meta.Tactic.simp.numSteps] "{s.numSteps}"
+    return (r, { s with })
+where
+  simpMain (e : Expr) : SimpM Result := withCatchingRuntimeEx do
+    let origDiag := (← getThe Meta.State).diag
     try
-      withoutCatchingRuntimeEx do
-        let (r, s) ← simp e methods.toMethodsRef ctx |>.run { usedTheorems := usedSimps }
-        trace[Meta.Tactic.simp.numSteps] "{s.numSteps}"
-        return (r, s.usedTheorems)
+      withoutCatchingRuntimeEx <| simp e
     catch ex =>
-      if ex.isRuntime then throwNestedTacticEx `simp ex else throw ex
+      reportDiag (← get).diag origDiag
+      if ex.isRuntime then
+        throwNestedTacticEx `simp ex
+      else
+        throw ex
 
-def dsimpMain (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods : Methods := {}) : MetaM (Expr × UsedSimps) := do
-  withSimpConfig ctx do withCatchingRuntimeEx do
+def dsimpMain (e : Expr) (ctx : Context) (stats : Stats := {}) (methods : Methods := {}) : MetaM (Expr × Stats) := do
+  withSimpConfig ctx do
+    let (r, s) ← dsimpMain e methods.toMethodsRef ctx |>.run { stats with }
+    pure (r, { s with })
+where
+  dsimpMain (e : Expr) : SimpM Expr := withCatchingRuntimeEx do
+    let origDiag := (← getThe Meta.State).diag
     try
-      withoutCatchingRuntimeEx do
-        let (r, s) ← dsimp e methods.toMethodsRef ctx |>.run { usedTheorems := usedSimps }
-        pure (r, s.usedTheorems)
+      withoutCatchingRuntimeEx <| dsimp e
     catch ex =>
-      if ex.isRuntime then throwNestedTacticEx `dsimp ex else throw ex
+      reportDiag (← get).diag origDiag
+      if ex.isRuntime then
+        throwNestedTacticEx `simp ex
+      else
+        throw ex
 
 end Simp
-open Simp (UsedSimps SimprocsArray)
+open Simp (SimprocsArray Stats)
 
 def simp (e : Expr) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
-    (usedSimps : UsedSimps := {}) : MetaM (Simp.Result × UsedSimps) := do profileitM Exception "simp" (← getOptions) do
+    (stats : Stats := {}) : MetaM (Simp.Result × Stats) := do profileitM Exception "simp" (← getOptions) do
   match discharge? with
-  | none   => Simp.main e ctx usedSimps (methods := Simp.mkDefaultMethodsCore simprocs)
-  | some d => Simp.main e ctx usedSimps (methods := Simp.mkMethods simprocs d)
+  | none   => Simp.main e ctx stats (methods := Simp.mkDefaultMethodsCore simprocs)
+  | some d => Simp.main e ctx stats (methods := Simp.mkMethods simprocs d)
 
 def dsimp (e : Expr) (ctx : Simp.Context) (simprocs : SimprocsArray := #[])
-    (usedSimps : UsedSimps := {}) : MetaM (Expr × UsedSimps) := do profileitM Exception "dsimp" (← getOptions) do
-  Simp.dsimpMain e ctx usedSimps (methods := Simp.mkDefaultMethodsCore simprocs )
+    (stats : Stats := {}) : MetaM (Expr × Stats) := do profileitM Exception "dsimp" (← getOptions) do
+  Simp.dsimpMain e ctx stats (methods := Simp.mkDefaultMethodsCore simprocs )
 
 /-- See `simpTarget`. This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
 def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
-    (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
+    (mayCloseGoal := true) (stats : Stats := {}) : MetaM (Option MVarId × Stats) := do
   let target ← instantiateMVars (← mvarId.getType)
-  let (r, usedSimps) ← simp target ctx simprocs discharge? usedSimps
+  let (r, stats) ← simp target ctx simprocs discharge? stats
   if mayCloseGoal && r.expr.isTrue then
     match r.proof? with
     | some proof => mvarId.assign (← mkOfEqTrue proof)
     | none => mvarId.assign (mkConst ``True.intro)
-    return (none, usedSimps)
+    return (none, stats)
   else
-    return (← applySimpResultToTarget mvarId target r, usedSimps)
+    return (← applySimpResultToTarget mvarId target r, stats)
 
 /--
   Simplify the given goal target (aka type). Return `none` if the goal was closed. Return `some mvarId'` otherwise,
   where `mvarId'` is the simplified new goal. -/
 def simpTarget (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
-    (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) :=
+    (mayCloseGoal := true) (stats : Stats := {}) : MetaM (Option MVarId × Stats) :=
   mvarId.withContext do
     mvarId.checkNotAssigned `simp
-    simpTargetCore mvarId ctx simprocs discharge? mayCloseGoal usedSimps
+    simpTargetCore mvarId ctx simprocs discharge? mayCloseGoal stats
 
 /--
   Apply the result `r` for `prop` (which is inhabited by `proof`). Return `none` if the goal was closed. Return `some (proof', prop')`
@@ -740,9 +755,9 @@ def applySimpResultToFVarId (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result
 
   This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
 def simpStep (mvarId : MVarId) (proof : Expr) (prop : Expr) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
-    (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option (Expr × Expr) × UsedSimps) := do
-  let (r, usedSimps) ← simp prop ctx simprocs discharge? usedSimps
-  return (← applySimpResultToProp mvarId proof prop r (mayCloseGoal := mayCloseGoal), usedSimps)
+    (mayCloseGoal := true) (stats : Stats := {}) : MetaM (Option (Expr × Expr) × Stats) := do
+  let (r, stats) ← simp prop ctx simprocs discharge? stats
+  return (← applySimpResultToProp mvarId proof prop r (mayCloseGoal := mayCloseGoal), stats)
 
 def applySimpResultToLocalDeclCore (mvarId : MVarId) (fvarId : FVarId) (r : Option (Expr × Expr)) : MetaM (Option (FVarId × MVarId)) := do
   match r with
@@ -773,99 +788,99 @@ def applySimpResultToLocalDecl (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Res
     applySimpResultToLocalDeclCore mvarId fvarId (← applySimpResultToFVarId mvarId fvarId r mayCloseGoal)
 
 def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
-    (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option (FVarId × MVarId) × UsedSimps) := do
+    (mayCloseGoal := true) (stats : Stats := {}) : MetaM (Option (FVarId × MVarId) × Stats) := do
   mvarId.withContext do
     mvarId.checkNotAssigned `simp
     let type ← instantiateMVars (← fvarId.getType)
-    let (r, usedSimps) ← simpStep mvarId (mkFVar fvarId) type ctx simprocs discharge? mayCloseGoal usedSimps
-    return (← applySimpResultToLocalDeclCore mvarId fvarId r, usedSimps)
+    let (r, stats) ← simpStep mvarId (mkFVar fvarId) type ctx simprocs discharge? mayCloseGoal stats
+    return (← applySimpResultToLocalDeclCore mvarId fvarId r, stats)
 
 def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
     (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
-    (usedSimps : UsedSimps := {}) : MetaM (Option (Array FVarId × MVarId) × UsedSimps) := do
+    (stats : Stats := {}) : MetaM (Option (Array FVarId × MVarId) × Stats) := do
   mvarId.withContext do
     mvarId.checkNotAssigned `simp
     let mut mvarIdNew := mvarId
     let mut toAssert := #[]
     let mut replaced := #[]
-    let mut usedSimps := usedSimps
+    let mut stats := stats
     for fvarId in fvarIdsToSimp do
       let localDecl ← fvarId.getDecl
       let type ← instantiateMVars localDecl.type
       let ctx := { ctx with simpTheorems := ctx.simpTheorems.eraseTheorem (.fvar localDecl.fvarId) }
-      let (r, usedSimps') ← simp type ctx simprocs discharge? usedSimps
-      usedSimps := usedSimps'
+      let (r, stats') ← simp type ctx simprocs discharge? stats
+      stats := stats'
       match r.proof? with
       | some _ => match (← applySimpResultToProp mvarIdNew (mkFVar fvarId) type r) with
-        | none => return (none, usedSimps)
+        | none => return (none, stats)
         | some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value }
       | none =>
         if r.expr.isFalse then
           mvarIdNew.assign (← mkFalseElim (← mvarIdNew.getType) (mkFVar fvarId))
-          return (none, usedSimps)
+          return (none, stats)
         -- TODO: if there are no forwards dependencies we may consider using the same approach we used when `r.proof?` is a `some ...`
         -- Reason: it introduces a `mkExpectedTypeHint`
         mvarIdNew ← mvarIdNew.replaceLocalDeclDefEq fvarId r.expr
         replaced := replaced.push fvarId
     if simplifyTarget then
-      match (← simpTarget mvarIdNew ctx simprocs discharge? (usedSimps := usedSimps)) with
-      | (none, usedSimps') => return (none, usedSimps')
-      | (some mvarIdNew', usedSimps') => mvarIdNew := mvarIdNew'; usedSimps := usedSimps'
+      match (← simpTarget mvarIdNew ctx simprocs discharge? (stats := stats)) with
+      | (none, stats') => return (none, stats')
+      | (some mvarIdNew', stats') => mvarIdNew := mvarIdNew'; stats := stats'
     let (fvarIdsNew, mvarIdNew') ← mvarIdNew.assertHypotheses toAssert
     mvarIdNew := mvarIdNew'
     let toClear := fvarIdsToSimp.filter fun fvarId => !replaced.contains fvarId
     mvarIdNew ← mvarIdNew.tryClearMany toClear
     if ctx.config.failIfUnchanged && mvarId == mvarIdNew then
       throwError "simp made no progress"
-    return (some (fvarIdsNew, mvarIdNew), usedSimps)
+    return (some (fvarIdsNew, mvarIdNew), stats)
 
 def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
-    (usedSimps : UsedSimps := {}) : MetaM (TacticResultCNM × UsedSimps) := mvarId.withContext do
+    (stats : Stats := {}) : MetaM (TacticResultCNM × Stats) := mvarId.withContext do
   let mut ctx := ctx
   for h in (← getPropHyps) do
     let localDecl ← h.getDecl
     let proof  := localDecl.toExpr
     let simpTheorems ← ctx.simpTheorems.addTheorem (.fvar h) proof
     ctx := { ctx with simpTheorems }
-  match (← simpTarget mvarId ctx simprocs discharge? (usedSimps := usedSimps)) with
-  | (none, usedSimps) => return (TacticResultCNM.closed, usedSimps)
-  | (some mvarId', usedSimps') =>
+  match (← simpTarget mvarId ctx simprocs discharge? (stats := stats)) with
+  | (none, stats) => return (TacticResultCNM.closed, stats)
+  | (some mvarId', stats') =>
     if (← mvarId.getType) == (← mvarId'.getType) then
-      return (TacticResultCNM.noChange, usedSimps)
+      return (TacticResultCNM.noChange, stats)
     else
-      return (TacticResultCNM.modified mvarId', usedSimps')
+      return (TacticResultCNM.modified mvarId', stats')
 
 def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
-    (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
+    (stats : Stats := {}) : MetaM (Option MVarId × Stats) := do
    mvarId.withContext do
     mvarId.checkNotAssigned `simp
     let mut mvarIdNew := mvarId
-    let mut usedSimps : UsedSimps := usedSimps
+    let mut stats : Stats := stats
     for fvarId in fvarIdsToSimp do
       let type ← instantiateMVars (← fvarId.getType)
-      let (typeNew, usedSimps') ← dsimp type ctx simprocs
-      usedSimps := usedSimps'
+      let (typeNew, stats') ← dsimp type ctx simprocs
+      stats := stats'
       if typeNew.isFalse then
         mvarIdNew.assign (← mkFalseElim (← mvarIdNew.getType) (mkFVar fvarId))
-        return (none, usedSimps)
+        return (none, stats)
       if typeNew != type then
         mvarIdNew ← mvarIdNew.replaceLocalDeclDefEq fvarId typeNew
     if simplifyTarget then
       let target ← mvarIdNew.getType
-      let (targetNew, usedSimps') ← dsimp target ctx simprocs usedSimps
-      usedSimps := usedSimps'
+      let (targetNew, stats') ← dsimp target ctx simprocs stats
+      stats := stats'
       if targetNew.isTrue then
         mvarIdNew.assign (mkConst ``True.intro)
-        return (none, usedSimps)
+        return (none, stats)
       if let some (_, lhs, rhs) := targetNew.consumeMData.eq? then
         if (← withReducible <| isDefEq lhs rhs) then
           mvarIdNew.assign (← mkEqRefl lhs)
-          return (none, usedSimps)
+          return (none, stats)
       if target != targetNew then
         mvarIdNew ← mvarIdNew.replaceTargetDefEq targetNew
       pure () -- FIXME: bug in do notation if this is removed?
     if ctx.config.failIfUnchanged && mvarId == mvarIdNew then
       throwError "dsimp made no progress"
-    return (some mvarIdNew, usedSimps)
+    return (some mvarIdNew, stats)
 
 end Lean.Meta

src/Lean/Meta/Tactic/Simp/Rewrite.lean

@@ -109,6 +109,7 @@ where
       return false
 
 private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInfo) (val : Expr) (type : Expr) (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) : SimpM (Option Result) := do
+  recordTriedSimpTheorem thm.origin
   let rec go (e : Expr) : SimpM (Option Result) := do
     if (← isDefEq lhs e) then
       unless (← synthesizeArgs thm.origin bis xs) do

src/Lean/Meta/Tactic/Simp/SimpAll.lean

@@ -10,7 +10,7 @@ import Lean.Meta.Tactic.Simp.Main
 
 namespace Lean.Meta
 
-open Simp (UsedSimps SimprocsArray)
+open Simp (Stats SimprocsArray)
 
 namespace SimpAll
 
@@ -24,12 +24,13 @@ structure Entry where
   deriving Inhabited
 
 structure State where
-  modified  : Bool := false
-  mvarId    : MVarId
-  entries   : Array Entry := #[]
-  ctx       : Simp.Context
-  simprocs  : SimprocsArray
-  usedSimps : UsedSimps := {}
+  modified     : Bool := false
+  mvarId       : MVarId
+  entries      : Array Entry := #[]
+  ctx          : Simp.Context
+  simprocs     : SimprocsArray
+  usedTheorems : Simp.UsedSimps := {}
+  diag         : Simp.Diagnostics := {}
 
 abbrev M := StateRefT State MetaM
 
@@ -62,8 +63,8 @@ private partial def loop : M Bool := do
     -- We disable the current entry to prevent it to be simplified to `True`
     let simpThmsWithoutEntry := (← getSimpTheorems).eraseTheorem entry.id
     let ctx := { ctx with simpTheorems := simpThmsWithoutEntry }
-    let (r, usedSimps) ← simpStep (← get).mvarId entry.proof entry.type ctx simprocs (usedSimps := (← get).usedSimps)
-    modify fun s => { s with usedSimps }
+    let (r, stats) ← simpStep (← get).mvarId entry.proof entry.type ctx simprocs (stats := { (← get) with })
+    modify fun s => { s with usedTheorems := stats.usedTheorems, diag := stats.diag }
     match r with
     | none => return true -- closed the goal
     | some (proofNew, typeNew) =>
@@ -102,8 +103,8 @@ private partial def loop : M Bool := do
         }
   -- simplify target
   let mvarId := (← get).mvarId
-  let (r, usedSimps) ← simpTarget mvarId (← get).ctx simprocs (usedSimps := (← get).usedSimps)
-  modify fun s => { s with usedSimps }
+  let (r, stats) ← simpTarget mvarId (← get).ctx simprocs (stats := { (← get) with })
+  modify fun s => { s with usedTheorems := stats.usedTheorems, diag := stats.diag }
   match r with
   | none => return true
   | some mvarIdNew =>
@@ -143,12 +144,12 @@ def main : M (Option MVarId) := do
 
 end SimpAll
 
-def simpAll (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
+def simpAll (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (stats : Stats := {}) : MetaM (Option MVarId × Stats) := do
   mvarId.withContext do
-    let (r, s) ← SimpAll.main.run { mvarId, ctx, usedSimps, simprocs }
+    let (r, s) ← SimpAll.main.run { stats with mvarId, ctx, simprocs }
     if let .some mvarIdNew := r then
       if ctx.config.failIfUnchanged && mvarId == mvarIdNew then
         throwError "simp_all made no progress"
-    return (r, s.usedSimps)
+    return (r, { s with })
 
 end Lean.Meta

src/Lean/Meta/Tactic/Simp/SimpTheorems.lean

@@ -50,6 +50,9 @@ def Origin.key : Origin → Name
 
 instance : BEq Origin := ⟨(·.key == ·.key)⟩
 instance : Hashable Origin := ⟨(hash ·.key)⟩
+instance : LT Origin := ⟨(·.key.lt ·.key)⟩
+instance (a b : Origin) : Decidable (a < b) :=
+  inferInstanceAs (Decidable (a.key.lt b.key = true))
 
 /-
 Note: we want to use iota reduction when indexing instances. Otherwise,

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

@@ -98,11 +98,23 @@ def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool :=
 -- We should use `PHashMap` because we backtrack the contents of `UsedSimps`
 abbrev UsedSimps := PHashMap Origin Nat
 
+structure Diagnostics where
+  /-- Number of times each simp theorem has been used/applied. -/
+  usedThmCounter : PHashMap Origin Nat := {}
+  /-- Number of times each simp theorem has been tried. -/
+  triedThmCounter : PHashMap Origin Nat := {}
+  deriving Inhabited
+
 structure State where
   cache        : Cache := {}
   congrCache   : CongrCache := {}
   usedTheorems : UsedSimps := {}
   numSteps     : Nat := 0
+  diag         : Diagnostics := {}
+
+structure Stats where
+  usedTheorems : UsedSimps := {}
+  diag : Diagnostics := {}
 
 private opaque MethodsRefPointed : NonemptyType.{0}
 
@@ -118,6 +130,10 @@ opaque simp (e : Expr) : SimpM Result
 @[extern "lean_dsimp"]
 opaque dsimp (e : Expr) : SimpM Expr
 
+@[inline] def modifyDiag (f : Diagnostics → Diagnostics) : SimpM Unit := do
+  if (← isDiagnosticsEnabled) then
+    modify fun { cache, congrCache, usedTheorems, numSteps, diag } => { cache, congrCache, usedTheorems, numSteps, diag := f diag }
+
 /--
 Result type for a simplification procedure. We have `pre` and `post` simplication procedures.
 -/
@@ -291,7 +307,15 @@ Save current cache, reset it, execute `x`, and then restore original cache.
 @[inline] def withDischarger (discharge? : Expr → SimpM (Option Expr)) (x : SimpM α) : SimpM α :=
   withFreshCache <| withReader (fun r => { MethodsRef.toMethods r with discharge? }.toMethodsRef) x
 
+def recordTriedSimpTheorem (thmId : Origin) : SimpM Unit := do
+  modifyDiag fun { usedThmCounter, triedThmCounter } =>
+    let cNew := if let some c := triedThmCounter.find? thmId then c + 1 else 1
+    { usedThmCounter, triedThmCounter := triedThmCounter.insert thmId cNew }
+
 def recordSimpTheorem (thmId : Origin) : SimpM Unit := do
+  modifyDiag fun { usedThmCounter, triedThmCounter } =>
+    let cNew := if let some c := usedThmCounter.find? thmId then c + 1 else 1
+    { usedThmCounter := usedThmCounter.insert thmId cNew, triedThmCounter }
   /-
   If `thmId` is an equational theorem (e.g., `foo.eq_1`), we should record `foo` instead.
   See issue #3547.

tests/lean/906.lean.expected.out

@@ -1,3 +1,5 @@
 906.lean:2:4-2:15: warning: declaration uses 'sorry'
 906.lean:14:2-14:28: error: tactic 'simp' failed, nested error:
-maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)
+maximum recursion depth has been reached
+use `set_option maxRecDepth <num>` to increase limit
+use `set_option diagnostics true` to get diagnostic information

tests/lean/exceptionalTrace.lean.expected.out

@@ -1,4 +1,6 @@
-exceptionalTrace.lean:7:0-7:13: error: maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)
+exceptionalTrace.lean:7:0-7:13: error: maximum recursion depth has been reached
+use `set_option maxRecDepth <num>` to increase limit
+use `set_option diagnostics true` to get diagnostic information
 [Elab.step] expected type: <not-available>, term
     rt + 1
   [Elab.step] expected type: <not-available>, term

tests/lean/run/diagRec.lean

@@ -7,15 +7,16 @@ termination_by n
 /--
 info: 89
 ---
-info: unfolded declarations:
-  Nat.rec ↦ 407
+info: [reduction] unfolded declarations (max: 407, num: 3):
+    Nat.rec ↦ 407
+  ⏎
   Or.rec ↦ 144
-  Acc.rec ↦ 108
-unfolded reducible declarations:
-  Nat.casesOn ↦ 352
+  ⏎
+  Acc.rec ↦ 108[reduction] unfolded reducible declarations (max: 352, num: 3):
+    Nat.casesOn ↦ 352
+  ⏎
   Or.casesOn ↦ 144
-  PProd.fst ↦ 126
-use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+   PProd.fst ↦ 126use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 set_option diagnostics true in

tests/lean/run/isDefEqProjIssue.lean

@@ -51,7 +51,9 @@ where
     val.x
 
 /--
-error: (deterministic) timeout at 'whnf', maximum number of heartbeats (400) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
+error: (deterministic) timeout at `whnf`, maximum number of heartbeats (400) has been reached
+use `set_option maxHeartbeats <num>` to set the limit
+use `set_option diagnostics true` to get diagnostic information
 -/
 #guard_msgs in
 set_option backward.isDefEq.lazyWhnfCore false in

tests/lean/run/simpDiag.lean

@@ -0,0 +1,108 @@
+opaque q : Nat → Nat
+def f (x : Nat) : Nat :=
+  match x with
+  | 0 => 1
+  | x+1 => q (f x)
+
+theorem f_eq : f (x + 1) = q (f x) := rfl
+axiom q_eq (x : Nat) : q x = x
+
+/--
+info: [simp] used theorems (max: 50, num: 2):
+    f_eq ↦ 50
+  ⏎
+  q_eq ↦ 50[simp] tried theorems (max: 101, num: 2):
+    f_eq ↦ 101, succeeded: 50
+   q_eq ↦ 50, succeeded: 50use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+-/
+#guard_msgs in
+example : f (x + 50) = f x := by
+  set_option diagnostics true in
+  simp [f_eq, q_eq]
+
+example : f (x + 50) = f x := by
+  set_option diagnostics true in
+  simp [f_eq, q_eq]
+
+def ack : Nat → Nat → Nat
+  | 0,   y   => y+1
+  | x+1, 0   => ack x 1
+  | x+1, y+1 => ack x (ack (x+1) y)
+
+/--
+info: [simp] used theorems (max: 1201, num: 3):
+    ack.eq_3 ↦ 1201
+  ⏎
+  Nat.reduceAdd (builtin simproc) ↦ 771
+  ⏎
+  ack.eq_1 ↦ 768[simp] tried theorems (max: 1974, num: 2):
+    ack.eq_3 ↦ 1974, succeeded: 1201
+  ⏎
+  ack.eq_1 ↦ 768, succeeded: 768use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+---
+error: tactic 'simp' failed, nested error:
+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 in
+example : ack 4 4 = x := by
+  set_option diagnostics true in
+  simp [ack.eq_2, ack.eq_1, ack.eq_3]
+
+/--
+info: [simp] used theorems (max: 22, num: 5):
+    ack.eq_3 ↦ 22
+  ⏎
+  Nat.reduceAdd (builtin simproc) ↦ 14
+  ⏎
+  ack.eq_1 ↦ 11
+  ⏎
+  ack.eq_2 ↦ 4
+  ⏎
+  Nat.zero_add ↦ 1[simp] tried theorems (max: 38, num: 4):
+    ack.eq_3 ↦ 38, succeeded: 22
+  ⏎
+  ack.eq_1 ↦ 11, succeeded: 11
+  ⏎
+  ack.eq_2 ↦ 4, succeeded: 4
+  ⏎
+  Nat.zero_add ↦ 1, succeeded: 1[reduction] unfolded reducible declarations (max: 7, num: 1):
+    outParam ↦ 7use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+---
+error: tactic 'simp' failed, nested error:
+(deterministic) timeout at `whnf`, maximum number of heartbeats (500) has been reached
+use `set_option maxHeartbeats <num>` to set the limit
+use `set_option diagnostics true` to get diagnostic information
+-/
+#guard_msgs in
+set_option maxHeartbeats 500 in
+example : ack 4 4 = x := by
+  set_option diagnostics true in
+  set_option diagnostics.threshold 0 in
+  simp [ack.eq_2, ack.eq_1, ack.eq_3]
+
+@[reducible] def h (x : Nat) :=
+  match x with
+  | 0 => 10
+  | x + 1 => h x
+
+opaque q1 : Nat → Nat → Prop
+@[simp] axiom q1_ax (x : Nat) : q1 x 10
+
+/--
+info: [simp] used theorems (max: 1, num: 1):
+    q1_ax ↦ 1[simp] tried theorems (max: 1, num: 1):
+    q1_ax ↦ 1, succeeded: 1[reduction] unfolded declarations (max: 246, num: 2):
+    Nat.rec ↦ 246
+  ⏎
+  OfNat.ofNat ↦ 24[reduction] unfolded instances (max: 12, num: 1):
+    instOfNatNat ↦ 12[reduction] unfolded reducible declarations (max: 246, num: 2):
+    h ↦ 246
+   Nat.casesOn ↦ 246use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+-/
+#guard_msgs in
+example : q1 x (h 40) := by
+  set_option diagnostics true in
+  set_option diagnostics.threshold 0 in
+  simp

tests/lean/tcloop.lean.expected.out

@@ -1,3 +1,5 @@
 tcloop.lean:14:2-14:15: error: failed to synthesize
   B Nat
-(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)
+(deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached
+use `set_option synthInstance.maxHeartbeats <num>` to set the limit
+use `set_option diagnostics true` to get diagnostic information