profiling declarations

Stream: lean4

[Kevin Buzzard]

Twice today I've wanted to see how long Lean is taking to compile (or whatever it does) a declaration. In Lean 3 set_option profiler true would do this, and this still works in Lean 4 but it doesn't seem to tell me e.g. how long it just took to run instance foo : ..., and hover seems to indicate that it profiles tactics and #eval in Lean 4. How do I recover what we had in Lean 3?