adacovex 1.3.0¶

Date: 2026-08-01

Version bumped 1.1.0 -> 1.3.0.

Changes¶

C1: Default target changed to the current working directory¶

Running adacovex without --target now audits the current working directory instead of ../Ada_CRDT. The default target is resolved to an absolute path via Ada.Directories.Current_Directory.

Impact: make run-self no longer needs --target=.; any directory can be audited by simply running adacovex from it. --target=PATH still works for any other project.

C2: `--help` now exits cleanly¶

--help prints the usage text and exits with status 0 without scanning or assessment. Previously --help was parsed but adacovex continued running the full pipeline and exited according to the DAL result. A dedicated Help_Requested field was added to CLI_Config and handled in adacovex_main.

C3: Generated binder files removed from the repo¶

The generated b__adacovex_main.* and b__test_runner.* files were removed from version control (build artifacts only).

C4: Differential assessment (`--compare-base=REF`)¶

New --compare-base=REF flag assesses a git base revision in a temporary worktree (/tmp/adacovex-diff-<pid>) and prints a side-by-side table against the current working tree: packages, subprograms, docstring %, HLR traced, orphan tags, SPARK level, VCs proved, tests, DAL status. Exit code is 0 only when there is no regression and the current DAL is Achieved.

Implemented in the new non-SPARK Adacovex.Diff package (it spawns git via GNAT.OS_Lib), wired into adacovex_main as Run_Diff, with Compare_Base/Compare_Base_Len added to CLI_Config. Rows for proof/test artifacts that the base revision does not commit report N/A.

C5: Hardened dev-manifest swap in the Makefile¶

_dev_cmd (used by doc, fmt; prove no longer needs it now that gnatprove is a declared dependency of alire.toml) snapshots alire.toml, alire.lock, alire.lock.prev, and alire/settings.toml into a temp dir, swaps in alire-dev.toml, and restores the snapshots on exit via trap ... EXIT INT TERM. Interrupted or failed dev commands can no longer leave the manifest or lock files polluted with development dependencies (whether or not the lock files are committed). dev-setup and prod-setup were replaced with guidance stubs. alire.toml now declares gnatprove as an explicit dependency (adacovex analyses gnatprove.out and its own self-assessment runs the proof campaign), so alr gnatprove works without a dev-manifest swap; gnatprove is the only declared dependency beyond the GNAT runtime (gnatdoc/gnatformat stay dev-only in alire-dev.toml).

C6: GitHub Actions: composite action, CI, PR gate, and releases¶

New .github/actions/adacovex/action.yml (install Alire + GNAT toolchain, cache, build, run the assessment, publish dal-status/spark-level/ test-count/coverage-pct outputs, a Markdown step summary, and SVG badge artifacts), plus three workflows:

.github/workflows/ci.yml – self-assessment job + build/test job on push to main and pull requests.
.github/workflows/pr-check.yml – runs --coverage-delta against pull_request.base.sha so any PR that drops docstring coverage fails.
.github/workflows/release.yml – on a v* tag, builds the release binary, validates the self-assessment, and creates a GitHub Release with the binary tarball (adacovex + covex alias) and an action tarball. The tag itself publishes the action for uses: <owner>/adacovex/.github/actions/adacovex@vX.Y.Z.

The Alire toolchain is installed from the official alr-*-bin-x86_64-linux.zip release assets, and the GNAT toolchain default is the index-available 15.2.1. Dead, build-generated config/covex_config.* files are no longer tracked (gitignored). The release workflow force-pushes floating vMAJOR / vMAJOR.MINOR tags (e.g. v1 and v1.3 from v1.3.0) plus a latest tag, so the composite action can be consumed as @latest, @v1, or @v1.3 for the latest matching release; the action’s binary-download step resolves @latest (and any floating ref) to the matching release tag, and a coverage-pct output is also emitted from the docstring percentage in normal mode.

C7: Coverage gate (`--coverage-delta=REF`)¶

