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 <data>/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 <data>/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 manifest constraint is a caret range: ^16.1.0 accepts any 16.x at or above 16.1.0, so the pin is a minimum, not an exact match. adacovex strips the operator and deploys the bare version the constraint names, so every run of one release proves with the same prover.

The deployment is keyed by the exact version, so two projects pinning different gnatprove versions keep both toolchains side by side under <data>/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 the global configuration file, deployed through the same alr -n get path), a gnatprove on $PATH, a cached toolchain in <data>/toolchain/, and finally the platform toolchain download. adacovex status reports which tier applies without deploying anything. The global pin, the environment variables, and the state directories are documented in full on Global configuration and state.

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
just build          # version + dashboard/manual generators, then alr build
just test           # the native suite

just is the task runner every recipe in this manual uses (just --list lists them). just build runs the version, dashboard, and offline-manual generators and then alr build; a plain alr build also builds the binary when just is not installed. Either route produces bin/adacovex (with a bin/covex alias). Add --branch vX.Y.Z to the clone for a released tag. A stock Alire toolchain (gnat_native + gprbuild) plus the standard GNAT runtime is all that is needed. No other dependencies. (Contributors use the same just tasks; 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). See Global configuration and state for every environment variable adacovex reads.

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.

adacovex status also reports how the running binary was installed. It prints source-checkout for a binary built inside an adacovex source tree, alire-global for a binary under a global alr install prefix, and on-path for every other binary, with the path beside it. The same three values reach the JSON and the metrics output as install_method.

Keeping the man page in sync

adacovex man installs the man page (which embeds the version) into a man root that the host reader searches. It prefers the first home-owned $MANPATH entry, otherwise the platform data root: ~/.local/share/man on Linux and the BSDs, ~/Library/Application Support/man on macOS, and %APPDATA%\man on Windows. It refreshes the index with mandb (man-db) or makewhatis (mandoc). 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.

When neither indexer is available, the page still installs. Read it with man -l <root>/man1/adacovex.1. The command warns when the root is not on the reader’s man path. See Platforms – local man page for the platform matrix, the root selection, and the reader behaviour.

Keeping the tldr page in sync

adacovex tldr installs the bundled tldr cheat sheet into the local tldr client, so tldr adacovex works offline. The command detects the client and writes to that client’s own page location. tealdeer gets the page in the custom pages directory that tldr --show-paths reports, for example ~/.local/share/tealdeer/pages/adacovex.page.md on Linux. A base client gets the page in its cache pages tree (for example ~/.cache/tldr/pages/common/adacovex.md), plus the host platform directory (linux, osx, windows, android, sunos, or a BSD name). The path follows the platform rules in Platforms – local tldr page.

adacovex tldr --check exits 0 when the installed page matches the bundled one, and 1 when it is missing or stale. A shell prompt hook can auto-update. adacovex tldr --force rewrites an up-to-date page.

The page contains no version, so the check compares content, and an install after an upgrade always refreshes it. With no supported client, the command prints the page to stdout. adacovex tldr --check then exits 1 because there is no installed page.