adacovex 1.11.0

Date: 2026-08-17 Version bumped 1.10.0 -> 1.11.0.

Changes

C1: --version flag with the version source tied to the installation method

adacovex --version prints the bundled version (adacovex vX. Y. Z) and exits. The version’s source depends on how the binary was installed: a new tools/gen-version.py (pure stdlib, argparse/pathlib, typed) resolves it from the first available of ADACOVEX_VERSION (release builds – the release workflow and make release VERSION=x.y.z set it from the `vX.

Y. Ztag, and the action's build step regenerates the version file from it, so the shipped binary always reports exactly the tag it was built from),alire/alire-dev.toml(source checkouts), oralire.toml(dependency-managed installs: when covex is built as an Alire crate the binary is compiled from the published crate source, whosealire.toml-- the toml associated with the covex binary for dependency management -- carries the release-manifest version;alire-dev.tomlmay not exist in that tree). The script regeneratessrc/adacovex_version_info.adson everymake build(byte-identical when nothing changed), andAdacovex. Versioninsrc/adacovex.adsre-exports the generated constant, so–version, the man page, the SBOM tool version, and the result-cache namespace can never drift. make bump-versionno longer hand-editssrc/adacovex.ads`.

C2: man subcommand with a versioned man page

adacovex man installs the man page into the local man database (Linux/WSL, no root): the default root is $XDG_DATA_HOME/man or ~/.local/share/man, --dir=PATH overrides it, and the index is refreshed with mandb when present. The page is generated by a new Adacovex. Renderers. Man package and embeds the binary version (in the `.

THheader and aVERSIONsection).adacovex man –checkparses the installed page and exits0when it matches the binary,1when a newer version is available or none is installed, so a shell prompt hook can runadacovex man –checkand auto-install the man page when the machine detects a newer version.make manbuilds and installs. CLI hygiene: a bare–check/–dirwithout theman` subcommand is now a loud error instead of being silently ignored.

C3: Multi-VCS differential modes (Mercurial, Subversion, Fossil, jj)

--compare-base and --coverage-delta no longer require git. A new Adacovex. VCS package detects the target’s VCS by marker file (.git / .jj / .hg / .svn / .fslckout / _FOSSIL_, with a command-tool probe fallback) and snapshots a base revision without touching the working tree: git worktree add --detach, hg archive -r, svn info --show-item url + export -r, fossil open on a copied repo DB, and jj via jj git export into its internal git store followed by a git worktree against .jj/repo/store/git (jj commits are git commits). All snapshot commands run through sh -c, so the feature works on Linux and WSL.

For VCS whose snapshot UX is poor – Subversion (no local history, network-dependent checkouts) and Fossil (niche tooling) – adacovex prints a note recommending the developers convert the repository to git (or a git-compatible VCS); git and jj (colocated jj+git resolves as git) give the best experience.

C4: adacovex status reports VCS availability

adacovex status now has a vcs: section listing which VCS command-line tools are available on PATH for the differential modes – git, mercurial (hg), subversion (svn), fossil, jj, and the man-page tool (mandb) – plus the VCS detected for the target repository. When the target’s VCS tool is missing from PATH, status prints a note that --compare-base / --coverage-delta will need it. The exit code remains prove-toolchain-driven; the VCS report is informational.

C5: Markdown summaries on every CI run, with loud threshold failures

Every CI run now leaves a Markdown summary at the bottom of the job page. The composite action’s assessment step writes an ## adacovex assessment table (target, bundled version, compliance label, SPARK level, tests, coverage) with a PASSED/FAILED verdict, and a new if: always() Write run summary step appends a run-overview table on success and failure. The ci.yml, pr-check.yml, and release.yml workflows each gained a summary job (if: always(), needs: all other jobs) that aggregates every job result into one table. Threshold failures fail loudly at every layer: unmet --require-* gates exit non-zero, are re-surfaced as GitHub ::error:: annotations, are listed in the FAILED summary, and the workflow summary job exits 1 when any of its dependencies failed.

The action’s build step also verifies the downloaded/built binary with --version.

C6: man-db (mandb) detection in man and status

adacovex man now tells the user when man-db is missing instead of silently skipping the database refresh: Update_Database returns whether mandb was found and exited 0, and a missing/failed mandb prints a warning that the page is still installed and readable via man -l. adacovex status gained a note in the vcs: section explaining that adacovex man cannot refresh the man database when mandb is absent from PATH, so users know up front.

C7: make check quality gate + single-source crate description

A new make check target runs the full quality gate in one command – build, native tests, SPARK proof, SVG badges, API docs, SBOM, ASCII, changelog format, and description sync – and the obsolete dev-setup / prod-setup stubs were removed. The crate description now has a single source of truth: alire/description.txt + alire/long-description.txt, propagated to every manifest (alire.toml, release manifests, index entries) by a new tools/update-description.py (make description, CHECK=1 to verify), wired into make bump-version / make release so a new release always ships the current description. The release output (and the GitHub release body) now links every changelog from the last release tag up to the released version. Build/dev prerequisites now list Python 3 for the pure-stdlib tools/*.py scripts.

C8: Result caching extended to HLR/LLR parses, the SBOM graph, and diffs

The on-disk result cache now also covers the DO-178C HLR.md/LLR.md parses (hlr:/llr: keys, served into the DAL assessment), the resolved SBOM dependency graph (graph: key over the manifests, lockfile, every .gpr file, and the .adacovex/patches/ dir), and the --compare-base / --coverage-delta source scans (via Scan_Project_Cached), so unchanged inputs are not re-parsed across runs.

C9: sbom subcommand is standard-aware and defaults to all standards

The sbom subcommand accepts the standard flags (--standard, --dal, --asil, --class) and defaults to all standards: without an explicit standard flag the SBOM carries the joined DO-178C / ISO 26262 / IEC 62304 properties at the shared DAL tier; --standard=iso26262 / --asil=B narrows it to ISO 26262 at ASIL B, --class=A to IEC 62304 at Class A. The usage, man page, README, and CLI reference document the new form.

C10: --serve dashboard is standard-aware with light/dark themes

The served dashboard (--serve) is standard-aware like the sbom subcommand: without an explicit --standard / --asil / --class it renders every standard’s compliance level (DAL-C, ASIL B, Class A) at the shared tier, and an explicit standard flag narrows it to that single standard. The dashboard page also supports light and dark themes: colors are driven by CSS custom properties, the initial theme follows the browser’s prefers-color-scheme, and a header button toggles between light and dark (persisted in localStorage).

Test Suite

616 tests (was 501), across 12 categories (was 10). The CLI-config category covers --version, the man subcommand and its --check / --dir flags, and the standard-awareness defaults for the sbom subcommand and the --serve dashboard (all standards by default, narrowed by --standard / --asil / --class); the HTML/Markdown renderers category covers the standard-aware dashboard with the light/dark theme toggle, prefers-color-scheme, and the 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 covers page structure, the embedded version, an install/read-back round-trip, and the Update_Database man-db contract; the VCS support category (29) covers marker-file detection for every VCS, display and tool-binary names, and the UX-conversion recommendations.

Proof Results

Platinum, 401/401 VCs proved (unchanged from 1.10.0), 0 unproved, 0 justified: the --serve standard-awareness and light/dark theming work touched the config defaults and the HTML renderer only and added no proof obligations. Proven with make prove under gnatprove 16.1.0 (--steps=10000).

Traceability

No new HLRs. The VCS abstraction reuses the existing -- HLR-DIFF tag (src/core/adacovex-vcs.ads, src/core/adacovex-diff.ads); the changed CLI, prove/status, and root packages stay covered by the existing HLR-CLI (src/core/adacovex-config.ads), HLR-PROVE (src/core/adacovex-prove.ads), HLR-CACHE (src/core/adacovex-cache.ads, also tagging the new HLR/LLR parse-cache and SBOM graph-cache paths in src/parsers/adacovex-parsers- do178c.adb / src/parsers/adacovex-parsers-manifest.adb), HLR-SBOM (src/parsers/adacovex-parsers-manifest.ads), and HLR-ARCH (src/adacovex.ads) tags.