profiling a project

Stream: lean4

[Floris van Doorn]

I want to look for some excessive slow declarations in the Carleson project. What is the best way to find these (without visiting every file manually)? I tried adding the following to my lakefile.toml:

[leanOptions]
profiler = true
profiler.threshold = 1000

But that gives the error error: lakefile.toml:15:0: error: cannot redefine value key 'leanOptions.profiler'

[Floris van Doorn]

Something that prints the per-file compilation time would also be very helpful.

[Floris van Doorn]

Where is the source code that generates https://speed.lean-lang.org/ ?

[Sebastian Ullrich]

That looks like a Lake bug

[Sebastian Ullrich]

Floris van Doorn said:

Where is the source code that generates https://speed.lean-lang.org/ ?

https://github.com/leanprover-community/mathlib4/blob/master/scripts/bench/temci-config.run.yml

[Sebastian Ullrich]

The simplest setup is to loop over all files in the project and run lake env time lean -Dprofiler... separately on them, then you don't have to worry about parallelism overhead either

[Floris van Doorn]

Sebastian Ullrich said:

That looks like a Lake bug

lean4#7147

[Floris van Doorn]

Thanks for the pointers!

[Floris van Doorn]

For future reference, this gives you a per-file compilation time: (run lake build first)

find Carleson -type f -iname "*.lean" -exec printf "\n{}\n" \; -exec lake env time lean {} \; >& timing.out

[Floris van Doorn]

You can add -Dprofiler=true after the lean command to also profile each file.

[Floris van Doorn]

This also shows all info/warning messages, even when I pass the -q option, as follows:

lake env time lean -q MyFile.lean

Is that intended?

[Sebastian Ullrich]

I think that flag hasn't done anything in any Lean 4 version. So I don't even remember anymore what its exact semantics in Lean 3 were.