trace.profiler.useHeartbeats RFC

Stream: lean4

[Kevin Buzzard]

I love trace.profiler.useHeartbeats. The heartbeat output is far more stable than the reporting in seconds (which differs between restarts) and this makes diffs far more stable when debugging. But I've noticed two (very minor) things about it: (1) even though the output is an integer, it is consistently reported to 6 decimal places and (2) when I am mathlib typeclass hell and trying to figure out what's going on by "chasing the big number", it can be very difficult to spot the actual problem when useHeartbeats is on because 3395634.000000, 33956345.000000 and 339563452.000000 (a 7-digit, an 8-digit and a 9-digit number) all look quite similar when reported like this (especially when interspersed between many 4- and 5-digit numbers); this is in contrast to looking at the output in seconds, where it's very easy to visually spot the difference between 3.255733, 0.325573 and 0.032557 and ignore the 0.000023 stuff).

My RFC is to have trace.profiler.useHeartbeats on (so very stable numbers) but in a way where it's visually easy to differentiate between numbers at the "problematic scale" (which in my experience is 7-digit, 8-digit and 9-digit numbers). For example, reporting heartbeats but in the "mega" range (i.e. divide by a million and then report to 6 decimal places) would preserve the numerical stability of the output between runs and also make it visually much easier to spot the large figures in trace output.

[Kim Morrison]

How about when useHeartbeats is on, we print these numbers as e.g. 33_956_345 (i.e. Lean's existing mechanism for optional place notation hints when parsing numbers)?

[Sebastian Ullrich]

That sounds good to me. The alternative I could see is to stay with float formatting but use something like megaheartbeats as the unit, similar to Radar.

[Sebastian Ullrich]

By the way, I have an old lean4 PR I wanted to get mergeable at some point that would also allow measuring CPU instructions, just like in Radar, for a similarly deterministic metric that at the same time is closer to wall-clock time. This would be Linux-only however.

[Joachim Breitner]

Kim Morrison schrieb:

How about when useHeartbeats is on, we print these numbers as e.g. 33_956_345 (i.e. Lean's existing mechanism for optional place notation hints when parsing numbers)?

I'd print large numbers with underscores always even.