Platforms and the status subcommand¶
adacovex supports any platform that can run alire: packaging and delivery go through Alire, so adacovex runs wherever Alire itself builds. The tool targets Ada 2012 and later together with SPARK 2014, and uses only the GNAT runtime, so nothing in adacovex itself is platform-specific.
adacovex runs on any host that satisfies these requirements:
the GNAT toolchain to build it (the GNAT runtime is linked into the binary; a prebuilt binary needs only the GNAT runtime), and
GNAT.OS_Libfrom the GNAT runtime - adacovex uses it for path separation, temp files, environment variables, and locating executables onPATH(agprconfigoverride can redirect the runtime path).
No target manifest is required to run an assessment: the pipeline works on any
directory of Ada source. An Alire manifest (alire.toml), an alire.lock or
alire-dev.toml, or a GNAT project file is only needed for SBOM generation and
the dependency graph, which degrade gracefully (a warning, not a failure) when
absent.
Supported platforms¶
Three columns say three different things. Officially supported is the promise: a defect on that platform is a release blocker. Run by the maintainers is the evidence: a maintainer builds and runs the native suite and, where the job exists, the SPARK proof there. Alire index CI is what Alire’s own crate-publishing checks exercise on a pull request against the community index, which is the public proof that the crate installs and builds for that platform.
The platform-build job in .github/workflows/release.yml builds the tree
with a plain alr build and runs the native suite on macOS and Windows,
which is the evidence behind the Run by the maintainers column. It runs
only when a release tag is pushed: the publish job waits for it, so an
ordinary push or pull request never pays for the two extra runners and a
release never ships a binary the other platforms could not build. It uses
the same build path a consumer and Alire’s crate-index CI use, so a green
job means the crate installs and builds on that platform without the local
just tooling.
Platform |
Architecture |
Officially supported |
Run by the maintainers |
Alire index CI |
|---|---|---|---|---|
Linux |
x86_64 |
Yes |
Yes (the release platform; full |
Yes |
Linux |
ARM64 |
Yes |
No (cross-architecture verification on each release) |
Yes |
Linux |
i686, ARM, RISC-V, s390x, ppc64, and other combinations |
Yes (host-word-sized buffers) |
No |
Yes, for the architectures Alire builds |
Windows |
x86_64 |
Yes, built from source (no prebuilt bundle yet) |
Yes (the second development platform; native suite in CI) |
Yes |
Windows |
x86, ARM, ARM64 |
Best effort (the same source, no prebuilt bundle) |
No |
Yes, for the architectures Alire builds |
macOS |
x86_64, ARM64 |
Best effort, no prebuilt bundle |
Yes (native suite in CI) |
Yes |
FreeBSD, OpenBSD, NetBSD |
x86_64, ARM |
Best effort (XDG directories, GNAT runtime only) |
No |
No (Alire does not publish binaries there) |
WSL1, WSL2 |
x86_64 |
Yes (the host appears as Linux) |
Yes |
Covered by the Linux rows |
The prebuilt release bundle is Linux x86-64 only. Every other platform builds
from source with just build (alr build for the plain Alire route).
macOS is not a priority platform, and it is not a large gap: it shares the
POSIX path model with Linux, and Adacovex.Paths already answers its
~/Library directory convention, so the source builds there unchanged.
The differential modes (--compare-base / --coverage-delta) snapshot a
base revision through the VCS command itself. They run through the host shell:
sh -c on Linux, the BSDs, macOS, and WSL, and cmd /c on native Windows.
A Windows host therefore needs no WSL, Cygwin, MSYS2, or Git Bash for them.
The man and tldr subcommands follow the readers and clients that the host
runs; see Local man page and
Local tldr page. Every other feature works on every
platform above.
Platform-agnostic design¶
To keep the tool free of 32/64-bit and endian surprises, adacovex:
derives every fixed-size buffer from
System.Word_Sizeso a 32-bit host keeps proportionally smaller, still-large buffers and a 64-bit host keeps the classic values;stores time stamps and counters as
Long_Long_Integereverywhere, so a value that fits on a 64-bit host cannot be shrank by an implicit 32-bit conversion on Win32 or ARM;delegates host CPU detection, temp directory resolution, and command capture to a single, pure GNAT runtime module (
Adacovex.CPUs) whose platforms are listed in its specification;keeps every platform path decision in one place (
Adacovex.Paths): both/and\separate components, a Windows drive letter (C:\project) and a UNC root count as absolute,~expands fromHOMEthenUSERPROFILE, the host executable suffix (.exeon Windows) is appended once, and a path is normalised to a canonical/form before it becomes a cache key;keeps every platform directory decision in the same place: the configuration, cache, and data directories follow the XDG specification on Linux and the BSDs,
~/Libraryon macOS, and%APPDATA%/%LOCALAPPDATA%on Windows, withADACOVEX_STATE_HOMEas the one override (see Global configuration and state);keeps a cache entry name a legal file name on every platform: a namespaced key (
scan:<sha256>,prove:<sha256>,tools-<sha256>) writes its:as-, because Windows rejects:in a file name;never assumes the host word size when it converts a
File_Time_StamporCurrent_Timevalue: everyGNAT.OS_Lib.To_Cresult is carried as aLong_Long_Integerthrough an explicit conversion, so a 64-bit time stamp is never shrunk by an implicit 32-bit conversion on Win32;rises above Windows’ small default main-thread stack: the build reserves 32 MiB (
-Wl,--stack,33554432) so a function that holds several large fixed-size line buffers in one frame cannot tripSTORAGE_ERROR;resolves the GNATprove job count from the detected core count and honours the
CIenvironment variable so CI uses every core and a developer machine keeps two cores free;keeps every path, line, and description buffer bounded at compile time, with overlong input failing loudly (skipped, count incremented, DAL unmet) instead of silently truncated.
status subcommand¶
adacovex status reports platform and toolchain state without running
an assessment and without downloading anything:
Alire: installed and the version it reports;
adacovex install: how the running binary is installed (
source-checkout,alire-global,on-path) and the path it was invoked from;GNAT compiler: detected version and the target word size;
GNATprove: dependency-managed or
PATH-detected, plus the resolved proof level;CPUs: logical core count and the default
(--jobs)job count (all cores in CI,cores - 2otherwise);CI: whether the
CIvariable or one of the known CI markers is set;VCS: the detected source-control tools for the differential modes (
git,hg,svn,fossil,jj) plus both man indexers (mandb,makewhatis) for the man page installer.
status never changes the working tree and never writes files, so it
is safe to run from a CI job or a packaging script before any
assessment.
Installing on other platforms¶
The published installers cover the platforms above. To install on a
platform that has no installer, install the alire toolchain, then run:
git clone https://github.com/bladeacer/adacovex
cd adacovex
just build # alr build + the version/dashboard generators
just test # the native suite
just check # every gate CI runs before a release
just is the task runner every target in this manual uses (just --list
lists them); the Makefile is a thin shim that delegates to the same tasks,
so an existing make <task> reference still works. A plain alr build also
builds the binary when just is not installed yet.
The shipped binary carries the version of the manifest it was built
from: ADACOVEX_VERSION for release builds, alire-dev.toml for
source checkouts, and the alire.toml associated with the installed
binary for dependency-managed installs. See
Installation for the full method matrix and the
--version output.
A Windows developer runs just check with the fmt gate skipped.
gnatformat has no Windows binary in the Alire community index, so the
formatter gate SKIPs on Windows with the reason “gnatformat is not
available in the dev toolchain”; every other gate runs as usual. The
detail and the reason are on the contributor
guide.
Release binaries¶
The install.sh script and the GitHub Releases bundle ship a prebuilt
adacovex binary. The bundle is Linux x86-64 only, and every other platform
builds from source. Each archive is attested with actions/attest, so the
provenance of a downloaded binary is verifiable.
Local man page¶
adacovex man installs the man page into a man root that the host reader
searches, so man adacovex works without root. It does not depend on a
particular platform. It uses the reader that the host runs:
Host |
Man reader |
Install root |
Database refresh |
|---|---|---|---|
Linux, WSL |
man-db (man-db) |
|
|
macOS |
mandoc (mandoc) |
|
|
FreeBSD, OpenBSD, NetBSD |
mandoc |
|
|
Cygwin, MSYS2, Git Bash |
the reader in that environment |
the same environment’s |
|
Native Windows has no man reader. Use WSL, Cygwin, MSYS2, or Git Bash to read
the installed page. The installer still runs on native Windows and writes the
page under %APPDATA%\man, but nothing reads it there.
The root selection follows the reader, not a fixed path:
The first home-owned entry in
$MANPATH, when the user sets one. This is the best choice because the reader already searches it.Otherwise the platform data home plus
man(the table above).--dir=PATHoverrides both.
After the install, adacovex man checks the root against $MANPATH, or runs
manpath when the variable is unset. When the root is not searched, the
command prints a warning and the exact man -l command to read the page.
It refreshes the index with mandb (man-db), then with makewhatis (mandoc)
when mandb is absent or fails. It prints which tool ran. When neither is
available, the page is still installed, the command prints a warning, and you
read it with man -l. adacovex status reports both indexers up front.
adacovex man # install and refresh
adacovex man --dir="$HOME/.local/share/man" # choose the root
man -l "$HOME/.local/share/man/man1/adacovex.1"
Local tldr page¶
adacovex tldr installs the bundled page into the local tldr client. Both
client families publish their own platform list, and the installer follows the
client it detects:
Client |
Platforms (upstream) |
Page location |
|---|---|---|
tealdeer |
Linux, macOS, Windows, FreeBSD, NetBSD |
the custom pages directory from |
base clients (C, Node, Python, tlrc) |
Linux, macOS, Windows, Android, SunOS, FreeBSD, NetBSD, OpenBSD |
the cache pages tree, under |
Upstream references: tealdeer custom pages and the tldr client specification. The program reads the page directory from the client itself, so a non-standard configured directory works too. Without a client it prints the page, so the command always answers.
Host (from |
Base-client platform directory |
|---|---|
Linux |
|
Android (Termux) |
|
macOS ( |
|
FreeBSD, NetBSD, OpenBSD |
|
Solaris ( |
|
Windows (native, Git Bash, Cygwin, MSYS2) |
|
The installer writes the page to common and to the host platform directory,
so the two copies never disagree. A platform page shadows a stale common page,
and a common page covers an unknown platform. The Android pages are shared with
Linux in the tldr-pages repository, so linux is correct for Termux.