lean_profile_proof
Read-onlyIdempotent
Analyze performance of Lean theorem proofs by profiling execution time per line to identify optimization opportunities.
Instructions
Run lean --profile on a theorem. Returns per-line timing and categories.
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| file_path | Yes | Absolute path to Lean file | |
| line | Yes | Line where theorem starts (1-indexed) | |
| top_n | No | Number of slowest lines to return | |
| timeout | No | Max seconds to wait |
Output Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| ms | Yes | Total elaboration time in ms | |
| lines | No | Time per source line (>1% of total) | |
| categories | No | Cumulative time by category in ms |