2.7. What LeanProfiler does not infer🔗

LeanProfiler does not sample the native call stack, discover every function, intercept allocations, or recognize model operators automatically. Those jobs require compiler instrumentation, operating system sampling, or runtime-specific support. Instead, LeanProfiler records application boundaries chosen by the Lean program and gives adapters a typed place to add measurements they can justify.

This choice is useful when a program crosses several systems. A span can retain the name training.step or solver.expand while a lower-level profiler explains what happened inside one particular call. It also means that span placement is part of the experiment: begin with broad phases, inspect the first trace, and add detail only where the next question requires it.

Enabled profiling has real overhead: mutex access, clock and heartbeat samples, event storage, and eventual analysis. It is designed for selected runtime phases rather than tracing every arithmetic operation. Scheduled captures, stable span names, and a finite event limit keep that cost visible and controlled.