| name | performance |
| description | How to profile and optimize covalence — flamegraphs, callgrind/cachegrind, and the scaling-first methodology for finding super-linear work |
| disable-model-invocation | true |
Performance work in covalence
The bottleneck is almost never where a flat profile first suggests. Work
scaling-first: confirm the algorithm is the right complexity before
shaving constants.
The golden rule: a log-normal time distribution means hidden super-linearity
If per-item times (e.g. per-theorem import times — see the slowest / p99
fields from profile:import) look log-normal / heavy-tailed, there is still
super-linear-per-item work. A correct, linear(-ithmic) pipeline produces a
tight distribution. Do not declare a heavy tail "fundamental" until you've
checked the scaling.
How to find it:
- Pick a family of items of increasing size (e.g.
yonedalem1 …
yonedainv, or sort theorems by proof length).
- Measure work-per-unit-size —
time / size, and counts like
allocs / size, not just total time. If per-unit cost grows with size →
super-linear. (Plot it; ≈O(size^1.x) shows up immediately.)
- Instrument the suspected driver (a thread-safe
AtomicU64 counter bumped
in the hot function, read via a temp pub fn …_stats() + a temp re-export,
printed from the bench). Compare the count's growth vs. size. The function
whose count-per-size grows is the culprit — not necessarily the one with
the highest flat self-%.
- Rule out red herrings by counting: the highest flat-% function often just
rides along (e.g.
type_of_in rose because something else rebuilt terms it
then had to re-type). Find what drives the count.
- Fix the super-linearity (usually: cache/memoize a result that's rebuilt per
item, or skip unchanged subtrees via a cached summary). Re-measure the
per-unit cost — it should flatten.
- Strip all instrumentation before committing; validate the TCB with
cargo test -p covalence-core and (for the importer) a full set.mm import
with 0 failures.
Each fix tends to unmask the next super-linearity, so re-check the
distribution after every win.
Tools (all auto-download set.mm to a temp cache if missing)
| command | what | when |
|---|
bun run profile:flame [limit] [workers] [freq] | flamegraph of the whole set.mm import (perf record → SVG at /tmp/cov-import-flame.svg) + top-self summary on stderr + JSON | "where does import time go across the corpus?" |
bun run profile:theorem [label] [reps] (CACHE=1) | in-depth single-theorem profile under callgrind; CACHE=1 adds cachegrind D1/LL cache-miss simulation (callgrind = cachegrind + call graph) | drill into one slow proof's hot spots / cache behaviour |
bun run profile:import [limit] | import timing, throughput, per-theorem distribution (median/p99/slowest), perf stat counters (IPC, cache), peak RSS | check the distribution; spot the slowest theorems |
bun run profile:init | the init/ kernel-bootstrap profile | kernel/defs bootstrap perf |
Shared helper scripts/_setmm.mjs resolves set.mm: explicit arg → $COV_SET_MM
→ download to ${TMPDIR}/covalence-set.mm (cached). buildBench() builds the
mm_import_bench example.
The bench binary (crates/kernel/hol/init/examples/mm_import_bench.rs) modes:
<mm> [limit] [workers] (full parallel import) and --only <label> [reps]
(single theorem on one thread, persistent ClauseCache like the real import;
--only-cons routes through a HashCons to test interning).
perf / valgrind notes for this codebase
- Always
--call-graph=dwarf (-g): Rust release lacks frame pointers.
Term::cmp/type_of_in are recursive, so perf's caller attribution
collapses into the recursion — use the count-instrumentation method above
to find callers, not the perf caller graph.- callgrind is ~20–40× slower; a 138 s theorem ≈ 1 h. Run in the background and
use
reps=0 (profiles just the one warmup derive).
- The allocator shows as
_int_malloc / _int_free_chunk / malloc_consolidate
/ cfree / drop_in_place / Arc::drop_slow — sum these for "allocation %".
Settled findings (don't re-litigate)
- A faster allocator (mimalloc/jemalloc) does NOT help the import — tested on
the full corpus incl. the heavy tail (~349 s vs ~350 s). The ~6× single→24-
worker blowup is memory-bandwidth/volume contention, not malloc-lock
contention. The lever is reducing allocation volume, not the allocator.
- Interning during replay (
HashCons) makes single derives ~3× slower — the
Hash/structural cost of hashing huge terms outweighs the sharing. Use a
cheap cached discriminator (the 16-bit term fingerprint) for fast cmp/eq
instead.
See metamath-performance for the import pipeline specifics and the history
of fixes (packrat parser, term fingerprint, $e open-form cache, …).
