profiling proofs with simp and grind

Stream: general

[Chris Henson]

When using trace.profiler with proofs using simp and grind I have noticed that after the first trace, further traces can have significantly shorter times reported for elaboration, I assume due to caching. Are there any options to help with this?

[Sebastian Ullrich]

Do you mean after making an edit? I have not seen that before

[Chris Henson]

Yes, after making an edit. It is possible that I am misinterpreting normal variance in the times reported by the profiler, but I was suspicious because it seems to consistently report a faster elaboration time. (I'm not sure how to make an intentionally slow grind proof to turn this into something reproducible.)

[Sebastian Ullrich]

I doesn't have to be an MWE necessarily. We do have some persistent caches, but only for auxiliary declarations that, I would have assumed, do not take up significant time.

[Sebastian Ullrich]

Note that there is also trace.profiler.useHeartbeats that should give a more deterministic answer - which might or might not be helpful depending on which part you want to profile

[Chris Henson]

Do these persistently cached auxiliary declarations include proofs inside a have? If so, I think that explains it.

[Sebastian Ullrich]

No, they are general theorems derived from declarations such a congruence lemmas. Though if your edit is after the have, then of course it will only be elaborated once

[Chris Henson]

Hmm. Not asking you to take a look (you've been more than helpful enough with tips on using the profiler!) but in case anyone is curious, this theorem/commit is what I was looking at.

[Sebastian Ullrich]

If you could open a (draft) PR, I'm happy to take a look :)

[Chris Henson]

Okay thanks! I opened #31282.

[Sebastian Ullrich]

Okay, I added set_option trace.profiler true in in front of iIndepFun.indepFun_finset, refreshed the file just to be sure, and got

[Elab.async] [20.839547] elaborating proof of ProbabilityTheory.Kernel.iIndepFun.indepFun_finset ▶

Then I added an empty line in front and got 17s, which may be explainable from additional parallel load when elaborating the full file the first time around. Does this roughly match what you're seeing?

[Chris Henson]

That is comparable, and I expected some difference for the first elab of the file. Would you expect to still see a difference after that, say if you just add/remove that option and then make a whitespace change?

[Sebastian Ullrich]

Oh, I do get 6.9s when adding another empty line, interesting!

[Chris Henson]

I think that's approximately what I was seeing. I spent a while trying to track down exactly where the change was with your useHeartbeats suggestion but didn't find exactly where the difference was. (The nature of needing to add/remove something after the first elab makes it a little annoying to compare the traces)

[Sebastian Ullrich]

Oh my bad, I think my machine was simply busy in the background compiling other parts of Mathlib... I now consistently get 6-7s on single-character edits as well as on restarting the file. Typing out e.g. trace.profiler does push it up to 13s, suggesting cancellation of previous tasks is not quite effective here yet.

[Chris Henson]

Hmm, maybe just a similar effect on my machine I was misinterpreting. Thanks for talking the time to look!