output of `dbg_trace` is treated as error in `Delab`

Stream: lean4

[Asei Inoue]

import Lean

open Lean PrettyPrinter Delaborator SubExpr

def foo : Nat → Nat := fun x => x + 1

@[delab app.foo]
def delabFoo : Delab := do
  dbg_trace "dbg trace"

  `($(mkIdent `fooDelab))

#check (foo)

[Asei Inoue]

When the above code is run on VSCode, the output of dbg_trace seems to be treated as an error.
What is the correct way to do print debugging in Delab?

[Kyle Miller]

You can see the output, right? Is there any problem with it being treated as an error?

[Asei Inoue]

I wonder why this is treated as an error.

[Asei Inoue]

Is this intended behavior? Is this a bug?
I think the output of dbg_trace should not be treated as an error…

[Eric Wieser]

In the web editor the output doesn't seem to appear at all

[Asei Inoue]

use VSCode and see output in the terminal window.

[Kyle Miller]

dbg_trace outputs directly to stderr. This is a perfectly fine way to output debug messages.

[Eric Wieser]

Isn't there now a mechanism to capture stderr and pipe it to the infoview? I guess delaborators live outside this if so.

[Kyle Miller]

Maybe there are other mechanisms too, but the one I know about, docs#IO.FS.withIsolatedStreams (used by #eval for example), runs the value and yields the entire output at the end.

I think this sort of defeats the purpose of dbg_trace though, since this means you can't get any debug information until the end of a computation. Plus, there's a larger chance that the logging information will be dropped along the way in case there's an error. You're depending on all the monads in the stack to get the messages to the InfoView, and recall that there have been bugs here before, which makes debugging particularly challenging. (For example, #eval used to drop all log messages for the MetaM monad until recently. I think docs#Lean.liftCommandElabM too was dropping messages.)