feat: infoview.maxTraceChildren (#3370)

Incrementally unveil trace children for excessively large nodes to
improve infoview rendering time, adjust particularly chatty
`simp.ground` trace to make use of it.

src/Lean/Message.lean

@@ -64,8 +64,7 @@ inductive MessageData where
   /-- Tagged sections. `Name` should be viewed as a "kind", and is used by `MessageData` inspector functions.
     Example: an inspector that tries to find "definitional equality failures" may look for the tag "DefEqFailure". -/
   | tagged            : Name → MessageData → MessageData
-  | trace (cls : Name) (msg : MessageData) (children : Array MessageData)
-    (collapsed : Bool := false)
+  | trace (cls : Name) (msg : MessageData) (children : Array MessageData) (collapsed : Bool)
   deriving Inhabited
 
 namespace MessageData

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

@@ -387,9 +387,10 @@ def simpGround : Simproc := fun e => do
   if ctx.simpTheorems.isErased (.decl declName) then return .continue
   -- Matcher applications should have been reduced before we get here.
   if (← isMatcher declName) then return .continue
-  trace[Meta.Tactic.Simp.ground] "seval: {e}"
-  let r ← seval e
-  trace[Meta.Tactic.Simp.ground] "seval result: {e} => {r.expr}"
+  let r ← withTraceNode `Meta.Tactic.simp.ground (fun
+      | .ok r => return m!"seval: {e} => {r.expr}"
+      | .error err => return m!"seval: {e} => {err.toMessageData}") do
+    seval e
   return .done r
 
 def preDefault (s : SimprocsArray) : Simproc :=

src/Lean/Util/Trace.lean

@@ -128,7 +128,7 @@ def addRawTrace (msg : MessageData) : m Unit := do
 def addTrace (cls : Name) (msg : MessageData) : m Unit := do
   let ref ← getRef
   let msg ← addMessageContext msg
-  modifyTraces (·.push { ref, msg := .trace cls msg #[] })
+  modifyTraces (·.push { ref, msg := .trace (collapsed := false) cls msg #[] })
 
 @[inline] def trace (cls : Name) (msg : Unit → MessageData) : m Unit := do
   if (← isTracingEnabledFor cls) then

src/Lean/Widget/InteractiveDiagnostic.lean

@@ -91,6 +91,15 @@ private inductive EmbedFmt
 
 private abbrev MsgFmtM := StateT (Array EmbedFmt) IO
 
+/--
+Number of trace node children to display by default in the info view in order to prevent slowdowns
+from rendering.
+-/
+register_option infoview.maxTraceChildren : Nat := {
+  defValue := 50
+  descr := "Number of trace node children to display by default"
+}
+
 open MessageData in
 private partial def msgToInteractiveAux (msgData : MessageData) : IO (Format × Array EmbedFmt) :=
   go { currNamespace := Name.anonymous, openDecls := [] } none msgData #[]
@@ -138,12 +147,25 @@ where
             match ctx with
             | some ctx => MessageData.withContext ctx child
             | none     => child
+        let blockSize := ctx.bind (infoview.maxTraceChildren.get? ·.opts)
+          |>.getD infoview.maxTraceChildren.defValue
+        let children := chopUpChildren cls blockSize children.toSubarray
         pure (.lazy children)
       else
         pure (.strict (← children.mapM (go nCtx ctx)))
     let e := .trace cls header collapsed nodes
     return .tag (← pushEmbed e) ".\n"
 
+  /-- Recursively moves child nodes after the first `blockSize` into a new "more" node. -/
+  chopUpChildren (cls : Name) (blockSize : Nat) (children : Subarray MessageData) :
+      Array MessageData :=
+    if children.size > blockSize + 1 then  -- + 1 to make idempotent
+      let more := chopUpChildren cls blockSize children[blockSize:]
+      children[:blockSize].toArray.push <|
+        .trace (collapsed := true) cls
+          f!"{dbgTraceVal <| children.size - blockSize} more entries..." more
+    else children
+
 partial def msgToInteractive (msgData : MessageData) (hasWidgets : Bool) (indent : Nat := 0) : IO (TaggedText MsgEmbed) := do
   if !hasWidgets then
     return (TaggedText.prettyTagged (← msgData.format)).rewrite fun _ tt => .text tt.stripTags