Installing adacovex

Quick start

1. Install via Alire: alr install covex gnatprove && export PATH="$HOME/.local/bin:$PATH"

2. Assess your project: adacovex --target=. --dal=C

3. Serve the dashboard: adacovex --target=. --serve --port=8080

That is all you need for a local compliance assessment. For CI or release workflows, see CI/CD.

adacovex is distributed as the covex Alire crate, a release bundle on GitHub, or a source build. All three routes produce the same binary (adacovex, with a covex alias on Linux).

Option 1: declare it in your project’s Alire manifest (recommended)

Put covex in your project’s alire-dev.toml (never alire.toml, so release builds stay clean), alongside gnatprove:

# <project>/alire-dev.toml
[[depends-on]]
covex = "*"
gnatprove = "^16.1.0"

Then alr build produces bin/adacovex inside the project. covex prove deploys the pinned gnatprove crate standalone via alr -n get and runs it directly. Each project pins its own exact toolchain version. No global install is needed:

alr build
./bin/adacovex --target=. --dal=C
./bin/adacovex prove --target=.   # deploys gnatprove via alr get, then runs it

How prove resolves gnatprove (Option 1)

The manifest pin is authoritative: when alire-dev.toml or alire.toml declares gnatprove, covex prove always runs that version and never falls back to another prover (a prover-version drift can change which VCs are discharged, so results must always come from the pinned toolchain). The resolution works like this:

1. The version constraint is read from the manifest (^16.1.0 -> 16.1.0; the leading operator is stripped because alr -n get accepts a bare version only).

2. adacovex looks for an already-deployed gnatprove_<version>_<hash>/ crate under ~/.adacovex/toolchain/. One found, it is reused directly – no download, no alr exec, and no composition of your project’s whole dependency set (flaky third-party downloads can never fail a proof run).

3. Not deployed yet: adacovex runs alr -n get gnatprove=<version> into ~/.adacovex/toolchain/ (not into your project’s workspace) and prints a progress line – the first deployment downloads a ~130 MB bundle and may take a minute on a slow link. It is one-time per version: every later run (and every other project pinning the same version) reuses the deployed binary. A deployment that fails is a failed run, never a silent fallback.

4. The deployed gnatprove is run with its bin/ prepended to PATH so the solvers it ships (Z3, CVC5, Alt-Ergo) resolve.

The deployment is keyed by the exact version, so two projects pinning different gnatprove versions keep both toolchains side by side under ~/.adacovex/toolchain/ without interfering. A manifest that declares gnatprove with an unparseable version expression fails loudly rather than guessing.

Projects that do not declare gnatprove fall back to (in order): a global pin (ADACOVEX_GNATPROVE_VERSION, or [prove] gnatprove-version in ~/.adacovex/adacovex.toml, deployed through the same alr -n get path), a gnatprove on $PATH, a cached toolchain in ~/.adacovex/toolchain/, and finally the platform toolchain download. adacovex status reports which tier applies without deploying anything.

Option 2: alr install (global, to $PATH)

alr install covex gnatprove
export PATH="$HOME/.local/bin:$PATH"

covex is the Alire crate name for adacovex (crate page). Once on $PATH, it scans the current directory by default. A gnatprove installed this way is picked up from $PATH by covex prove when the target project declares no manifest dependency of its own.

Option 3: download a release bundle from GitHub

Every vX. Y. Z tag publishes `adacovex-vX. Y.

Z.tar.gz` on the GitHub Releases page.

curl -fsSL https://raw.githubusercontent.com/bladeacer/adacovex/main/install.sh | bash

Bundles are attested with actions/attest.

Release binaries are Linux x86-64 only. Other platforms build from source via Alire (see Platforms).

Building from source

git clone --depth 1 https://github.com/bladeacer/adacovex.git
cd adacovex && alr build   # or: --branch vX.Y.Z for a released tag

alr build produces bin/adacovex (with a bin/covex alias). A stock Alire toolchain (gnat_native + gprbuild) plus the standard GNAT runtime is all that is needed. No other dependencies. (Contributors use the richer make build workflow; see the developer guide.)

Version source per installation method

adacovex --version (and the man page, the SBOM tool version, and the result cache namespace) resolve the version from tools/gen-version.py. The version depends on the installation method:

1. ADACOVEX_VERSION – release builds (the shipped binary always reports the tag it was built from).

2. alire/alire-dev.toml – source checkouts (version = "x.y.z").

3. alire.toml – dependency-managed installs: the toml associated with the covex binary for dependency management carries the release version.

Keeping the man page in sync

adacovex man installs the man page (which embeds the version) into ~/.local/share/man. It refreshes mandb when present. adacovex man --check exits 0 when the installed page matches the binary. A shell prompt hook can auto-update. man --force overwrites an up-to-date page (for example to repair a hand-edited one).

When man-db is missing, the page still installs. Read it with man -l ~/.local/share/man/man1/adacovex.1. adacovex status reports mandb availability up front. See Platforms – local man page for the install roots and man-db behaviour.