LeanProfiler

LeanProfiler records named IO regions in a running Lean program. Each capture produces:

• a Trace Event file that opens in Perfetto;
• a strict JSON summary with integer-nanosecond timings, grouped rows, heartbeats, and process counters.

The trace shows order and nesting. The summary supports scripts and baseline comparisons.

Add it to a project

[[require]]
name = "LeanProfiler"
git = "https://github.com/lean-dojo/LeanProfiler"
rev = "main"

Wrap the work you want to measure:

import LeanProfiler

open LeanProfiler

def main : IO Unit :=
  profileFromEnvironment "application" do
    span "batch.load" loadBatch
    span "model.forward" forward (metadata := {
      phase := some "forward"
      backend := some "eager"
      dtype := some "float32"
      device := some "cpu"
    })

Run it with profiling enabled:

LEAN_PROFILE=1 lake exe your_executable

The default files are:

build/leanprofiler-trace.json
build/leanprofiler-summary.json

Use LEAN_PROFILE_OUT and LEAN_PROFILE_SUMMARY_OUT to keep several runs. LEAN_PROFILE_MAX_EVENTS bounds long captures, and LEAN_PROFILE_PROCESS_NAME changes the process label shown in Perfetto.

Without LEAN_PROFILE=1, the same action runs without retaining spans or writing reports.

Try the examples

LEAN_PROFILE=1 lake exe leanprofiler_nested_example
LEAN_PROFILE=1 lake exe leanprofiler_async_example
LEAN_PROFILE=1 lake exe leanprofiler_schedule_example

The examples cover nested metadata, asynchronous completion, and scheduled active steps.

What the output looks like

The timeline shows the order, duration, and nesting of every recorded span.

The comparison plot makes changed p95 timings visible before you inspect the JSON report.

Compare summaries

lake exe leanprofiler compare \
  build/baseline-summary.json \
  build/candidate-summary.json \
  --metric p95_ns \
  --absolute-tolerance 500000 \
  --relative-tolerance-bps 1000 \
  --json build/comparison.json

A candidate increase is a regression only when it exceeds both tolerances. New and missing keys are reported separately. Invalid or incomplete summaries are rejected unless the caller requests a diagnostic comparison.

TorchLean

TorchLean programs can import the core package directly. A separate package contains a command runner and MLP training walkthrough:

cd integrations/TorchLean
lake build
lake test
LEAN_PROFILE=1 lake exe leanprofiler_torchlean_mlp

The runner also has a CUDA adapter. It rejects CPU parity stubs, waits for the selected device before closing the command span, and records TorchLean device-buffer counters:

LEAN_PROFILE=1 \
lake -R -K cuda=true exe leanprofiler_torchlean \
  quickstart_mlp --device cuda --steps 3

See the integration README.

Guide

The Verso guide follows one real capture from instrumentation through its timeline, summary, and regression check. It also covers sessions, hooks, Lean's elaboration profilers, PyTorch profiler differences, and TorchLean.

Build it locally:

cd guide
lake exe leanprofiler-guide-assets
lake exe leanprofiler-guide --output build/guide

The rendered site is under guide/build/guide/html-multi.

The checked-in JSON captures are real observations. The SVG figures are regenerated from those artifacts by Lean code.

Tests

lake test
lake lint

The TorchLean package has its own test driver under integrations/TorchLean.

Team and license

Maintained by the LeanProfiler Team. Released under the MIT license.