Profiling without nested traces

Stream: lean4

[Andrew Yang]

Is there a way to get the output of set_option trace.Meta.synthInstance true annotated with time like how set_option trace.profiler true does but without the whole nested trace? Or alternatively can I make the set_option trace.profiler true only output nodes that are tagged [Meta.synthInstance]?

[Sebastian Ullrich]

It's a bit counterintuitive but you can enable specific trace classes as well as profiler for that