chore: wrap diagnostic results in MessageData.traces (#4897)

Currently, the messages in the diagnostic summaries are created by
appending interpolated strings. We wrap these in `.trace`'s, and the
results are better formatted when expanding child nodes in the info
view. Particularly, the latter diagnostic summaries remain on their own
lines flush to the left instead of on the same line directly adjacent to
the last child node.

src/Lean/Meta/Diagnostics.lean

@@ -35,38 +35,38 @@ structure DiagSummary where
 def DiagSummary.isEmpty (s : DiagSummary) : Bool :=
   s.data.isEmpty
 
-def mkDiagSummary (counters : PHashMap Name Nat) (p : Name → Bool := fun _ => true) : MetaM DiagSummary := do
+def mkDiagSummary (cls : Name) (counters : PHashMap Name Nat) (p : Name → Bool := fun _ => true) : MetaM DiagSummary := do
   let threshold := diagnostics.threshold.get (← getOptions)
   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}"
+      data := data.push <| .trace { cls } m!"{MessageData.ofConst (← mkConstWithLevelParams declName)} ↦ {counter}" #[]
     return { data, max := entries[0]!.2 }
 
 def mkDiagSummaryForUnfolded (counters : PHashMap Name Nat) (instances := false) : MetaM DiagSummary := do
   let env ← getEnv
-  mkDiagSummary counters fun declName =>
+  mkDiagSummary `reduction counters fun declName =>
     getReducibilityStatusCore env declName matches .semireducible
     && isInstanceCore env declName == instances
 
 def mkDiagSummaryForUnfoldedReducible (counters : PHashMap Name Nat) : MetaM DiagSummary := do
   let env ← getEnv
-  mkDiagSummary counters fun declName =>
+  mkDiagSummary `reduction counters fun declName =>
     getReducibilityStatusCore env declName matches .reducible
 
 def mkDiagSummaryForUsedInstances : MetaM DiagSummary := do
-  mkDiagSummary (← get).diag.instanceCounter
+  mkDiagSummary `type_class (← get).diag.instanceCounter
 
 def mkDiagSynthPendingFailure (failures : PHashMap Expr MessageData) : MetaM DiagSummary := do
   if failures.isEmpty then
     return {}
   else
     let mut data := #[]
     for (_, msg) in failures do
-      data := data.push m!"{if data.isEmpty then "  " else "\n"}{msg}"
+      data := data.push <| .trace { cls := `type_class } msg #[]
     return { data }
 
 /--
@@ -85,10 +85,10 @@ def reportDiag : MetaM Unit := do
     let unfoldDefault ← mkDiagSummaryForUnfolded unfoldCounter
     let unfoldInstance ← mkDiagSummaryForUnfolded unfoldCounter (instances := true)
     let unfoldReducible ← mkDiagSummaryForUnfoldedReducible unfoldCounter
-    let heu ← mkDiagSummary (← get).diag.heuristicCounter
+    let heu ← mkDiagSummary `def_eq (← get).diag.heuristicCounter
     let inst ← mkDiagSummaryForUsedInstances
     let synthPending ← mkDiagSynthPendingFailure (← get).diag.synthPendingFailures
-    let unfoldKernel ← mkDiagSummary (Kernel.getDiagnostics (← getEnv)).unfoldCounter
+    let unfoldKernel ← mkDiagSummary `kernel (Kernel.getDiagnostics (← getEnv)).unfoldCounter
     let m := MessageData.nil
     let m := appendSection m `reduction "unfolded declarations" unfoldDefault
     let m := appendSection m `reduction "unfolded instances" unfoldInstance

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

