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

fix: stray dbgTraceVal in trace children elision (#3622)

Browse source
This commit is contained in:
Sebastian Ullrich 2024-03-07 10:44:25 +01:00 • committed by GitHub
parent 611b174689
commit 6af7a01af6
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 6 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Lean/Util/Trace.lean
View file

@ -140,16 +140,13 @@ def addTrace (cls : Name) (msg : MessageData) : m Unit := do
let msg ← mkMsg
addTrace cls msg
private def addTraceNodeCore (oldTraces : PersistentArray TraceElem)
(cls : Name) (ref : Syntax) (msg : MessageData) (collapsed : Bool) : m Unit :=
modifyTraces fun newTraces =>
oldTraces.push { ref, msg := .trace cls msg (newTraces.toArray.map (·.msg)) collapsed }
private def addTraceNode (oldTraces : PersistentArray TraceElem)
(cls : Name) (ref : Syntax) (msg : MessageData) (collapsed : Bool) : m Unit :=
withRef ref do
let msg := .trace cls msg ((← getTraces).toArray.map (·.msg)) collapsed
let msg ← addMessageContext msg
addTraceNodeCore oldTraces cls ref msg collapsed
modifyTraces fun _ =>
oldTraces.push { ref, msg }
def withSeconds [Monad m] [MonadLiftT BaseIO m] (act : m α) : m (α × Float) := do
let start ← IO.monoNanosNow
@ -307,6 +304,7 @@ def withTraceNodeBefore [MonadRef m] [AddMessageContext m] [MonadOptions m]
return (← k)
let oldTraces ← getResetTraces
let ref ← getRef
-- make sure to preserve context *before* running `k`
let msg ← withRef ref do addMessageContext (← msg)
let (res, secs) ← withSeconds <| observing k
let aboveThresh := trace.profiler.get opts && secs > trace.profiler.threshold.getSecs opts
@ -316,7 +314,7 @@ def withTraceNodeBefore [MonadRef m] [AddMessageContext m] [MonadOptions m]
let mut msg := m!"{ExceptToEmoji.toEmoji res} {msg}"
if profiler.get opts || aboveThresh then
msg := m!"[{secs}s] {msg}"
addTraceNodeCore oldTraces cls ref msg collapsed
addTraceNode oldTraces cls ref msg collapsed
MonadExcept.ofExcept res
end Lean

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

@ -164,7 +164,7 @@ where
let more := chopUpChildren cls blockSize children[blockSize:]
children[:blockSize].toArray.push <|
.trace (collapsed := true) cls
f!"{dbgTraceVal <| children.size - blockSize} more entries..." more
f!"{children.size - blockSize} more entries..." more
else children
partial def msgToInteractive (msgData : MessageData) (hasWidgets : Bool) (indent : Nat := 0) : IO (TaggedText MsgEmbed) := do