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

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.