Performance

adacovex is a zero-dependency CLI. Its hot path is the assessment pipeline (scan -> patch -> doc metrics -> proof parse -> test parse -> DAL assess -> render, plus the SBOM). This page defines the benchmark categories and the expected numbers on a typical machine.

The benchmark how-to is on Benchmarking, with the pipeline and prove timings, the binary size and the bundled manual, and the server throughput and latency measured beside it. The per-release just prove timings, grouped into phases, are on Prove timing and the optimisation review; the reverse-chronological record of the work behind the numbers is on Performance optimisation history.

Benchmark category reference

adacovex has two caches and one build step; every benchmark category is defined by which of them are populated:

  • the result cache (<cache>/<version>/, or --cache-dir): adacovex’s own content-addressed store of scan, graph, and prove results;

  • the gnatprove session store (<target>/obj/gnatprove/): gnatprove’s internal per-unit session, which re-analyses only changed units;

  • the build (alr build, run by every make recipe that proves): a no-op takes ~0.3 s when built; just clean forces a full recompile.

Category

Command

Result cache

gnatprove session

What it measures

Pipeline cold

adacovex --cache-dir=<fresh>

empty

n/a (not spawned)

Scan, parse, DAL, SBOM, render with no cached results

Pipeline warm

adacovex --cache-dir=<populated>

hit

n/a

Cache-hit path: startup, walks, blob deserialisation

Prove cold

adacovex prove --no-cache --cache-dir=<fresh>

empty

wiped

Truly cold proving: full solver run + everything in pipeline cold (a first CI invocation on a bare runner)

Prove cold clone

adacovex prove --cache-dir=<fresh> --target=<fresh copy>

empty

absent (fresh tree)

A first run on a freshly cloned checkout: no cache, no session, and no gnatprove.out yet – the proof, the summary parse, and the pipeline all from zero

Prove warm

adacovex prove --cache-dir=<populated>

hit

n/a

The short-circuit: one content-hash of the inputs, then serve the stored proof (a developer on an unchanged tree)

Cold build

tools/build.py --release in a copy without obj/, bin/, docs/_build/

n/a

absent

The first build a fresh checkout pays: generators, workspace sync, full compile and link

Docs regen, cold tree

python3 tools/gen-docs.py without docs/_build/

n/a

n/a

The bundled-manual phase on a fresh clone: the committed spec already records the sources, so Sphinx does not run

Docs regen, full Sphinx

python3 tools/gen-docs.py --fresh

n/a

n/a

A clean Sphinx build plus the full re-encode – what a real docs change pays

Two further shapes exist and are worth recognising (one-time-per-session states, not steady states, so they are not benchmarked):

  • adacovex-side cold: prove --no-cache with the result cache wiped but obj/gnatprove/ populated. gnatprove’s session absorbs the solver cost; the run re-does only the adacovex-side work (~1.3 s here) – what a --cache-dir change on a built machine costs.

  • partial session: obj/gnatprove/ holds only some units (after a targeted gnatprove -u run). A prove miss then re-analyses the missing units and lands between the two cold shapes. A full just prove always ends with a complete session, so back-to-back runs sit at prove-warm.

What the numbers mean

Figures are from just bench/perf-bench on the benchmark machine (hyperfine, cold + warm per scenario). They shift with the machine and the codebase; what matters is the shape:

  • Pipeline cold ~77 ms: dominated by source scanning (Ada file enumeration and SHA-256 of every scanned file), the SBOM tree walk and word scan, and the renderers. Nothing here can be skipped: the result cache is empty, so every file must be read and hashed at least once (tool-version probes and ecosystem-metadata lookups live per-machine, outside the result cache, and survive cache wipes).

  • Pipeline warm ~48 ms: the on-disk result cache skips re-parsing unchanged sources; the stamp fast-path skips the per-file SHA-256 entirely (a file unchanged in size is not re-hashed); the tools-set cache skips the SBOM dev-dependency word scan and the tool probes. The remaining time is process startup, directory walks, and blob deserialization. 1.63.0’s directory memo (packed 66-byte entries, a 128-byte key, and a 128-entry cap) cut the warm newfstatat count to 7 924 from 13 428 in a paired run against the v1.62.0 release binary.

  • Cold build ~38.4 s (release profile, fresh checkout, load 0.95): about 0.29 s of generators run as a concurrent bundle (0.46 s when the five steps run in series), the workspace sync inside the 301 ms no-op alr build, and about 38 s of compile and link over 79 units with both mains at -j0. The docs phase used to cost 9-10 s of that; it is now a fingerprint hit of 76 ms (see Pipeline and prove timings).

  • Prove cold ~79 s (load-dependent on this desktop): a from-scratch solver run over 1054 VCs plus the whole pipeline, dominated by gnatprove itself (the CPU time across the proof jobs is the stable part) and paid once per gnatprove session, not per run. The row is solver-bound: a paired run against the v1.62.0 release binary cannot separate the two versions, because the sign of the difference flips between the two trees.

  • Prove warm ~63 ms: the prove result cache serves the stored proof after one content-hash of the input tree, and restores the cached gnatprove.out so the assessment parses it – the number a developer hits on an unchanged tree. Back-to-back just prove runs sit here (the adacovex run is ~0.06 s; the rest of the wall is alr build).

  • Prove cold clone: bounded by the same solver run as prove cold plus one tree copy; the only structural difference is that the clone starts without even a gnatprove.out, so the run cannot short-circuit anything. Read it as the first-invocation cost a new machine or CI runner pays.

  • System time is the tell: ~22 ms on pipeline cold (file I/O), ~14 ms on pipeline warm.

How the timing table is kept

docs/contributing/perf/prove-timing.md keeps one column per phase: a range of versions whose implementation methodology is largely similar. Each phase carries one representative version that supplies the phase’s complete metric set. A new version folds into the open phase while the methodology holds; a methodology shift closes the phase and opens a new one.

The 1.48.0-1.54.0 phase is retired to the notes, and the 1.55.0-1.56.0, 1.57.0-1.60.0, and 1.61.0-1.62.0 phases are closed, represented by 1.55.0, 1.58.0, and 1.62.0. The open phase is 1.63.0-, represented by 1.63.0: that version packed the directory memo again, moved the five pre-build steps into one concurrent bundle, and gave just bench a per-step build-phase breakdown, so the implementation and the measurement methodology both moved. The 1.55.0 detail is on The 1.55.0 timing re-baseline; the whole table is on Prove timing and the optimisation review.

CI

CI runs the self-assessment with result caching disabled where determinism matters (--no-cache-equivalent fresh dirs). The make gates are timed loosely: timings are informational only, because a gate that fails on a slow runner helps nobody. The bench target is not part of just check; it is run by hand before releases.

When the numbers regress

Run just perf-bench first: it reports the CPU break-down and the strace syscall counts. The usual suspects are a new tree walk that re-enumerates a directory a cache already covers, or a new per-file hash that the stamp fast path does not cover. just run-ada-crdt is a handy second datapoint on a smaller tree.