Zulip Chat Archive

Stream: lean4

Topic: Profiling


view this post on Zulip Calvin Lee (Jan 26 2021 at 06:19):

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.

view this post on Zulip Kevin Buzzard (Jan 26 2021 at 07:07):

In lean 3 it was set_option profiler true

view this post on Zulip Calvin Lee (Jan 26 2021 at 17:35):

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?

view this post on Zulip Sebastian Ullrich (Jan 26 2021 at 17:45):

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

view this post on Zulip Scott Kovach (Jan 26 2021 at 17:59):

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

view this post on Zulip Calvin Lee (Jan 26 2021 at 19:08):

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?

view this post on Zulip Scott Kovach (Jan 26 2021 at 19:46):

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)

view this post on Zulip Scott Kovach (Jan 26 2021 at 19:50):

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

view this post on Zulip Sebastian Ullrich (Jan 26 2021 at 21:42):

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

view this post on Zulip Calvin Lee (Jan 26 2021 at 21:42):

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?

view this post on Zulip Sebastian Ullrich (Jan 26 2021 at 21:43):

NDEBUG could affect the runtime headers, not sure

view this post on Zulip Calvin Lee (Jan 26 2021 at 21:44):

I think setting LEANC_OPTS affects this anyway. Thank you!

view this post on Zulip Sebastian Ullrich (Jan 26 2021 at 21:45):

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.

view this post on Zulip Miguel Raz Guzmán Macedo (Feb 01 2021 at 01:09):

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

view this post on Zulip Wojciech Nawrocki (Feb 01 2021 at 01:46):

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.

view this post on Zulip Wojciech Nawrocki (Feb 01 2021 at 01:53):

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.

view this post on Zulip Miguel Raz Guzmán Macedo (Feb 01 2021 at 01:57):

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


Last updated: May 07 2021 at 13:21 UTC