From 4935829abe93236b32457ba4904f0ab1317de49a Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 20 Jan 2025 19:06:24 -0700
Subject: [PATCH] feat: generalize `infoview.maxTraceChildren` to the cmdline
 (#6716)

This PR renames the option `infoview.maxTraceChildren` to
`maxTraceChildren` and applies it to the cmdline driver and language
server clients lacking an info view as well. It also implements the
common idiom of the option value `0` meaning "unlimited".
---
 src/Lean/Message.lean                      | 18 ++++++++++++++++--
 src/Lean/Widget/InteractiveDiagnostic.lean | 15 +++------------
 2 files changed, 19 insertions(+), 14 deletions(-)

diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index f9dbd53d6b..ef7014d63f 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -220,6 +220,15 @@ where
   | trace _ msg msgs        => visit mctx? msg || msgs.any (visit mctx?)
   | _                       => false
 
+/--
+Maximum number of trace node children to display by default to prevent slowdowns from rendering. In
+the info view, more children can be expanded interactively.
+-/
+register_option maxTraceChildren : Nat := {
+  defValue := 50
+  descr := "Maximum number of trace node children to display"
+}
+
 partial def formatAux : NamingContext → Option MessageDataContext → MessageData → BaseIO Format
   | _,    _,         ofFormatWithInfos fmt    => return fmt.1
   | _,    none,      ofGoal mvarId            => return formatRawGoal mvarId
@@ -236,8 +245,13 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD
     if data.startTime != 0 then
       msg := f!"{msg} [{data.stopTime - data.startTime}]"
     msg := f!"{msg} {(← formatAux nCtx ctx header).nest 2}"
-    let children ← children.mapM (formatAux nCtx ctx)
-    return .nest 2 (.joinSep (msg::children.toList) "\n")
+    let mut children := children
+    if let some maxNum := ctx.map (maxTraceChildren.get ·.opts) then
+      if maxNum > 0 && children.size > maxNum then
+        children := children.take maxNum |>.push <|
+          ofFormat f!"{children.size - maxNum} more entries... (increase `maxTraceChildren` to see more)"
+    let childFmts ← children.mapM (formatAux nCtx ctx)
+    return .nest 2 (.joinSep (msg::childFmts.toList) "\n")
   | nCtx, ctx?,      ofLazy pp _             => do
     let dyn ← pp (ctx?.map (mkPPContext nCtx))
     let some msg := dyn.get? MessageData
diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean
index 2ad00405d1..b30e64efd7 100644
--- a/src/Lean/Widget/InteractiveDiagnostic.lean
+++ b/src/Lean/Widget/InteractiveDiagnostic.lean
@@ -109,15 +109,6 @@ 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 #[]
@@ -168,8 +159,8 @@ 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 blockSize := ctx.bind (maxTraceChildren.get? ·.opts)
+          |>.getD maxTraceChildren.defValue
         let children := chopUpChildren data.cls blockSize children.toSubarray
         pure (.lazy children)
       else
@@ -185,7 +176,7 @@ where
   /-- 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
+    if blockSize > 0 && children.size > blockSize + 1 then  -- + 1 to make idempotent
       let more := chopUpChildren cls blockSize children[blockSize:]
       children[:blockSize].toArray.push <|
         .trace { collapsed := true, cls }