From 1e1e17cb35f61880daced15ebbb511ea27bef83b Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 25 Feb 2025 17:16:35 +0100 Subject: [PATCH] fix: be consistent in not reporting newlines between trace nodes to info view (#7143) This PR makes the server consistently not report newlines between trace nodes to the info view, enabling it to render them on dedicates lines without extraneous spacing between them in all circumstances. The info view code will separately need to be adjusted to this new behavior, until then this change will make adjacent trace node leafs consistently be rendered *on the same line* if there is sufficient space. The cmdline should be unaffected in any case. --- src/Lean/Message.lean | 6 ++- src/Lean/Util/Trace.lean | 4 +- src/Lean/Widget/InteractiveDiagnostic.lean | 6 +++ tests/lean/run/traceFormat.lean | 62 ++++++++++++++++++++++ 4 files changed, 76 insertions(+), 2 deletions(-) create mode 100644 tests/lean/run/traceFormat.lean diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 14fb6af7d7..e7e6bf8025 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -241,6 +241,11 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD | nCtx, ctx, compose d₁ d₂ => return (← formatAux nCtx ctx d₁) ++ (← formatAux nCtx ctx d₂) | nCtx, ctx, group d => Format.group <$> formatAux nCtx ctx d | nCtx, ctx, trace data header children => do + let childFmts ← children.mapM (formatAux nCtx ctx) + if data.cls.isAnonymous then + -- Sequence of top-level traces collected by `addTraceAsMessages`, do not indent. + return .joinSep childFmts.toList "\n" + let mut msg := f!"[{data.cls}]" if data.startTime != 0 then msg := f!"{msg} [{data.stopTime - data.startTime}]" @@ -250,7 +255,6 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD 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)) diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean index 22db50dd6a..2f1b287903 100644 --- a/src/Lean/Util/Trace.lean +++ b/src/Lean/Util/Trace.lean @@ -380,7 +380,9 @@ def addTraceAsMessages [Monad m] [MonadRef m] [MonadLog m] [MonadTrace m] : m Un pos2traces := pos2traces.insert (pos, endPos) <| pos2traces.getD (pos, endPos) #[] |>.push traceElem.msg let traces' := pos2traces.toArray.qsort fun ((a, _), _) ((b, _), _) => a < b for ((pos, endPos), traceMsg) in traces' do - let data := .tagged `trace <| .joinSep traceMsg.toList "\n" + -- cmdline and info view differ in how they insert newlines in between trace nodes so we just + -- put them in a synthetic root node for now and let the rendering functions handle this case + let data := .tagged `trace <| .trace { cls := .anonymous } .nil traceMsg logMessage <| Elab.mkMessageCore (← getFileName) (← getFileMap) data .information pos endPos end Lean diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean index b30e64efd7..25d3d02801 100644 --- a/src/Lean/Widget/InteractiveDiagnostic.lean +++ b/src/Lean/Widget/InteractiveDiagnostic.lean @@ -149,6 +149,12 @@ where | ctx, compose d₁ d₂ => do let d₁ ← go nCtx ctx d₁; let d₂ ← go nCtx ctx d₂; pure $ d₁ ++ d₂ | ctx, group d => Format.group <$> go nCtx ctx d | ctx, .trace data header children => do + if data.cls.isAnonymous then + -- Sequence of top-level traces collected by `addTraceAsMessages`, do not indent. + -- As with nested sibling nodes, we do not separate them with newlines but rely on the client + -- to never put trace nodes on the same line. + return .join (← children.mapM (go nCtx ctx)).toList + let mut header := (← go nCtx ctx header).nest 4 if data.startTime != 0 then header := f!"[{data.stopTime - data.startTime}] {header}" diff --git a/tests/lean/run/traceFormat.lean b/tests/lean/run/traceFormat.lean new file mode 100644 index 0000000000..a809bf7662 --- /dev/null +++ b/tests/lean/run/traceFormat.lean @@ -0,0 +1,62 @@ +import Lean.CoreM + +/-! +Tests formatting of traces in various combinations, on the cmdline automatically via `#guard_msgs` +and in the info view via manual testing. +-/ + +open Lean + +def withNode (cls : Name) (msg : MessageData) (k : CoreM Unit) (collapsed := true) (tag := "") : CoreM Unit := do + let oldTraces ← getTraces + modifyTraces fun _ => {} + k + let ref ← getRef + let mut data := { cls, collapsed, tag } + let msg := .trace data msg ((← getTraces).toArray.map (·.msg)) + modifyTraces fun _ => + oldTraces.push { ref, msg } + +/-- +info: [test] top-level leaf +[test] top-level leaf +[test] node with single leaf + [test] leaf +[test] node with adjacent leafs + [test] leaf + [test] leaf +[test] nested nodes + [test] leaf + [test] node + [test] leaf + [test] leaf +[test] uncollapsed node + [test] leaf + [test] node + [test] leaf + [test] leaf +[test] node with nested newline + [test] line1 + line2 +-/ +#guard_msgs in +#eval show CoreM Unit from do + addTrace `test "top-level leaf" + addTrace `test "top-level leaf" + withNode `test "node with single leaf" do + addTrace `test "leaf" + withNode `test "node with adjacent leafs" do + addTrace `test "leaf" + addTrace `test "leaf" + withNode `test "nested nodes" do + addTrace `test "leaf" + withNode `test "node" do + addTrace `test "leaf" + addTrace `test "leaf" + withNode `test "uncollapsed node" (collapsed := false) do + addTrace `test "leaf" + withNode `test "node" do + addTrace `test "leaf" + addTrace `test "leaf" + withNode `test "node with nested newline" do + addTrace `test "line1\nline2"