Profiling

Stream: lean4

[Calvin Lee]

Any tips on profiling lean4 code? I remember reading some work was being done here to make the compiler faster, and I was hoping some of that might be applicable to what I'm doing.

[Kevin Buzzard]

In lean 3 it was set_option profiler true

[Calvin Lee]

This appears to work for profiling the compilation
but I want to profile the runtime performance of my program. Is there any way to do that?

[Sebastian Ullrich]

It's a regular executable, use your favorite profiling tool. I usually use perf on Linux.

[Scott Kovach]

I did a bit of poking around in a lean program using perf and the flamegraph tool: www.brendangregg.com/FlameGraphs/cpuflamegraphs.html

[Calvin Lee]

Scott Kovach said:

I did a bit of poking around in a lean program using perf and the flamegraph tool: www.brendangregg.com/FlameGraphs/cpuflamegraphs.html

Flamegraphs work well!
However for me a majority of my time is spent in a function called [Unknown]... any ideas?

[Scott Kovach]

I got better stacktraces by passing

cflags=("-I$bindir/../include" "-fno-omit-frame-pointer" "-g")

I did this by modifying leanc (elan which leanc), which is probably not the right way to do it
I still had an [unknown] stack, but it's not much of the total time so I ignored it. it's possible we're missing debug symbols for the lean standard library code (is it possible to regenerate those without going through the entire lean bootstrap process? I haven't tried compiling from source yet)

[Scott Kovach]

talking about .../.elan/toolchains/leanprover-lean4-nightly/bin/../lib/lean there

[Sebastian Ullrich]

You can use leanmake LEANC_OPTS="-fno-omit-frame-pointer -g" or, starting with the next nightly, leanpkg build LEANC_OPTS="-fno-omit-frame-pointer -g" instead

[Calvin Lee]

I also noticed how leanc is always called with -DNDEBUG when running leanmake bin. If NDEBUG is not defined, do lean programs have additional debugging symbols/assertions/etc or does this only affect the runtime?

[Sebastian Ullrich]

NDEBUG could affect the runtime headers, not sure

[Calvin Lee]

I think setting LEANC_OPTS affects this anyway. Thank you!

[Sebastian Ullrich]

Good question about debug symbols for the stdlib. Note though that compiling Lean from source is no harder than for any other cmake project. You don't have to worry about bootstrapping unless you want to extend Lean.

[Miguel Raz Guzmán Macedo]

How do people recommend one benchmark a Lean script?
The following file Foo.lean only prints Hello World! - does this command trigger a recompilation every time or does it run the object file?

time lean --run Foo.lean

[Wojciech Nawrocki]

That (lean --run) will indeed recompile the module and execute it in the interpreter. If you want to run your program as native code, probably the easiest way is to set up a package by running leanpkg init Foo in the directory you want your package to reside in, and then running leanpkg build bin there. This will produce a binary in <packagedir>/build/bin.

[Wojciech Nawrocki]

Note that this requires main to be defined. If you wish to benchmark within an #eval, you can also use timeit (needs import Init.System.IO) but that goes through the interpreter, which is slower.

[Miguel Raz Guzmán Macedo]

Oh wow, thanks a million @Wojciech Nawrocki , that helped a lot!