Can I enable entirety of subclasses of a trace class?

Stream: general

[nrs]

set_option trace.Meta true doesn't do anything, so I have to get more specific and write e.g. set_option trace.Meta.isDefEq true, synthInstance, etc.

Is there a way to enable all of trace.Meta's subclasses?

[nrs]

edit : API available at Lean.Data.Options

[Eric Wieser]

Each trace option is registered as inherited or not inherited, and I don't think that can be adjusted externally.

[nrs]

Hm right, this is either a lakefile thing or has to be implemented by working with initialization, and I have no clue how the latter works. The API for options is not available once the lsp is running

[Eric Wieser]

Using set_option trace.profiler true turns on most trace classes as a special case

[nrs]

had not seen this message! thanks a lot will try it out

[nrs]

came back to report MetaM has a MonadWithOptions instance which can be used to run it with given options