5.4. Similar controls, different observations🔗

Both profilers name ranges, aggregate repeated work, schedule short captures inside long loops, and export a timeline. What creates an event is different:

Capability	LeanProfiler	PyTorch profiler
Primary boundary	running Lean application	PyTorch framework and supported device runtime
User-defined range	`span` or `profiled def`	`record_function`
Capture boundary	`profile` or `profileFromEnvironment`	`torch.profiler.profile`
Long-run schedule	skip, warmup, record, record-and-save	`NONE`, `WARMUP`, `RECORD`, `RECORD_AND_SAVE`, advanced by `step()`
Automatic operation events	none	PyTorch operators and selected runtime activity
Accelerator timing	host timing; an adapter may synchronize the device	supported device activities, including CUDA kernels when CUPTI is available
Shapes	application-supplied metadata	optional operator input shapes
Memory	process resources; allocator adapters may supply span counters	optional tensor allocation, release, and memory timeline data
Stacks and FLOPs	not collected automatically	optional source stacks and estimates for selected operators
Aggregation	structured key plus min, mean, median, p95, max, self, and total	`key_averages`, optionally grouped by shape, stack, or overload
Lean-specific signal	heartbeats	none
Trace export	Trace Event JSON for Perfetto	Chrome Trace JSON; TensorBoard trace handler is also available
Built-in regression input	strict versioned summary and built-in comparison	the user or surrounding tooling defines the gate

LeanProfiler is not a smaller reimplementation of PyTorch Profiler. It adds an application-level view for Lean programs, including code that never enters PyTorch. PyTorch Profiler supplies the deeper operator and device view when the work is inside PyTorch.