5.7. Start with the symptom
Symptom | First tool | Why |
|---|---|---|
one Lean declaration is slow to build |
| the cost occurs during elaboration or compilation |
a running Lean command has a slow phase | LeanProfiler | the application owns the meaningful phase names |
a PyTorch operator dominates CPU time | PyTorch Profiler | operators are discovered and grouped automatically |
a CUDA model waits unexpectedly | LeanProfiler boundary plus PyTorch/CUPTI or Nsight detail | one view locates the application call; the other resolves kernels and runtime activity |
a candidate build regressed | LeanProfiler comparison over repeated controlled captures | the summary schema and threshold policy are explicit |