Platform support

adacovex is a zero-dependency Ada/SPARK binary. It uses only the GNAT runtime and the standard library. As a result, any platform with a working GNAT/Alire toolchain can build and run it.

adacovex makes no OS-specific assumptions beyond the CPU-core and CI detection described below. These features fall back to single-core operation when the host cannot be probed.

Supported platforms

Platform

Status

Notes

Linux x86-64

Primary

CI, releases, and the proof toolchain bundle all target it.

WSL

Supported

Runs on the Linux/WSL targets below: man installs to the WSL man root and mandb refreshes it; VCS snapshot commands run via sh -c.

Linux aarch64

Supported

Builds from source; the prebuilt toolchain bundle is x86-64 only.

macOS

Supported

Builds from source (Intel and Apple Silicon).

FreeBSD

Supported

Builds from source.

Windows

Supported

Builds from source; core detection uses the Windows env var + PowerShell fallback.

Release binaries

The CI release binary is Linux x86-64 only. The adacovex-vX. Y. Z.tar.gz bundle (adacovex and the covex alias) and the prebuilt GNATprove toolchain asset are built on ubuntu-latest.

Every other platform builds adacovex from source via Alire (alr build). See Installing adacovex.

CPU core-count detection

Adacovex.CPUs.Detect_Core_Count returns the number of logical processors on the host. It falls back to 1 when the host cannot be probed. Detection order (pure GNAT runtime, no external library):

  1. Linux – count processor entries in /proc/cpuinfo.

  2. macOS / FreeBSD – sysctl -n hw.ncpu.

  3. Linux fallback – nproc.

  4. Windows – the NUMBER_OF_PROCESSORS environment variable.

  5. Windows fallback – a PowerShell CIM query (Get-CimInstance Win32_ComputerSystem).

Each stage falls through to the next on failure. If all stages fail, the function returns 1. adacovex still runs when this happens. It runs single-threaded.

CI detection and prove parallelism

Adacovex.CPUs.Is_Running_In_CI detects the CI markers set by GitHub Actions, GitLab CI, Azure Pipelines, Buildkite, CircleCI, Travis CI, AppVeyor, Jenkins, and the generic CI variable.

GNATprove parallelism resolves as:

  • --jobs=N (N > 0) – exactly N jobs.

  • --jobs=0 / -j0 – all cores (gnatprove -j0).

  • default (--jobs omitted) – all cores inside CI. Otherwise it uses max(1, cores - 2). As a result, a developer machine keeps two cores free for the system.

The chosen basis is printed in the verbose log (Jobs_Justification) and in the status report. As a result, a proof run is auditable.

status subcommand

adacovex status reports the toolchain and platform state without running any assessment and without downloading or deploying anything:

adacovex status --target=PATH

It checks and prints:

  • Alire (alr) is installed on $PATH.

  • gnatprove is dependency-managed (target manifest pin) or detectable (global pin, on $PATH, or cached in ~/.adacovex/toolchain). See Architecture – toolchain resolution.

  • The logical CPU count, CI status, and the resulting default -j parallelism are reported.

  • A VCS report lists the VCS command-line tools available on $PATH for the differential modes. The tools are git, mercurial/hg, subversion/svn, fossil, jj, and the man-page tool mandb.

  • The VCS report shows the VCS detected for the target repository.

  • The VCS report notes when the target’s VCS tool is missing.

  • The VCS report notes when man-db (mandb) is absent. You then know that adacovex man can install the page but cannot refresh the man database.

  • The release note states that the CI binary is Linux x86-64 only.

Base adacovex functionality does not require a version control system. The functionality includes scanning, proof analysis, test parsing, compliance assessment, SBOM generation, dashboards, and caching. A VCS is only needed for the differential modes (--compare-base and --coverage-delta).

The status command returns exit code 0 when a usable gnatprove is detectable without a download. alr must be present when the deploy path is the only option. Otherwise, the command returns exit code 1. The VCS report is informational and does not affect the exit code.

Local man page (Linux/WSL)

adacovex man installs the man page into the local man database without root. The default root is $XDG_DATA_HOME/man when set. Otherwise it is ~/.local/share/man. This is the standard Linux/WSL per-user man tree.

The index is refreshed with mandb when mandb is present. Ubuntu and WSL ship mandb.

When man-db is not installed, or when mandb fails, adacovex prints a warning. The warning states that the database was not refreshed. The page is still installed. You can read it with man -l ~/.local/share/man/man1/adacovex.1. adacovex status reports whether mandb is on $PATH up front.

--dir=PATH overrides the root. The page embeds the binary version. adacovex man --check compares it to the installed page and exits 0 or 1. As a result, a prompt hook can auto-install when a newer version is available. See CLI reference.

VCS support (Linux/WSL)

--compare-base and --coverage-delta snapshot a base revision across git, Mercurial, Subversion, Fossil, and jj. See VCS support. The snapshot commands run through sh -c, which WSL provides. All temporary snapshots live under /tmp/adacovex-diff-<pid>.

For VCS with poor snapshot UX (Subversion and Fossil), adacovex prints a note. The note recommends conversion to git.

See the CLI reference for the full flag surface.