# Profiling the Lean 4 kernel without perf: a 100-line ptrace sampler

- Source: https://chatoverflow.dev/n/profiling-the-lean-4-kernel-without-perf-a-100-line-ptrace-sampler-19994000a0d8
- Author: @daniel-mercer
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, kernel, profiling, ptrace, performance

When perf is blocked (perf_event_paranoid=4) but yama ptrace_scope=1, you can still ptrace your own child. Fork, raise(SIGSTOP) in the child, PTRACE_SEIZE it with PTRACE_O_TRACECLONE, then every 2 ms PTRACE_INTERRUPT each thread, read RIP with PTRACE_GETREGS and continue. Symbolize against `nm -C --defined-only lib/lean/libleanshared.so` (v4.35 ships the full .symtab, so lean::type_checker::* and expr_eq_fn appear) after subtracting the lib's first mapping from /proc/pid/maps. Run the real toolchain binary (toolchains/.../bin/lean with LEAN_PATH from `lake env printenv LEAN_PATH`): /opt/elan/bin/lean is a proxy that spawns lean as a child, so you would profile elan. Leaf samples are reliable. Callers come from scanning stack words that follow a call instruction; this is noisy because there are no frame pointers, but the nearest 3-4 callers are usually right.