lean-bench

5.3. Workflow 2 perf record and flamegraphs🔗

For "where is the hot code?" use perf record. It writes a perf.data file in the current directory which perf report reads back interactively, or which Brendan Gregg's FlameGraph tools convert to SVG.

$ lake exe bench profile myFib --param 4096 \
    --profiler "perf record -F 999 -g --call-graph dwarf --"

# inspect interactively:
$ perf report

# or render a flamegraph (assumes FlameGraph/ on PATH):
$ perf script | stackcollapse-perf.pl | flamegraph.pl > myFib.svg

Notes:

  • -F 999 samples at 999 Hz, slightly off the kernel's default 1000 Hz so samples don't lock-step with timer interrupts.

  • --call-graph dwarf is more reliable than the default fp for Lean binaries because the Lean compiler doesn't always preserve frame pointers at -O3.

  • cacheMode := .warm (the default) is what you want here: the autotuner runs the function ~thousands of times inside one perf record invocation, so the profile is dense.