adacovex 1.24.0¶

Date: 2026-08-24

Version bumped 1.23.0 -> 1.24.0.

Changes¶

C1: Complexity module docstrings and SPARK mode alignment¶

The Adacovex. Complexity package now carries a package-level docstring and @brief tags on every public subprogram, and all body subprograms have docstrings. The package-level pragma SPARK_Mode (Off) remains necessary because it instantiates the non-formal `Ada. Containers.

Vectors`; the exception is now documented consistently across AGENTS.md, the Makefile, and the proof-status ledger.

C2: Complexity gate CI provisions Alire before build¶

The complexity-gate jobs in ci.yml and pr-check.yml now run alire-project/setup-alire before make complexity-check, so the gate no longer fails with /bin/sh: alr: not found on a fresh runner.

C3: Temp directory and shell abstraction for non-Linux platforms¶

Hardcoded /tmp/ paths in adacovex-cpus, adacovex-vcs, adacovex-prove, adacovex-renderers-man, and adacovex-parsers-manifest are replaced by Adacovex. CPUs. Get_Temp_Directory, which honours TMPDIR / TEMP / TMP environment variables and falls back to /tmp. The shell executable is similarly abstracted through `Adacovex.

CPUs. Get_Shell_Command`.

C4: GNAT v16.1.0 toolchain rollout¶

The composite action default, CI workflow pins, and documentation now all target gnat_native=16.1.0 (previous default was 15.2.1). The action input default, ci.yml, pr-check.yml, release.yml, docs/ci-cd.md, and docs/architecture.md are updated so consumers do not inherit a stale toolchain pin.

C5: Documentation tier separation clarified¶

AGENTS.md now explicitly defines the two documentation tiers: docs/ (user documentation: install, CLI, dashboard, SBOM, VCS, standards, CI/CD, proving, architecture, changelogs, HLR/LLR, performance) for end users and safety engineers; and docs/api-docs/ (generated gnatdoc reference, docstring spec, test format, SPARK/DAL/ASIL/class levels) for contributors and auditors.

C6: HLR index completeness¶

HLR-COMPLEXITY is added to both docs/HLR.md and docs/compliance/HLR.md, closing the gap between the tag used in source docstrings and the published HLR index.

Fixes¶

H1: Complexity-check target no longer drifts from native implementation¶

The Makefile target description and help text now correctly state that make complexity-check invokes the native Ada checker (./bin/adacovex complexity), removing the stale tools/check-complexity.py reference.

H2: Stale Python-checker references purged from docs¶

docs/ci-cd.md, AGENTS.md, .github/workflows/ci.yml, and docs/changelogs/adacovex-1.24.0.md no longer mention the removed tools/check-complexity.py; the complexity gate is now uniformly described as the native Ada implementation.

Test Suite¶

900 tests passing across 14 categories.

Proof Results¶

Platinum, 720/720 VCs proved under gnatprove 16.1.0. 0 unproved, 0 justified.

Traceability¶

No new HLRs. Coverage:

HLR-COMPLEXITY – C1 docstrings and SPARK exception documentation for the complexity checker; C6 added to HLR indexes;
HLR-DOC – C1 package-level and body docstrings for the complexity module; C5 documentation tier separation;
HLR-CI – C2 Alire provisioning in the complexity-gate workflow; C4 GNAT v16.1.0 rollout in CI and action;
HLR-CPU – C3 portable temp-directory and shell abstractions.

See docs/cli-reference.md, docs/ci-cd.md, docs/architecture.md.