Mathlib profiling

Stream: lean4 dev

[Sebastian Ullrich]

I thought it might make sense to start looking into possibly optimizing mathlib4 compile times now that they are non-negligible. My first observation though is an unexpected per-file overhead independent of the file size: image.png
This slice takes about 140ms, though it might take longer for later files. Because what I think is happening in at least the first half is that we have the interpreter run an initialize addLinter ... block (from std4?)... and since a linter is a lambda and a lambda from the interpreter must contain certain metadata, the Lean object mark_mt is spending all that time on presumably is the entire Environment.

[Sebastian Ullrich]

It's harder to tell what's happening in the second part, but it certainly looks very similar. Unfortunate that we would go through the effort of upgrading the Environment to MT and then immediately persistent afterwards

[Sebastian Ullrich]

Precompilation obviously would avoid this, as would storing linters in an (additional) attribute for the first part. I don't see a way to optimize this in the interpreter in general.

[Heather Macbeth]

Thanks for looking into this, indeed it seems like there should now be enough data for some optimization.

[Hanting Zhang]

Pardon the beginner question but how do you read this graph? Is time the y-axis (going down)? What is the x-axis?

[Kyle Miller]

This is a "flame graph." The width of each box is proportional to how long a particular function took, and stacked on top of it are the functions that that function itself called. This way, you can see how much time during a function's execution is attributed to waiting for other functions to complete.

[Kyle Miller]

I think that this one is showing aggregate data. There are also versions where you see every single function call through time as a history of program execution.

[James Gallicchio]

I think it's not aggregated actually... but Sebastian is the only one who can say there haha

[Sebastian Ullrich]

It might be (it does say so at the bottom), but I'm not sure to be honest. This is Hotspot.