fix: add workaround for MessageData limitations

This PR adds a workaround for the discrepancy between Terminal/Emacs and VS Code when displaying info trees.

src/Lean/Meta/Diagnostics.lean

@@ -72,12 +72,12 @@ def mkDiagSynthPendingFailure (failures : PHashMap Expr MessageData) : MetaM Dia
 /--
 We use below that this returns `m` unchanged if `s.isEmpty`
 -/
-def appendSection (m : MessageData) (cls : Name) (header : String) (s : DiagSummary) (resultSummary := true) : MessageData :=
+def appendSection (m : Array MessageData) (cls : Name) (header : String) (s : DiagSummary) (resultSummary := true) : Array MessageData :=
   if s.isEmpty then
     m
   else
     let header := if resultSummary then s!"{header} (max: {s.max}, num: {s.data.size}):" else header
-    m ++ .trace { cls } header s.data
+    m.push <| .trace { cls } header s.data
 
 def reportDiag : MetaM Unit := do
   if (← isDiagnosticsEnabled) then
@@ -89,7 +89,7 @@ def reportDiag : MetaM Unit := do
     let inst ← mkDiagSummaryForUsedInstances
     let synthPending ← mkDiagSynthPendingFailure (← get).diag.synthPendingFailures
     let unfoldKernel ← mkDiagSummary `kernel (Kernel.getDiagnostics (← getEnv)).unfoldCounter
-    let m := MessageData.nil
+    let m := #[]
     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
@@ -99,8 +99,8 @@ def reportDiag : MetaM Unit := do
               synthPending (resultSummary := false)
     let m := appendSection m `def_eq "heuristic for solving `f a =?= f b`" heu
     let m := appendSection m `kernel "unfolded declarations" unfoldKernel
-    unless m matches .nil do
-      let m := m ++ "use `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
-      logInfo m
+    unless m.isEmpty do
+      let m := m.push "use `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
+      logInfo <| .trace { cls := `diag, collapsed := false } "Diagnostics" m
 
 end Lean.Meta

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

@@ -52,12 +52,12 @@ def reportDiag (diag : Simp.Diagnostics) : MetaM Unit := do
     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
+      let m := #[]
       let m := appendSection m `simp "used theorems" used
       let m := appendSection m `simp "tried theorems" tried
       let m := appendSection m `simp "tried congruence theorems" congr
       let m := appendSection m `simp "theorems with bad keys" thmsWithBadKeys (resultSummary := false)
-      let m := m ++ "use `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
-      logInfo m
+      let m := m.push <| "use `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
+      logInfo <| .trace { cls := `simp, collapsed := false } "Diagnostics" m
 
 end Lean.Meta.Simp

tests/lean/run/4171.lean

@@ -714,8 +714,10 @@ example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
 
 
 /--
-info: [simp] theorems with bad keys
-  [simp] foo, key: @Quiver.Hom.unop _ _ _ _ (@Opposite.op (@Quiver.Hom _ _ _.1 _.1) _)use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+info: [simp] Diagnostics
+  [simp] theorems with bad keys
+    [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
@@ -733,8 +735,10 @@ example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
 attribute [simp] foo
 
 /--
-info: [simp] theorems with bad keys
-  [simp] foo, key: @Quiver.Hom.unop _ _ _ _ (@Opposite.op (@Quiver.Hom _ _ _.1 _.1) _)use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+info: [simp] Diagnostics
+  [simp] theorems with bad keys
+    [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

@@ -5,21 +5,25 @@ def ack : Nat → Nat → Nat
 termination_by a b => (a, b)
 
 /--
-info: [reduction] unfolded declarations (max: 2567, num: 5):
-  [reduction] Nat.rec ↦ 2567
-  [reduction] Eq.rec ↦ 1517
-  [reduction] Acc.rec ↦ 1158
-  [reduction] Or.rec ↦ 770
-  [reduction] PSigma.rec ↦ 514[reduction] unfolded reducible declarations (max: 2337, num: 4):
-  [reduction] Nat.casesOn ↦ 2337
-  [reduction] Eq.ndrec ↦ 1307
-  [reduction] Or.casesOn ↦ 770
-  [reduction] PSigma.casesOn ↦ 514[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
+info: [diag] Diagnostics
+  [reduction] unfolded declarations (max: 2567, num: 5):
+    [reduction] Nat.rec ↦ 2567
+    [reduction] Eq.rec ↦ 1517
+    [reduction] Acc.rec ↦ 1158
+    [reduction] Or.rec ↦ 770
+    [reduction] PSigma.rec ↦ 514
+  [reduction] unfolded reducible declarations (max: 2337, num: 4):
+    [reduction] Nat.casesOn ↦ 2337
+    [reduction] Eq.ndrec ↦ 1307
+    [reduction] Or.casesOn ↦ 770
+    [reduction] PSigma.casesOn ↦ 514
+  [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 ↦ 754
+  use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 unseal ack in

tests/lean/run/diagRec.lean

@@ -7,12 +7,15 @@ termination_by n
 /--
 info: 89
 ---
-info: [reduction] unfolded declarations (max: 407, num: 3):
-  [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
+info: [diag] Diagnostics
+  [reduction] unfolded declarations (max: 407, num: 3):
+    [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 ↦ 144
+  use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 set_option diagnostics true in

tests/lean/run/diagnostics.lean

@@ -9,15 +9,19 @@ theorem f_eq : f (x + 1) = q (f x) := rfl
 set_option trace.Meta.debug true
 
 /--
-info: [reduction] unfolded declarations (max: 15, num: 6):
-  [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
+info: [diag] Diagnostics
+  [reduction] unfolded declarations (max: 15, num: 6):
+    [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 ↦ 15
+  use `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))))) :=
@@ -26,15 +30,19 @@ example : f (x + 5) = q (q (q (q (q (f x))))) :=
   rfl
 
 /--
