20 lines
534 B
Markdown
20 lines
534 B
Markdown
Using `perf`
|
|
------------
|
|
|
|
On Linux machines, we use `perf` + `hotspot` to profile `lean`.
|
|
|
|
Suppose, we are in the `lean4` root directory, and have a release build at `build/release`.
|
|
Then, we can collect profile data using the following command:
|
|
|
|
```
|
|
perf record --call-graph dwarf build/release/stage1/bin/lean src/Lean/Elab/Term.lean
|
|
```
|
|
|
|
Recall that, if you have `elan` installed in your system, `lean` is
|
|
actually the `elan` binary that selects which `lean` to execute.
|
|
|
|
To visualize the data, we use `hotspot`:
|
|
|
|
```
|
|
hotspot
|
|
```
|