adacovex 1.12.0¶
Date: 2026-08-18 Version bumped 1.11.0 -> 1.12.0.
Changes¶
C1: --theme=NAME flag and a light/dark/system theme dropdown¶
--serve gains a --theme=NAME flag (system | light | dark, default
system) that sets the dashboard’s initial theme. The header control is now
a dropdown with three options – light mode, dark mode, and system theme
– instead of a two-state button. system follows
prefers-color-scheme.
C2: contextual help keyword with flag/subcommand topics¶
help is now a subcommand-like keyword that prints contextual help for a
single flag or subcommand instead of the full usage. The topic is matched
case-insensitively with an optional leading --, and may appear on either
side of the keyword: adacovex help serve, adacovex help --serve, and
adacovex --serve help all print the serve-specific help. adacovex help
(with no topic) and --help print the full usage. Unknown topics print the
full usage with an “Unknown topic” notice.
C4: man page rendering fixed (no more runaway gaps)¶
Two roff bugs made the man page render with broken spacing. The SYNOPSIS used the . RI macro with separate arguments, which groff concatenates without spaces ([--format=FMT][--out=PATH]), and long option lines interleaved with .br caused groff’s terminal output to pad the paragraph with tab stops (adacovex<big gap>sbom). Each SYNOPSIS line is now a single quoted `.
B` argument, and every MODES / EXIT-STATUS description is a single logical line that groff wraps with the proper hanging indent, so the page renders cleanly.
C5: JSON API documented and contextual help extended to all flags¶
The --serve documentation now explains the JSON API end to end: start the
server with adacovex --target=. --serve --port=8080, then
curl http://localhost:8080/api/metrics; the response fields (spark_level,
total_vcs, proved_vcs, tests_passed, tests_failed, doc_coverage,
standard, level, dal_status, and the per-standard standards object)
are documented in the CLI reference and README. Contextual help topics were
added for the remaining flags: --emit-svg / --no-svg,
--emit-markdown, --skip-dir / --relaxed, --verbose, --no-sbom /
--sbom-format, the prove subcommand options (--jobs, --level,
--timeout, --steps, --memlimit, --force, --no-loop-unrolling,
--no-inlining), and the man flags (--check, --dir).
C6: ?theme= query parameter on the dashboard URL¶
The served dashboard accepts a ?theme=light|dark|system query parameter
(for embedding), which takes priority over everything else. Theme
resolution on page load is now: query parameter, then explicit CLI
--theme=light|dark, then the saved localStorage choice, then the system
prefers-color-scheme. Theme persistence remains localStorage-only –
no cookies are used anywhere.
C7: adacovex action builds the target’s native tests before running them¶
The composite action’s run-tests input claims to “build and run the native
test suite”, but in a consumer workspace the build: true step builds
adacovex in a scratch checkout and never touched the target – so
test-command: ./test_crdt failed with ./test_crdt: No such file or directory (exit 127), which broke Ada_CRDT’s release workflow. The action
now runs alr build in the target root before executing test-command
(in the self-assessment case that is an incremental no-op after the adacovex
build). The man-page test suite gained a SYNOPSIS regression check (no
.RI concatenation artifacts).
C8: dashboard HTML is a real file bundled at build time¶
The --serve dashboard’s static shell (doctype, CSS, header with the theme
dropdown + Save settings button, footer with an embed hint, and the theme
script) moved out of the Ada renderer’s line-by-line string literals into a
single HTML file, resources/dashboard.html. tools/gen-dashboard.py
(pure stdlib, typed, --check mode like gen-version.py) bundles it into
src/adacovex-dashboard_template.ads at make build (committed and
byte-identical when unchanged), and Adacovex.Renderers.HTML now only
builds the dynamic card markup, injecting it at the __CARDS__ placeholder
and filling the __THEME__ initial-theme marker. Editing the page chrome
is now a plain HTML edit with no Ada knowledge required.
C9: embed hint on the dashboard¶
The dashboard footer now shows “Embed: append ?theme=light|dark|system to
the URL to pin the theme”, and the theme dropdown carries a matching
title attribute, so embedders discover the query-param pinning from the
page itself.
C10: man page documents theme priority and the JSON API¶
The man page’s --serve entry now documents the full theme resolution
order (?theme= query param, then explicit --theme=light/dark, then the
saved localStorage choice, then the system preference), that persistence
is localStorage-only (no cookies), and the GET /api/metrics JSON endpoint
with a curl example.
C11: action integration test for consumer run-tests¶
A new consumer-run-tests CI job restructures the workspace into a minimal
zero-dependency fixture crate (no adacovex.gpr, so the action’s consumer
branch triggers), copies the action in, and runs it with build: true +
run-tests: true + test-command: ./fixture_main. This pins the fix for
the Ada_CRDT release failure (the action must build the target’s native
tests before running test-command); the target build runs in the target
root so subdirectory target values work too. The action’s internal
Checkout step is now conditional (only re-checks-out when the workspace is
empty) so a consumer fixture already present in the workspace survives, and
the scratch source clone cleans its directory first.
Test Suite¶
647 tests (was 501), across 12 categories (was 10). The CLI-config category (112 checks) covers --version, the man subcommand and its --check / --dir flags, the sbom subcommand’s and --serve dashboard’s standard-awareness defaults (all standards by default, narrowed by --standard / --asil / --class), the --theme flag (default system, light/dark parsing, invalid-value errors), and the contextual help keyword (topic capture in both orders, bare help, and newly documented flags such as --emit-svg and --verbose); the HTML/Markdown renderers category (34 checks) covers the dashboard’s theme dropdown (all three options, the data-initial-theme CLI-theme marker, the Save settings button, saveTheme persistence, the ? theme= query param, the embed hint, the bundled template shell, data-theme override, prefers-color-scheme, and localStorage, plus no leftover __CARDS__/__THEME__ placeholders) on top of the standard-aware dashboard and JSON output; the DAL compliance category (16) gained the cached-HLR parse round-trip; the SBOM generator category (118) gained the dependency-graph cache round-trip; the Man page renderer category (18 checks) covers page structure, the embedded version, an install/read-back round-trip, the Update_Database man-db contract, and a SYNOPSIS regression check (single quoted . B lines, no `.
RI` concatenation); the VCS support category (29 checks) covers marker-file detection for every VCS, display and tool-binary names, and the UX-conversion recommendations.
Proof Results¶
Platinum, 408/408 VCs proved across 45 analysed units (up from 44): the
--theme additions (the Dashboard_Theme type and its To_String /
To_Theme / Is_Valid_Theme conversions in Adacovex.Types) reuse the
already-proved uppercase/parse patterns and add 7 VCs, all proved; the new
bundled dashboard template package (Adacovex.Dashboard_Template, a String
constant generated from resources/dashboard.html) adds one analysed unit
with no proof obligations; the VCS and man-page packages are non-SPARK I/O
code and add no proof obligations. Proven with make prove under gnatprove
16.1.0 (--steps=10000).
Traceability¶
No new HLRs. The dashboard/theme/help work stays covered by the existing
HLR-CLI (src/core/adacovex-config.ads) and HLR-RENDER-HTML
(src/renderers/adacovex-renderers-html.ads/.adb) tags; the bundled
template package is generated data (no subprograms, no HLR), and the action
and CI changes are workflow files that add no traceability.