6. Choose the right profiler🔗

A Lean command can be slow in three distinct places. Lean may spend time elaborating and compiling the program. The running application may spend time reading data, searching, serving requests, or waiting at a foreign boundary. A library or device runtime may spend time in native functions, memory copies, and kernels. No single profiler sees all three.

The views can support one investigation, but their events and timing columns answer different questions.

1. 6.1. Before main: Lean's profilers
2. 6.2. After main: LeanProfiler
3. 6.3. Inside PyTorch: PyTorch Profiler
4. 6.4. Similar controls, different observations
5. 6.5. Read the timing columns carefully
6. 6.6. Use both around a foreign boundary
7. 6.7. Start with the symptom
8. 6.8. References