adacovex 1.19.0

Date: 2026-08-23 Version bumped 1.18.0 -> 1.19.0.

Changes

C1: dashboard charts powered by Charts.css

The --serve dashboard now renders four live charts (vendored Charts.css v1.2.0, MIT):

  • SPARK proof donut – proved vs unproved VCs;

  • Test results bar chart – per-category pass counts;

  • Proof check-types bar chart – proved checks per check kind;

  • Docstring coverage bar chart – documented vs undocumented subprograms per unit.

Charts.css is vendored as resources/charts.min.css and inlined into the self-contained dashboard template (resources/dashboard.html), so the dashboard keeps its zero-dependency, single-file, offline-serving property – no CDN, no network. The chart cards are generated by the new Renderers. HTML. Render_Charts and injected through the template’s __CHARTS__ placeholder.

Charts update live with the metrics (the JSON API below feeds the same data the dashboard shows). See docs/dashboard.md and docs/THIRD_PARTY_NOTICES.md.

C2: dependency graph – REST API + JSON metrics export

The dependency graph the SBOM builds is no longer locked inside sbom.json:

  • GET /api/deps on the --serve dashboard returns the full dependency graph as JSON (name, version, scope, parent, purl, kind), matching the existing /api/metrics endpoint style. The server state now carries the resolved graph, populated once in serve mode.

  • --emit-metrics=PATH writes a combined machine-readable export after the assessment: {"metrics": {...}, "dependencies": {...}} – the same JSON the dashboard API serves, on disk for scripting, dashboards, or archiving.

Both are wired end to end: emit-metrics action input, docs/ci-cd.md row, and the action-parity gate. --emit-metrics output is uploaded as a CI artifact (see C7). One new server-routing test pins the /api/deps route.

C3: shell auto-completion – adacovex completion

adacovex completion (alias --completion[=SHELL]) prints a static completion script for bash, fish, zsh, or pwsh (SHELL auto-detected from $SHELL; unknown shells fall back to bash). The scripts complete the subcommands and every long flag from the binary’s own Known_Flags table, so the completion set cannot drift from the CLI:

eval "$(adacovex completion)"           # bash (default) / auto-detected
source <(adacovex completion zsh)       # zsh
adacovex completion fish | source       # fish
adacovex completion pwsh | Invoke-Expression   # PowerShell

Zero dependencies: bash uses compgen, zsh _arguments, fish a complete-based function, pwsh Register-ArgumentCompleter. The scripts complete the current word with a prefix filter against the flag list and subcommand names, appending nothing for bare-flag completion. The new Adacovex.Completion package (spec + body, docstring-complete, no SPARK aspects – pure string emission) is covered by 13 new CLI-config tests (script presence per shell, embedded flag-list check, unknown-shell fallback). completion is deliberately a CLI-only early-exit mode in the action-parity allow-list (like status / man / sbom): CI does not need an interactive shell.

C4: system-tool probe cache (SBOM speedup)

The SBOM’s dev-scope dependency scan probes every referenced system tool’s version by spawning <tool> <flag> – tens of milliseconds per tool. The result is now cached on disk under <cache-root>/probes/<tool> with a 7-day TTL, so unchanged toolchains stop paying the spawn cost on every run.

Measured on an 11-tool toolchain (self-assessment, this repo):

before

after

cold full pipeline

~490 ms

~490 ms

warm full pipeline

~430 ms

~310 ms

system time (warm)

~40 ms

~8 ms

--no-cache disables the probe cache too (it lives under the cache root). The TTL means a toolchain upgrade shows up in the SBOM within a week even on machines that never re-probe explicitly. See docs/perf.md.

C5: make bench – hyperfine timings + binary size

A new bench target times the assessment pipeline with hyperfine when installed (bash time fallback: no tooling required), measuring cold (fresh result + probe cache) and warm (populated caches) runs, and reports the binary size – raw and stripped (strip measured on a /tmp copy, so the build output is never modified). Numbers are machine-dependent on purpose: the target is a deterministic recipe, and it is intentionally not part of make check (a slow CI runner must not fail a build). Documented in docs/perf.md. Binary size check on the current build: 7.1 MiB, 3.1 MiB stripped (-57%).

