Getting timestamps alongside trace information

Stream: lean4

[Eric Wieser]

I'm looking at a simp call that is unusually slow, and I using set_option trace.<...> to see exactly what's going on. Is there any way to get the current time displayed with each trace message, without having to modify all the existing trace lines in core?

[Kevin Buzzard]

I'm assuming the answer isn't set_option trace.profiler true?

[Eric Wieser]

Correct, that doesn't help here