adacovex CLI Reference

This page is the quick reference: usage, the full flag table, and a short note per flag. Feature-specific detail is in dedicated pages (linked from each section):

Usage

adacovex [options]
adacovex sbom [--format=cyclonedx-json|spdx-json|md] [--out=PATH]
           [--standard=NAME|--dal=LEVEL|--asil=LEVEL|--class=LEVEL]
adacovex prove [-t=PATH] [prove options]
adacovex status [-t=PATH]
adacovex man [--check|--force] [--dir=PATH]
adacovex completion [bash|fish|zsh|pwsh]

Every flag has the explicit long spelling and, where it reads better, a shorthand. The shorthands are -t (--target), -m (--manifest), -s (--serve), -p (--port), -c (--cache), -b (--compare-base), -d (--coverage-delta), -l (--level), -r (--require-proof), and -j (--jobs). The bare words serve, cache, and relaxed also select their flag. Use the long forms in scripts and non-trivial cases; the shorthands are for interactive use.

-l is only the GNATprove proof level. It is never a compliance tier. Compliance selection stays on --standard and its level companions --dal, --asil, and --class.

Flags

Flag

Default

Mode

Description

--target=PATH, -t PATH

. (CWD)

both

Target project root directory

--manifest=PATH, -m PATH

auto-detected

both

Override project manifest path

--dal=LEVEL

C

both

DO-178C DAL level (A-E, also the shared rigour tier)

--asil=LEVEL

-

both

ISO 26262 level: A|B|C|D|QM

--class=LEVEL

-

both

IEC 62304 safety class: A|B|C

--standard=NAME

do178c

both

do178c|iso26262|iec62304|all, or a combined tier token (dal-A..E, asil-A..D, asil-QM, class-A..C)

--serve, -s, serve

off

both

Start HTTP dashboard server (standard-aware, light/dark/system themes)

--serve-workers=N, --workers=N

CPU-scaled (2-8)

serve

HTTP server task-pool worker count

--theme=NAME

system

serve

Dashboard theme: light|dark|system

--port=N, -p N

8080

serve

Dashboard server port

--tz=ZONE / --timezone=ZONE

OS timezone

both

Display timezone (IANA name or UTC/GMT offset)

--excludes=EXT,EXT

empty

complexity

Skip comma-separated file extensions

--skip-path=PATH

empty

complexity

Skip any file whose path contains PATH (repeatable)

--group=KIND

file

spark-coverage

Row grouping: file|folder|package

--metric=METRIC

statements

spark-coverage

Summary metric: statements|subprograms|vcs

--spark-format=FMT

text

spark-coverage

Report shape: text|json

--min-coverage=PCT

0 (all)

spark-coverage

Hide rows whose verified percentage is below PCT

--require-coverage=PCT

off

spark-coverage

CI gate: exit 1 when the gate metric falls below PCT

--gate-metric=METRIC

statements

spark-coverage

Metric the --require-coverage gate applies to

--emit-svg[=PATH], --svg-path=PATH

<target>/docs/badges

both

Output directory for SVG badges

--no-svg

off

both

Suppress SVG badge output (wins over the emit form)

--emit-markdown[=PATH], --emit-md[=PATH], --md-path=PATH

<target>/docs

both

Output directory for Markdown reports

--no-md

off

both

Suppress Markdown report output (wins over the emit form)

--emit-metrics=PATH

off

both

Write a JSON export of metrics + dependency graph to PATH

--completion[=SHELL]

-

-

Print shell completion script (bash/fish/zsh/pwsh, auto-detected) and exit

--skip-dir=NAME

demo,deps,examples

relaxed

Directory name to skip (repeatable)

--relaxed, relaxed / --strict

off

both

Disable / re-enable strict mode (skip dirs, no patches)

--compare-base=REF, --diff=REF, --base=REF, -b REF

off

both

Differential mode vs a base rev (git/hg/svn/fossil/jj)

--coverage-delta=REF, --delta=REF, -d REF

off

both

Docstring-coverage gate vs a base rev (git/hg/svn/fossil/jj)

--cache, -c, cache

on

both

Enable on-disk result caching

--no-cache

off

both

Disable result caching (always re-scan/re-parse/re-prove)

--cache-dir=PATH

the result cache <ver>/<schema>

both

Cache directory for analysis results

--cache-max=N

4096

both

Max cache entries before oldest-first eviction

--no-sbom

off

both

Skip the automatic SBOM written at the end of every assessment

--sbom-format=FMT

cyclonedx-json

both

Format of the automatic SBOM: cyclonedx-json|spdx-json|md

--require-spark=LVL, --spark=LVL

off

both

Fail loudly (exit 1) if SPARK level < LVL (Stone..Platinum)

--require-docstrings=PCT, --docstrs=PCT

off

both

Fail loudly if docstring coverage < PCT% (0-100)

--require-tests=N, --tests=N

off

both

Fail loudly if passing test count < N

--require-proof=PCT, -r PCT

