profile information

Stream: general

[Yury G. Kudryashov]

Hi, lean --profile reports several "took ..." for each declaration: "type checking", "compilation", "decl post-processing", "elaboration". What does each step mean?

[Simon Hudon]

• Elaboration is the step that runs your tactic but it also "guesses" all the type error that you don't provide. In other functional languages, we could call that type inference.

• Type checking is when all the type information is all provided, how long does it take to check all the types. This includes checking that the proof tree that you provide forms a valid proof. This step can sometimes be slow because of all the (sometimes recursive) definitions that it has to unfold to check definitional equality.

• Compilation is the step takes a Lean definition and translates it into something that can be executed efficiently. It is especially relevant for tactics as they are not executed in the kernel (i.e. unfolded during type checking). Any definition that those use (e.g. list.map) also have to be compiled.

I'm not sure about "decl post-processing". It might have to do with equation compilation

[Kevin Buzzard]

Thanks Simon. I'm using the profiler a lot at the minute because my category theory code is slow

[Bryan Gin-ge Chen]

Note that some of the info may be inaccurate, see this issue by @Wojciech Nawrocki: https://github.com/leanprover-community/lean/issues/58

Somewhat relatedly, it'd be nice if someone with more knowledge of the C++ could help improve the profiler output. @Scott Morrison has a script that's generating a lot of profiler output here. I attempted to make sense of it (with the aim of visualizing the fast / slow parts of mathlib over time) but it's a bit too hard for me to figure out which profiler lines correspond to which statement / file. I don't know how big of a task this would be; it might be more trouble than it's worth.

[Yury G. Kudryashov]

I run lean --profile --json, and it has all the file/line info

[Yury G. Kudryashov]

Cumulative profiling times say elaboration 1.2e+04s, tactic execution 9.86e+03s. I wonder why this is more than the total running time of 1h.

[Simon Hudon]

That's probably because of parallel processing

[Yury G. Kudryashov]

I'll try with -j1