trace nodes do not nest correctly in the infoview

Stream: lean4

[Eric Wieser]

The following code:

import Lean

open Lean

def foo : MetaM Unit := do
  withTraceNode `trace.Meta.foo (fun e => return m!"{exceptEmoji e} foo") do
    trace[trace.Meta.foo.log] "foo.log"
    -- does it nest if the name is within the current trace node?
    withTraceNode `trace.Meta.foo.bar (fun e => return m!"{exceptEmoji e} foo bar") do
      trace[trace.Meta.foo.bar.log] "foo.bar.log"
    -- does it nest if the name is not within the current trace node?
    withTraceNode `trace.Meta.bar (fun e => return m!"{exceptEmoji e} bar") do
      trace[trace.Meta.foo.bar.log] "bar.log"

set_option trace.profiler true
set_option trace.profiler.threshold 0
-- we can't register a new trace class in this file, so hijack an existing one
set_option trace.Meta true

run_meta foo

gives

image.png

Should the [bar] nodes not be indented?

[Eric Wieser]

I would guess the cause is a missing .group in the formatter code?

[Eric Wieser]

I think this is most noticeable in the formatting of the trace.Meta.synthInstance output, which I was showing to a Rust user at Brown the other day, and he was confused that everything seemed to be flattened

[Eric Wieser]

lean4#6345 attempts a fix

[Junyan Xu]

You apparently didn't read the section because you didn't remove it :upside_down:

[Eric Wieser]

@Junyan Xu, I'm afraid after multiple readings I don't understand your comment

[Christian Merten]

Junyan refers to the very big "Read this section before submitting" in the issue description, which ends with the sentence:

Remove this section, up to and including the --- before submitting.

[Eric Wieser]

Filed as a bug instead at lean4#6389, since my patch didn't work.