6. Profile TorchLean🔗

A TorchLean run crosses several boundaries before a single kernel becomes interesting: data enters the program, the model runs, gradients are computed, parameters change, and device work completes. LeanProfiler records those application-level intervals without changing TorchLean's tensor or proof APIs.

A TorchLean application may depend only on the core LeanProfiler package. This repository also contains an optional integration package with a command runner, a real MLP training workload, and CUDA completion hooks:

cd integrations/TorchLean
lake build
lake test
lake lint

The nested package follows TorchLean's main branch in its Lake configuration. Its checked-in manifest pins the resolved revision until lake update TorchLean is run, so a saved profile can name the code it measured.

1. 6.1. Import the core API
2. 6.2. Run a model command
3. 6.3. Train and measure the example MLP
4. 6.4. Instrument a TorchLean trainer
5. 6.5. Interpret CPU spans
6. 6.6. Interpret CUDA spans
7. 6.7. Compare like with like