trace[debug] in linters

Stream: lean4

[Eric Wieser]

I discovered today that trace[debug] doesn't work in linters, because the trace state is discarded here. Is this deliberate? If so, is there an easy way to copy the traceState into the messages into my own code, so that I can see why my linter is failing?

[Jannis Limperg]

You probably already know this, but you can use dbg_trace instead, this goes directly to stdout.

[Eric Wieser]

My actual issue is that the output of trace.Meta.synthInstance is not appearing anywhere

[Sebastian Ullrich]

Not easily I believe as addTraceAsMessages has been made public and generic only recently. However I went ahead and fixed this in lean#4460 as there any non-reporting state is discarded anyway at the end of the thread.

[Eric Wieser]

    let traces := (← getTraceState).traces.toList
    if !traces.isEmpty then
      Lean.logInfo <| m!"Traces from linter:" ++ .joinSep (traces.map (·.msg)) .nil

seemed to work for me to at least see the output