C6: cyclomatic-complexity gate – no god objects

New make complexity-check static gate (native Ada implementation), wired into make check, ci.yml, pr-check.yml, and release.yml:

  • per-file source LOC cap (2000) and a percentage-of-codebase cap (10%) – no file may dominate the tree (god objects);

  • per-subprogram cyclomatic complexity cap (50 decision points) – god functions are flagged as refactor candidates;

  • per-file total decision-point cap (300).

The gate shipped with the refactors it enforces: the DO-178C markdown scanner’s file-reading loop was extracted into a shared generic line-parser (one file-read skeleton, two entry types) and its in-line table parsing into Parse_Table_Row; the test-result parser’s big loop was split into six line-style handlers (Passed/Failed, TAP, Automake, Surefire, Unity) plus the category-helper; and the source scanner’s file-name extraction became a helper. Worst function complexity fell from 57 to 49, and the highest-complexity file dropped under the file cap. All thresholds are configurable flags and are documented in the tool’s module docstring.

C6b: test-summary tables now parse in both layouts (incl. the native one)

The Markdown-table parser only accepted the AUnit-report layout with a leading index cell (| - | Category | N | PASS |); the native test_runner layout (| Category | N | PASS |, no index cell) and space-padded count cells (| 67 |) were silently skipped, so the new dashboard Tests chart was empty for the project’s own test_result.md. Parse_Table_Row now detects the numeric count cell by its digits in either layout, trims column padding from the count and category cells, and keeps the existing footer-overrides-totals semantics. Seven new Test-result-parser tests pin the plain layout (with header and separator rows). This makes the test format spec the single source of truth for what every format – Markdown tables (both layouts), TAP, Automake, Maven Surefire, Unity and AUnit reports – looks like and which line wins when formats mix.

C7: CI – less brittle, better debugging output

  • the composite action folds the assessment output into a log group (::group::) so the step result never hides the debug detail;

  • WARNING lines are re-surfaced as ::notice:: annotations;

  • a new adacovex-assessment artifact (uploaded if: always(), success or failure) carries the full untruncated assessment log – and the --emit-metrics JSON export when requested – so a flaky or unmet gate never requires re-running locally to reproduce;

  • a standalone complexity-gate job runs in ci.yml and pr-check.yml (visible in each workflow’s summary table).

Test Suite

886 tests passing (was 865) across 14 categories: the CLI config category grows from 139 to 152 with the completion-script tests (bash/zsh/fish/pwsh script shape, embedded flag list, unknown-shell fallback), the server routing category grows from 24 to 25 with the /api/deps route test, and the test-result parser category grows from 43 to 50 with the plain-layout/space-padded table tests. Counts synced with make test-count.

Proof Results

Platinum, 720/720 VCs proved across 48 analysed units (unchanged from 1.18.0): all new code (chart rendering, deps serialization, completion scripts, probe cache, complexity tooling, CI wiring) lives in default-off or I/O-bound bodies or is Python/bash tooling – no new proof obligations. 0 unproved, 0 justified. The probe cache and completion packages re-verified with adacovex prove --target=. --force under gnatprove 16.1.0 (--steps=10000).

Traceability

No new HLRs. The new surface extends three existing tags with CLI-relevant tests, all wired through the parity gate and native tests:

  • HLR-DASH – chart cards + /api/deps (server tests category, dashboard docs);

  • HLR-CLI – --emit-metrics export, completion subcommand (config tests);

  • HLR-SBOM / SBOM-dev-deps – probe cache (cache.ads/.adb, perf docs);

  • quality gates – complexity-check feature gate (Makefile, ci.yml, pr-check.yml, release.yml, action-parity allow-list).

See docs/cli-reference.md (flags, completion, --emit-metrics), docs/dashboard.md (charts, REST API), and docs/perf.md (bench, probe cache, binary size).