tracing in one file?

Stream: lean4

[Scott Morrison]

Is it possible to setup tracing in a single file?

import Lean

open Lean Elab Tactic Meta

initialize registerTraceClass `foo

def foo : TacticM Unit := do
  for f in ← getLCtx do
      trace[foo] f.type

elab "foo" : tactic => foo

set_option trace.foo true
example (h : 0 < 1) (g : 37 < 42) : 3 < 7 := by foo

fails with unknown option 'trace.foo', while if I move the last two lines to a separate file it works fine. This is quite inconvenient when trying to make MWEs!

[Scott Morrison]

I know about dbg_trace but can't make it useful here because it won't pretty print Exprs.

[Mario Carneiro]

you can use sudo set_option for this

[Mario Carneiro]

IIUC you can use trace classes that haven't been defined yet, it's only in set_option that the trace class needs to be registered. So sudo set_option just disables the check

[Mario Carneiro]

You can also use Meta.debug if you just want something for test files that happens to already be declared