# 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.

Z` release publishes the matching action version. `make badges` in `Ada_CRDT` now 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.