From 65509c561715611ed729a924a7671e40db526d6f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 6 Sep 2021 07:12:36 -0700
Subject: [PATCH] doc: add basic `perf` documentation

---
 doc/perf.md | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 doc/perf.md

diff --git a/doc/perf.md b/doc/perf.md
new file mode 100644
index 0000000000..46d684b357
--- /dev/null
+++ b/doc/perf.md
@@ -0,0 +1,20 @@
+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
+```