Infoview hangs after using `IO.println` in `Delab`

Stream: general

[Alissa Tung]

import Lean

open Lean PrettyPrinter Delaborator SubExpr

@[delab app.Prod.fst, delab app.Prod.snd]
def delabProdProjs : Delab := do
  let xs@#[_, _, _] := (← SubExpr.getExpr).getAppArgs | failure
  IO.println xs
  let stx ← delabProjectionApp
  match stx with
  | `($(x).fst) => `($(x).1)
  | `($(x).snd) => `($(x).2)
  | _ => failure

def xs := (0, 1, 2)

#check xs.fst

consider the above code, the insert of IO.println XS causes info view hangs at #check xs.fst, and keeps not working even after delete the IO.println, but okay after delete then restart server.

Is this a bug of info view? If so, I think I can transfer this thread to GitHub issues.

[Mac Malone]

I suspect this is lean4#738 caused by the delaborator being called directly by the Lean language server in an asynchronous task without redirecting/capturing its output (as it was not expected to print anything).

[Eric Wieser]

Is there a preferred way to print as debugging from within a delaborator?

[Kyle Miller]

You can use dbg_trace. The message seems to appear directly in the Lean server log (so appears in VS Code as an error popup), but at least you can see it.

import Lean

open Lean PrettyPrinter Delaborator SubExpr

@[delab app.Prod.fst, delab app.Prod.snd]
def delabProdProjs : Delab := do
  let xs@#[_, _, _] := (← SubExpr.getExpr).getAppArgs | failure
  dbg_trace "xs = {xs}"
  let stx ← delabProjectionApp
  match stx with
  | `($(x).fst) => `($(x).1)
  | `($(x).snd) => `($(x).2)
  | _ => failure

def xs := (0, 1, 2)

#check xs.fst

[Eric Wieser]

What's the difference between dbg_trace and docs#dbgTrace ?

[Eric Wieser]

And perhaps a related question: where would I have had to look to learn about each of them?

[Jannis Limperg]

Afaik dbg_trace is just a little wrapper around dbgTrace that allows you to use an interpolated string directly, rather than writing dbgTrace s!"...".

[Jannis Limperg]

Stuff like this should really be in the metaprogramming book, probably in the MetaM chapter.

[Eric Wieser]

That should be in the docstring for dbg_trace

[Joachim Breitner]

The current docstring is

dbg_trace e; body evaluates to body and prints e (which can be an interpolated string literal) to stderr. It should only be used for debugging.

What would you like to have added?

Ah, the docstring disappears when dbg_trace is used in a do block. LMFT. PR at <https://github.com/leanprover/lean4/pull/2787>

[Eric Wieser]

I'd also like to see a docstring on dbgTrace that mentions that there is special syntax for it, so I'm not left wondering if the functions are unrelated