off

both

Fail loudly if proved-VC coverage < PCT% (0-100)

--verbose

off

both

Verbose diagnostics

--version

-

-

Print the bundled version and exit

man

-

-

Install the man page into the local man database

man --check

-

-

Exit 0 if the installed man page matches the binary version, 1 otherwise

man --force

-

-

Reinstall the man page even when it already matches (repair)

man --dir=PATH

platform man root

-

Install the man page under PATH/man1 instead

tldr

-

-

Install the bundled tldr page into the local tldr client (tealdeer or a base client)

tldr --check

-

-

Exit 0 if the installed tldr page matches the bundled page, 1 when it is missing or stale

tldr --force

-

-

Rewrite the installed tldr page even when it already matches

--help

-

both

Print usage and exit

prove-mode flags are accepted by the main command and validated only in prove mode: --jobs/-j, --level/-l, --timeout, --steps, --memlimit, --force, --no-loop-unrolling, --no-inlining, --args, --suppress-warnings, --quiet. See The prove subcommand.

Every flag is detailed with its default, constraints, and examples on two companion pages:

Strict vs relaxed mode

Aspect

Strict (default)

Relaxed (--relaxed)

Directory exclusions

.git, obj, tests, config, .adacovex only

Same + demo,deps,examples + --skip-dir additions

Vendored code

Scanned and counted

Skipped

Patch files

Applied from .adacovex/patches/ (docstrings always, SPARK proof aspects in prove mode)

Not applied

Use case

Full compliance audit

Quick assessment of production code

Patch files can carry SPARK contracts as well as docstrings: a SPARK_Mode / Pre / Post / Global aspect makes the patch a proof patch for vendored code in prove mode – a spec patch (.ads) declares the contracts, and a body patch (.adb) opts the vendored body into the proof. Why they exist, how to write them, and pitfalls are in Proving and writing proofs – proof patches.

Exit codes

Code

Meaning

0

Success (DAL achieved, all checks pass, --version, man or tldr page installed/up-to-date)

1

Compliance failure (DAL unmet, tests failing, a --require-* CI gate unmet, differential regression, man --check finding a newer version available or none installed, tldr --check finding a missing or stale page, and more)

Terminal colour

adacovex colours its terminal output (failures red, passes green, headings bold) so the important lines stand out. Colour is on by default and drops out automatically when the output would not take it:

  • NO_COLOR is set (the cross-tool opt-out convention);

  • a CI variable is set (GitHub Actions, GitLab CI, and more), so CI logs stay plain and machine-readable;

  • TERM is dumb (or empty).

The sbom subcommand

adacovex sbom resolves the target project’s dependency graph from its Alire manifest, alire/alire.lock, and the root .gpr with clauses, then writes a proof-aware software bill of materials in CycloneDX 1.5 JSON or SPDX 2.3 JSON. It is standard-aware (all standards by default), honours SOURCE_DATE_EPOCH for deterministic output, and is mutually exclusive with --compare-base / --coverage-delta. Full detail (usage, properties, determinism, exit codes) is in The sbom subcommand.

Examples

# Self-assessment (strict mode, 100% docs required)
adacovex --target=.

# ISO 26262 assessment at ASIL B (dedicated flag)
adacovex --target=. --asil=B

# IEC 62304 assessment at safety Class A (dedicated flag)
adacovex --target=. --class=A

# ISO 26262 assessment at rigour tier C (ASIL B) via --standard
adacovex --target=. --standard=iso26262 --dal=C

# Emit badges for every standard at the shared tier
adacovex --target=. --standard=all

# Report toolchain + platform status
adacovex status --target=.

# Assess a CRDT library at DAL-C in relaxed mode
adacovex --target=../Ada_CRDT --dal=C --relaxed

# Without SVG output
adacovex --target=../Ada_CRDT --no-svg

# Custom skip dirs
adacovex --target=../Ada_CRDT --relaxed --skip-dir=vendor

# With Markdown reports
adacovex --target=. --emit-markdown=docs/compliance

# Web dashboard on custom port (shorthand: -t, -s, -p)
adacovex -t=. -s -p 9090

# Combined standard + tier token
adacovex --standard=asil-b

# Bare --emit-md writes to the default <target>/docs directory
adacovex --target=. --emit-md

# Differential assessment vs a git base revision
adacovex --target=. --compare-base=HEAD

# Proof-aware SBOM (CycloneDX 1.5 JSON; all standards by default)
adacovex sbom --format=cyclonedx-json --target=. --dal=C
# SBOM for a single standard (ISO 26262 at ASIL B)
adacovex sbom --format=cyclonedx-json --target=. --asil=B
# SPDX 2.3 SBOM at IEC 62304 Class A
adacovex sbom --format=spdx-json --target=. --class=A --out=sbom.spdx.json

# Proof-aware SBOM (SPDX 2.3 JSON) at a custom path
adacovex sbom --format=spdx-json --out=docs/compliance/sbom.spdx.json