@@ -32,7 +32,7 @@ def mkSimpDiagSummary (counters : PHashMap Origin Nat) (usedCounters? : Option (
         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}"
+      data := data.push <| .trace { cls := `simp } m!"{key} ↦ {counter}{usedMsg}" #[]
     return { data, max := entries[0]!.2 }
 
 private def mkTheoremsWithBadKeySummary (thms : PArray SimpTheorem) : MetaM DiagSummary := do
@@ -41,15 +41,15 @@ private def mkTheoremsWithBadKeySummary (thms : PArray SimpTheorem) : MetaM Diag
   else
     let mut data := #[]
     for thm in thms do
-      data := data.push m!"{if data.isEmpty then "  " else "\n"}{← originToKey thm.origin}, key: {← DiscrTree.keysAsPattern thm.keys}"
+      data := data.push <| .trace { cls := `simp } m!"{← originToKey thm.origin}, key: {← DiscrTree.keysAsPattern thm.keys}" #[]
       pure ()
     return { data }
 
 def reportDiag (diag : Simp.Diagnostics) : MetaM Unit := do
   if (← isDiagnosticsEnabled) then
     let used ← mkSimpDiagSummary diag.usedThmCounter
     let tried ← mkSimpDiagSummary diag.triedThmCounter diag.usedThmCounter
-    let congr ← mkDiagSummary diag.congrThmCounter
+    let congr ← mkDiagSummary `simp diag.congrThmCounter
     let thmsWithBadKeys ← mkTheoremsWithBadKeySummary diag.thmsWithBadKeys
     unless used.isEmpty && tried.isEmpty && congr.isEmpty && thmsWithBadKeys.isEmpty do
       let m := MessageData.nil

tests/lean/run/3313.lean

@@ -37,7 +37,7 @@ set_option maxSynthPendingDepth 2 in
 
 /--
 info: [type_class] max synth pending failures (maxSynthPendingDepth: 1), use `set_option maxSynthPendingDepth <limit>`
-    AddCommGroup Ruse `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+  [type_class] AddCommGroup Ruse `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 ---
 error: failed to synthesize
   HasQuotient (Synonym (Synonym R)) (Submodule R (Synonym (Synonym R)))

tests/lean/run/4171.lean

@@ -530,8 +530,6 @@ def isoOfIso {M N : Mon_ C} (f : M.X ≅ N.X) : M ≅ N where
   hom := { hom := f.hom }
   inv := { hom := f.inv }
 
-
-
 @[simp]
 instance monMonoidalStruct : MonoidalCategoryStruct (Mon_ C) :=
   let tensorObj (M N : Mon_ C) : Mon_ C :=
@@ -717,7 +715,7 @@ example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
 
 /--
 info: [simp] theorems with bad keys
-    foo, key: @Quiver.Hom.unop _ _ _ _ (@Opposite.op (@Quiver.Hom _ _ _.1 _.1) _)use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+  [simp] foo, key: @Quiver.Hom.unop _ _ _ _ (@Opposite.op (@Quiver.Hom _ _ _.1 _.1) _)use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
@@ -736,7 +734,7 @@ attribute [simp] foo
 
 /--
 info: [simp] theorems with bad keys
-    foo, key: @Quiver.Hom.unop _ _ _ _ (@Opposite.op (@Quiver.Hom _ _ _.1 _.1) _)use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+  [simp] foo, key: @Quiver.Hom.unop _ _ _ _ (@Opposite.op (@Quiver.Hom _ _ _.1 _.1) _)use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where

tests/lean/run/ack.lean

@@ -6,26 +6,18 @@ termination_by a b => (a, b)
 
 /--
 info: [reduction] unfolded declarations (max: 1725, num: 4):
-    Nat.rec ↦ 1725
-  ⏎
-  Eq.rec ↦ 1114
-  ⏎
-  Acc.rec ↦ 1050
-  ⏎
-  PSigma.rec ↦ 513[reduction] unfolded reducible declarations (max: 1577, num: 3):
-    Nat.casesOn ↦ 1577
-  ⏎
-  Eq.ndrec ↦ 984
-  ⏎
-  PSigma.casesOn ↦ 513[kernel] unfolded declarations (max: 1193, num: 5):
-    Nat.casesOn ↦ 1193
-  ⏎
-  Nat.rec ↦ 1065
-  ⏎
-  Eq.ndrec ↦ 973
-  ⏎
-  Eq.rec ↦ 973
-   Acc.rec ↦ 754use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+  [reduction] Nat.rec ↦ 1725
+  [reduction] Eq.rec ↦ 1114
+  [reduction] Acc.rec ↦ 1050
+  [reduction] PSigma.rec ↦ 513[reduction] unfolded reducible declarations (max: 1577, num: 3):
+  [reduction] Nat.casesOn ↦ 1577
+  [reduction] Eq.ndrec ↦ 984
+  [reduction] PSigma.casesOn ↦ 513[kernel] unfolded declarations (max: 1193, num: 5):
+  [kernel] Nat.casesOn ↦ 1193
+  [kernel] Nat.rec ↦ 1065
+  [kernel] Eq.ndrec ↦ 973
+  [kernel] Eq.rec ↦ 973
+  [kernel] Acc.rec ↦ 754use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 unseal ack in
@@ -37,12 +29,10 @@ theorem ex : ack 3 2 = 29 :=
 
 /--
 info: [kernel] unfolded declarations (max: 1193, num: 4):
-    Nat.casesOn ↦ 1193
-  ⏎
-  Nat.rec ↦ 1065
-  ⏎
-  Eq.ndrec ↦ 973
-   Eq.rec ↦ 973use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+  [kernel] Nat.casesOn ↦ 1193
+  [kernel] Nat.rec ↦ 1065
+  [kernel] Eq.ndrec ↦ 973
+  [kernel] Eq.rec ↦ 973use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 set_option diagnostics true in

tests/lean/run/diagRec.lean

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

tests/lean/run/diagnostics.lean

@@ -10,19 +10,14 @@ set_option trace.Meta.debug true
 
 /--
 info: [reduction] unfolded declarations (max: 15, num: 6):
-    Nat.rec ↦ 15
-  ⏎
-  Add.add ↦ 10
-  ⏎
-  HAdd.hAdd ↦ 10
-  ⏎
-  Nat.add ↦ 10
-  ⏎
-  f ↦ 5
-  ⏎
-  OfNat.ofNat ↦ 5[reduction] unfolded instances (max: 5, num: 1):
-    instOfNatNat ↦ 5[reduction] unfolded reducible declarations (max: 15, num: 1):
-    Nat.casesOn ↦ 15use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+  [reduction] Nat.rec ↦ 15
+  [reduction] Add.add ↦ 10
+  [reduction] HAdd.hAdd ↦ 10
+  [reduction] Nat.add ↦ 10
+  [reduction] f ↦ 5
+  [reduction] OfNat.ofNat ↦ 5[reduction] unfolded instances (max: 5, num: 1):
+  [reduction] instOfNatNat ↦ 5[reduction] unfolded reducible declarations (max: 15, num: 1):
+  [reduction] Nat.casesOn ↦ 15use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 example : f (x + 5) = q (q (q (q (q (f x))))) :=
@@ -32,19 +27,14 @@ example : f (x + 5) = q (q (q (q (q (f x))))) :=
 
 /--
 info: [reduction] unfolded declarations (max: 15, num: 6):
-    Nat.rec ↦ 15
-  ⏎
-  Add.add ↦ 10
-  ⏎
-  HAdd.hAdd ↦ 10
-  ⏎
-  Nat.add ↦ 10
-  ⏎
-  f ↦ 5
-  ⏎
-  OfNat.ofNat ↦ 5[reduction] unfolded instances (max: 5, num: 1):
-    instOfNatNat ↦ 5[reduction] unfolded reducible declarations (max: 15, num: 1):
-    Nat.casesOn ↦ 15use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+  [reduction] Nat.rec ↦ 15
+  [reduction] Add.add ↦ 10
+  [reduction] HAdd.hAdd ↦ 10
+  [reduction] Nat.add ↦ 10
+  [reduction] f ↦ 5
+  [reduction] OfNat.ofNat ↦ 5[reduction] unfolded instances (max: 5, num: 1):
+  [reduction] instOfNatNat ↦ 5[reduction] unfolded reducible declarations (max: 15, num: 1):
+  [reduction] Nat.casesOn ↦ 15use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 example : f (x + 5) = q (q (q (q (q (f x))))) := by

tests/lean/run/simpDiag.lean

@@ -9,11 +9,10 @@ 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
+  [simp] f_eq ↦ 50
+  [simp] q_eq ↦ 50[simp] tried theorems (max: 101, num: 2):
+  [simp] f_eq ↦ 101, succeeded: 50
+  [simp] 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
@@ -31,14 +30,11 @@ def ack : Nat → Nat → Nat
 
 /--
 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: 1973, num: 2):
-    ack.eq_3 ↦ 1973, succeeded: 1201
-  ⏎
-  ack.eq_1 ↦ 768, succeeded: 768use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+  [simp] ack.eq_3 ↦ 1201
+  [simp] Nat.reduceAdd (builtin simproc) ↦ 771
+  [simp] ack.eq_1 ↦ 768[simp] tried theorems (max: 1973, num: 2):
+  [simp] ack.eq_3 ↦ 1973, succeeded: 1201
+  [simp] 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
@@ -97,15 +93,14 @@ opaque q1 : Nat → Nat → Prop
 
 /--
 info: [simp] used theorems (max: 1, num: 1):
-    q1_ax ↦ 1[simp] tried theorems (max: 1, num: 1):
-    q1_ax ↦ 1, succeeded: 1use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+  [simp] q1_ax ↦ 1[simp] tried theorems (max: 1, num: 1):
+  [simp] q1_ax ↦ 1, succeeded: 1use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 ---
 info: [reduction] unfolded declarations (max: 246, num: 2):
-    Nat.rec ↦ 246
-  ⏎
-  OfNat.ofNat ↦ 24[reduction] unfolded reducible declarations (max: 246, num: 2):
-    h ↦ 246
-   Nat.casesOn ↦ 246use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+  [reduction] Nat.rec ↦ 246
+  [reduction] OfNat.ofNat ↦ 24[reduction] unfolded reducible declarations (max: 246, num: 2):
+  [reduction] h ↦ 246
+  [reduction] Nat.casesOn ↦ 246use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 example : q1 x (h 40) := by