-info: [reduction] unfolded declarations (max: 15, num: 6):
-  [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
+info: [diag] Diagnostics
+  [reduction] unfolded declarations (max: 15, num: 6):
+    [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 ↦ 15
+  use `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

@@ -8,11 +8,14 @@ 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):
-  [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
+info: [simp] Diagnostics
+  [simp] used theorems (max: 50, num: 2):
+    [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: 50
+  use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 example : f (x + 50) = f x := by
@@ -29,12 +32,15 @@ def ack : Nat → Nat → Nat
   | x+1, y+1 => ack x (ack (x+1) y)
 
 /--
-info: [simp] used theorems (max: 1201, num: 3):
-  [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
+info: [simp] Diagnostics
+  [simp] used theorems (max: 1201, num: 3):
+    [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: 768
+  use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 ---
 error: tactic 'simp' failed, nested error:
 maximum recursion depth has been reached
@@ -92,15 +98,21 @@ opaque q1 : Nat → Nat → Prop
 @[simp] axiom q1_ax (x : Nat) : q1 x 10
 
 /--
-info: [simp] used theorems (max: 1, num: 1):
-  [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: [simp] Diagnostics
+  [simp] used theorems (max: 1, num: 1):
+    [simp] q1_ax ↦ 1
+  [simp] tried theorems (max: 1, num: 1):
+    [simp] q1_ax ↦ 1, succeeded: 1
+  use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 ---
-info: [reduction] unfolded declarations (max: 246, num: 2):
-  [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
+info: [diag] Diagnostics
+  [reduction] unfolded declarations (max: 246, num: 2):
+    [reduction] Nat.rec ↦ 246
+    [reduction] OfNat.ofNat ↦ 24
+  [reduction] unfolded reducible declarations (max: 246, num: 2):
+    [reduction] h ↦ 246
+    [reduction] Nat.casesOn ↦ 246
+  use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 example : q1 x (h 40) := by