When the numbers in traces don't add up

Stream: general

[Kevin Buzzard]

Inspired by #mathlib4 > Benchmark results @ 💬 I was idly profiling declarations in Mathlib/RingTheory/Kaehler to try and understand why they are sometimes so slow. When profiling docs#Derivation.liftKaehlerDifferential I ran into something I've seen before:

          [Meta.synthInstance] [0.142324] ✅️ IsScalarTower S (S ⊗[R] S) ↥(KaehlerDifferential.ideal R S) ▼
            [] [0.016920] ✅️ apply @IsScalarTower.right to IsScalarTower S (S ⊗[R] S) (S ⊗[R] S) ▶
            [] [0.015517] ✅️ apply @IsScalarTower.right to IsScalarTower S (S ⊗[R] S) (S ⊗[R] S) ▶
            [check] [0.040628] ✅️ Submodule.isScalarTower' (KaehlerDifferential.ideal R S) ▶

This is a situation where the numbers plainly don't add up; 50% of the time taken by instance synthesis seems to have vanished into thin air. This is lines 102 to 105 of this gist which is just a cut-and-paste of a partly-unfolded set_option trace.profiler true in output for docs#Derivation.liftKaehlerDifferential . I've asked about this before and have always received either answers I didn't understand or answers of the form "just edit lean and add some more number reporting" which I am manifestly incapable of doing. Is there a way of explaining to a mathematician what's going on?

[Henrik Böving]

In essence one of two things could be happening here. The first is that there are a lot of things that are happening but they take such a short time that they fall below trace.profiler.threshold and thus don't show up in the profile. The other reason could be, that there is some piece of code that is taking time here which isn't wrapped in withTraceNode and thus only appears in the next higher trace node.

[Kevin Buzzard]

Thanks! With set_option trace.profiler.threshold 1 (and set_option trace.profiler.useHeartbeats true) the trace above is a lot more verbose and is here. With some emacs macro trickery I checked that in fact the numbers do add up so it's lots of small things contributing in this case.

34+34+1935+937+197351+2351+24934+2090+2085+2061+2016+2002+2042+2042+2017+2037+2019+2059+2019+1796+2190+1309+517+149+529+152+538+154+546+156+558+472+55005+6104+1079+975+37387+17631+173+873+988+85366+1241+63387+27027+315+26863+205+963+763+2555+25134+2300+2555+77465+18420+172+702+174+710+506+55328+24398+1139+1090+1860+69503+1138+1810+3615+1150+22773+20021+180+933+2137+1368+3866+3953+67216+66956+228880+50624+1848+1074+3480+3651+68144+67864+524475+80571+2095+1337+3765+3929+67194+66905+489552+63402+374+94432+1183120