New --coverage-delta=REF flag for PR-style CI checks: it computes docstring coverage on a git base ref and the current tree (scan + patches + metrics only, no GNATprove/tests/DAL), prints a compact table and a machine-parseable coverage_delta: base=.. current=.. regressed=.. line, and exits 1 when coverage dropped. Works on base refs that do not commit build artifacts and is mutually exclusive with --compare-base. make release now runs this docstring-coverage gate comparing the last release tag against the current tree and aborts if coverage regressed – the same PR compliance gate, applied between releases.

C8: Binary named `adacovex`, clean dev tree¶

The compiled CLI is now named adacovex (via for Executable ("adacovex_main.adb") use "adacovex" in adacovex.gpr), with a covex symlink alias. All scripts, docs, and workflows reference bin/adacovex / covex; adacovex_main remains only as the internal Ada source unit name.

adacovex.gpr now sets for Object_Dir use "obj", so *.o, *.ali, *.cswi, *.bexch no longer accumulate in the repo root. Stray artifacts were removed from the working tree. The composite action gained branding (shield/green) and an author so it can be listed on the GitHub Actions marketplace; each `vX. Y.

Zrelease publishes the matching action version.make badgesinAda_CRDTnow builds adacovex first if the binary is missing and passes an explicit–target=.`.

C9: All workflows use the single composite action¶

ci.yml (self-assessment and build+tests jobs), pr-check.yml (coverage gate), and release.yml now all delegate to .github/actions/adacovex instead of duplicating inline Alire/GNATprove steps. The action gained three inputs to cover every workflow need: run-tests (build + native test suite, assess: false), release-build (pass --release to alr build), and assess (skip the assessment/outputs/badges for build/test-only jobs).

Fixes¶

H1: GNATprove `Initialization` row clobbered Flow Dependencies data¶

Modern gnatprove.out emits separate Flow Dependencies and Initialization summary rows. The parser wrote both into Flow_Checks / Flow_Proved, so a non-empty Initialization row overwrote the real flow-analysis numbers.

Impact: For projects with non-empty init checks, the Bronze level check (Flow_Proved >= Flow_Checks) used init data instead of flow data, and the “Flow Dependencies” rows in the HTML dashboard and Markdown report showed the wrong values.

Fix: Added Init_Checks / Init_Proved to Proof_Summary, parse the Initialization row into them, and surface an Initialization row in the HTML dashboard and Markdown verification report.

H2: `Proved_VCs` computed incorrectly for modern GNATprove layout¶

The modern summary layout is Total | Flow | Provers | Justified | Unproved (no explicit “Proved” column). The old code read column 3 as Proved_VCs, which is the “solved-by-provers” count in the modern layout.

Fix: Proved_VCs is now computed as Total - Justified - Unproved, which is equivalent to flow-solved + provers-solved and correct for both the old and modern layouts.

H3: Empty proof data returned Gold instead of Stone¶

Determine_SPARK_Level fell through to Gold for a summary with no data (0 >= 0). A summary is now detected as empty (all counters zero) and returns Stone, so a project with no GNATprove output cannot pass DAL assessment on a false Gold.

H4: DAL-level minimum SPARK requirements corrected in the docs¶

The DAL-level minimum SPARK requirements documented in AGENTS.md and README.md were corrected to match docs/HLR.md and the implemented Min_SPARK_For table (DAL-A: Gold, DAL-B: Silver, DAL-C: Bronze, DAL-D/E: none).

Test Suite¶

GNATprove parser tests extended to cover the modern layout, empty summaries, and the Flow/Initialization separation (7 new checks; suite now 169 tests).

Proof Results¶

Self-assessment: Platinum (28/28 VCs proved, AoRTE-free). Ada_CRDT (strict): Platinum (273 VCs proved).

Traceability¶

New -- HLR-DIFF tag on Adacovex.Diff is defined in docs/compliance/HLR.md and traced by the differential-assessment feature.