max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: generalize infoview.maxTraceChildren to the cmdline (#6716)

Browse source 
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".
This commit is contained in:
Sebastian Ullrich 2025-01-20 19:06:24 -07:00 • committed by GitHub
parent 778333c667
commit 4935829abe
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 19 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/Lean/Message.lean
View file

@ -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

15
src/Lean/Widget/InteractiveDiagnostic.lean
View file

@ -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 }