Seeing traces in lake exec

Stream: general

[Tomaz Mascarenhas]

Suppose I have the following file:

import Lean
import Foo

open Lean

set_option trace.tt true

def foo : MetaM Unit := do
  trace[tt] "this is a trace"
  return ()

#eval show MetaM Unit from do foo -- [tt] this is a trace

def main : IO Unit := do
  let env ← importModules #[] {} 0 (loadExts := true)
  let coreContext : Core.Context := { fileName := "", fileMap := default }
  let coreState : Core.State := { env }
  let _ ← Meta.MetaM.toIO foo coreContext coreState
  IO.println s!"done"

Where Foo.lean just defines the trace class tt. when I run lake exec I just see the message "done" but not the traces. Is it possible to pass some flag to lake so I can see the traces in the terminal?

[Arthur Paulino]

Try dbg_trace "this is a trace" instead of trace[tt] "this is a trace"

[Tomaz Mascarenhas]

yeah... the thing is I am already working on a project filled with things like trace[tt] that I would like to debug; but I guess I find and replace these traces by dbg_trace. Thanks!

[Kyle Miller]

Trace messages are collected in the state, and once you get to IO it's your responsibility to print them out. They're somewhere in that _ in the let.

I think you could do Meta.MetaM.toIO (foo *> printTraces), which uses IO.println to print them out before leaving the MetaM monad.

[Tomaz Mascarenhas]

I see! foo *> printTraces indeed works, thanks!