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
+```