adacovex 1.18.0¶
Date: 2026-08-23 Version bumped 1.17.0 -> 1.18.0.
Changes¶
C1: quiet-by-default prove output – --quiet and --suppress-warnings=SETS¶
The prove subcommand’s stdout is now quiet by default for local runs:
GNATprove’s benign informational messages (the default suppression set –
the loop-unrolling/inlining notice blocks) are filtered out of the replayed
output, so a local adacovex prove no longer prints the purely-informational
cannot unroll loop (too many loop iterations) [info-unrolling-inlining]
notices. The filter drops whole message blocks (tag line, info:/-->
header, and any + sub-message in the in-instantiation shape) while every
other gnatprove line – checks, warnings, and the summary – passes through
untouched. The proof outcome is never affected: the notices are informational
only.
Three ways to control it:
--quiet– explicit request for the default suppression set (which is already the default, so this is the documented spelling of the default behaviour). Keep it for CI-adjacent scripts that want to say what they mean.--suppress-warnings– alias of--quiet, kept for compatibility with 1.17.0.--suppress-warnings=SETS– suppress a custom comma-separated list of gnatprove info tags: a set nameSsuppresses blocks tagged[info-S](or a bare[S]). Example:--suppress-warnings=unrolling-inlining,xyz.
--verbose always wins: it shows every message and disables suppression
entirely. CI passes --verbose in both this project’s workflows
(ci.yml, release.yml) and the Ada_CRDT dogfood workflows, so CI output
stays authoritative – the composite action forwards the verbose input to
both the assessment step and the Run GNATprove step. Local runs are quiet
without any flag; nothing is hidden in CI.
The filtering lives in Adacovex.Prove.Replay_Suppressed, which now takes
the comma-separated set list (empty = default set) instead of hardcoding the
single unrolling tag. Prove_Options carries the set list, and
CLI_Config tracks the effective quiet state plus an explicit-flag marker so
--quiet/--suppress-warnings still validate as prove-mode flags without a
plain local run tripping the “requires the prove subcommand” check.
C2: loop-unrolling notices eliminated at the source¶
The prove subcommand always passes --no-loop-unrolling to gnatprove (as
of 1.17.0), so gnatprove never emits the “cannot unroll loop” notice in
the first place; the C1 suppression is the safety net for any residual info
messages from other tags or other gnatprove versions. Ada_CRDT’s make prove and its CI workflows also pass --no-loop-unrolling explicitly, so
the notices are gone there too with the current published binary, not just
the next release. Proof-neutral: 720/720 adacovex and 589/589 Ada_CRDT VCs,
0 unproved, with and without the flag.
Test Suite¶
865 tests passing (was 853) across 14 categories: the config category grows
from 124 to 136 with the new --quiet / --suppress-warnings /
--suppress-warnings=SETS parsing checks (including the quiet-by-default
defaults: suppression on, empty set list, explicit flag unset). All other
categories unchanged. Counts synced with make test-count.
Proof Results¶
Platinum, 720/720 VCs proved across 49 analysed units (unchanged from
1.17.0): the C1/C2 changes touch CLI parsing, the prove option record, and
the output-replay filter – all default-off or I/O-bound bodies, so no new
proof obligations. 0 unproved, 0 justified. Re-verified with
adacovex prove --target=. --force under gnatprove 16.1.0 (--steps=10000).
The Ada_CRDT dogfood target re-verified at Platinum, 589/589 VCs, 0
unproved, 0 justified.
Traceability¶
No new HLRs. The quiet/suppression behaviour extends the existing HLR-CLI
tag (--quiet, --suppress-warnings=SETS parsing in adacovex-config) and
HLR-PROVE (Replay_Suppressed set-list filtering in adacovex-prove),
covered by the C1 config tests and the make run-ada-crdt dogfood
regression. The CI --verbose wiring is covered by this project’s and
Ada_CRDT’s workflow files; see docs/cli-reference.md for the full flag
documentation.