Speed and heartbeats

Stream: general

[Damiano Testa]

While trying to understand what counts as a "speed improvement", I decided to run a test: seeing whether replacing exact by refine would have an effect on !bench.

I created two branches.

#11935 tests the speed of running exact x vs refine x and report the difference in heartbeats: an overwhelming refine win.

refine is faster than exact 13896 times
exact is faster than refine 445 times
gain using refine: 468050598
gain using  exact: 1320351

#11936 where I simply rename exact to refine: benchmarking says that it is slower!

Why the difference?

[Henrik Böving]

Your initial numbers don't seem correctly measured to me.

here they are basically always the same:
image.png

and then in overhleming refine victories like here:
image.png

the proof doesn't seem to pass at all?

[Damiano Testa]

Ah, you are right: the second one that is run among exact and refine is consistently (a tiny amount) faster than the first one!