adacovex 1.38.0

Date: 2026-08-30

Version bumped 1.37.0 -> 1.38.0.

Changes

C1: Manual is now an mdBook project with a Read the Docs site

The user documentation under docs/ is now a proper mdBook project: docs/book.toml (with src = ".") and a root docs/SUMMARY.md table of contents. Read the Docs builds the public manual from it (.readthedocs.yaml, mdbook build docs), so the deployed site, the repository pages, and the bundled offline manual all share one source of truth. make book builds the book locally into docs/book/ (a gitignored build product – see C13) and bundles it into the binary; make book-serve serves the manual locally at http://localhost:8000; make docs-serve keeps serving the raw Markdown.

C2: Bundled offline manual served at /docs

The --serve server now serves a bundled offline manual at /docs (both spellings, with and without the trailing slash, reach the same page). tools/gen-docs.py runs mdbook build over docs/ at build time and bundles the resulting site into the binary as src/adacovex-docs_template.ads (regenerated by make book, which is also part of make build): every page, stylesheet, script, and badge is a lookup table entry keyed by book-relative path, so the manual is fully self-contained and navigable offline. Each asset is its own small Ada string constant – a single multi-megabyte blob would overflow the gnatprove frontend stack (see H4). External fonts and the PNG screenshots are dropped (the screenshots show as notes), and the bundled HTML stays pure ASCII. The header Documentation (offline manual) link and the API playground’s /docs endpoint both open it, so a user on a machine without a network connection can still consult the manual.

C4: yace token colours follow the pinned theme

The vendored yace highlighter’s token colours are driven by the dashboard’s --tok-* CSS variables. The variables had a light default and a dark @media (prefers-color-scheme: dark) block, but no explicit light override, so a user who pinned the light theme on a dark OS still saw dark token colours. The CSS now defines the token colours explicitly per theme (:root, [data-theme="light"], [data-theme="dark"]), so the highlighted JSON always matches the active dashboard theme, not the OS.

C5: complexity-check skips the mdBook build output

The complexity subcommand’s directory walk now skips book directories, so the mdBook build output (docs/book/) is excluded from the source-quality scan. The build output contains minified single-line JavaScript (the search index alone is a 1.4 MB line, far beyond the Max_Line buffer), which printed a spurious “line exceeds Max_Line buffer” error on every scan and, in constrained environments, could push the scan into heap exhaustion. The gate now scans assessed source only, matching the existing obj / bin / dist / build exclusions.

C6: Dashboard preview screenshots refreshed and API tab added

The Charts tab preview (docs/media/dashboard_preview_charts.png) is regenerated from the live dashboard, and a new API tab preview (docs/media/dashboard_preview_api.png) is captured and added to the dashboard walk-through in docs/dashboard.md. The walk-through now covers all eight tabs in header order, and the Charts tab description is corrected from “six cards” to the real eight (the two shared radars, proof and test donuts, proof and test bars, the docstring radial gauge, and the dependency scope polar ring). The screenshots are captured with a Playwright script (tests/e2e/capture-previews.mjs) against the live --serve dashboard.

C8: mdBook search works in the bundled offline manual

The bundled manual served at /docs is searchable offline with mdBook’s own search. In 1.38 the mdBook search machinery was dropped from the bundle (mdbook’s elasticlunr search index is a multi-MB single blob that would overflow the gnatprove frontend as one Ada string constant) and the search box was hidden, so the manual in the binary had no search. tools/gen-docs.py now bundles the whole mdBook search stack – elasticlunr, mark, searcher, and the search index itself – and keeps the search box visible. The index is split into fixed-size chunks, each its own Ada constant (so no single constant exceeds the gnatprove limit), and the server streams the chunks back as one response when the page requests it, so no worker task materialises a multi-megabyte body.

The search index keeps a stable searchindex.js name in the bundle (the content-hashed searchindex-<hash>.js is normalised at build time), so the committed spec never churns its asset name or page references on a docs edit (see C12). No parallel search index or widget: the search button runs mdbook’s own code against mdbook’s own index, exactly like the online site.

C10: Docs reorganised into audience folders

The manual pages now live in folders that mirror their audience, so the navigation shows the structure at a glance: docs/usage/ holds the end-user guides (installation, CLI reference, dashboard, SBOM, standards, platforms, VCS, CI/CD, target projects), docs/contributing/ holds the contributor and maintainer guides (developer guide, proving, architecture, requirements, performance, STE100, LLM usage), and the top level keeps the index plus the maintainer references (HLR/LLR, test report, credits, third-party notices) next to the proof/, compliance/, badges/, api-docs/, and changelogs/ outputs. docs/SUMMARY.md groups the TOC into Getting started / Using adacovex / Contributing / Maintainer references, and every cross-link, README link, AGENTS.md doc-links entry, tools/doc-links.map, tools/rst2md.py guide table, and generated api-docs page was updated in the same change. The manual index no longer carries the maintainer-only build and generated-output instructions; those moved to the developer guide (docs/contributing/developer-guide.md) so end-user pages stay focused on using adacovex.

C11: Maintainer-only make targets scoped out of end-user docs

End-user pages no longer reference make/dev targets: ci-cd.md scopes make action-parity-check, make coverage-gate, make release, and the release workflow to the developer guide and swaps the debugging-guide make prove for the user-facing adacovex prove; installation.md builds from source with alr build (the user-facing route) instead of make build; and cli-reference.md points contributors at the developer guide instead of make complexity-check. The action’s own alr build steps remain, since they describe what the action does for the user.

C13: docs/book no longer committed; the generated spec is the artifact

The mdBook build output (docs/book/) is no longer committed. mdBook content-hashes its assets, so the build churned searchindex-<hash>.js and every page’s reference to it on each docs edit – pure version-control noise. docs/book/ is now gitignored and regenerated locally by make book; the committed artifact is the generated spec src/adacovex-docs_template.ads, which is stable (see C8 and C12) and is gated by python3 tools/gen-docs.py --check inside make check. The manual’s own search and print work identically offline and online, and a fresh clone builds the binary without mdbook (the committed spec is kept until make book regenerates it).

C12: Offline manual print button works and the search index name is stable

The offline manual at /docs now behaves exactly like the online one when printing. mdBook’s print view (print.html – the single-page rendering the print button opens and which triggers the print dialog on load) and its print stylesheet are bundled with the rest of the site, so Print this book works offline instead of returning 404. The SVG favicon is bundled too; only the PNG favicon and the PNG dashboard screenshots are dropped.

The bundled search index no longer churns its name on every docs edit. mdBook content-hashes the index (searchindex-<hash>.js), and the hash changes whenever the manual text changes, so each rebuild renamed the asset and rewrote the reference on every page. tools/gen-docs.py now normalises the index to a stable searchindex.js – the asset and every page’s reference – so a docs edit updates the same entry in place and the generated spec stops diffing on the file name.

Fixes

H1: Vendored yace.js now appears in the SBOM

The vendored JavaScript bundles (graphre.js, nomnoml.js, flexsearch.js, yace.js) sat at the resources/ root, but the vendored yace.js lived under resources/js/ with the authored dashboard modules. The SBOM asset scanner treats resources/js/ as authored dashboard code and skipped it, so yace never became a dependency component. yace.js now sits at the resources/ root with the other vendored libraries, the layout clearly separates dependency JavaScript from dashboard JavaScript, and the SBOM lists yace (MIT, v1.1.0, pkg:generic/yace) alongside the other bundled libraries.

H3: /docs subpages are served again

The Docs_Subpath slicing assumed the request path started at index 1, but Get_Path returns a slice of the request line, so every /docs/<subpath> kept a leading slash and returned 404 – only /docs and /docs/ resolved. The six-character prefix is now stripped from the slice’s actual first index, so every page, stylesheet, and badge of the bundled manual serves (an e2e test pins the exact, nested, and extensionless subpaths plus a missing-page 404).

H5: Idle connections no longer pin the server worker pool

The dashboard server’s fixed-size worker pool (4 workers) blocks each worker on the next request of a keep-alive connection. Browsers hold several idle connections open, so once all four workers were waiting on silent connections, the next request queued forever – the e2e suite started hitting 60-second timeouts on /docs subpages as it grew. Each accepted socket now carries a 5-second receive timeout, and a timed-out (or dropped) connection is closed in the worker’s error path (which previously leaked the socket). A worker frees instead of pinning the pool forever, and the request is served. (The timeout was originally 5s; H10 below shortens it to half a second so a multi-asset docs burst fans out across the pool instead of waiting one timeout per queued connection.) The e2e suite returns to 28 passing in ~14 seconds.

H4: Bundled manual no longer overflows the gnatprove frontend

The complete-book offline manual is a 4 MB asset set, and gen-docs.py emitted it as one giant &-concatenation chain (300k+ string literals). GNAT’s frontend parses that tree fine, but gnatprove’s flow analysis blew its stack (Storage_Error stack overflow at adacovex-docs_template.ads), aborting make prove and therefore make check and every release. Experiments showed the limit is the constant size itself (a single string constant over ~1 MB overflows whatever its structure), so the generated spec now holds one aliased constant String per asset (the multi-MB search index is split into fixed-size chunks, each its own constant – 166 bodies in all), each well under the limit, never concatenated into one value – with an Asset_Bodies access-to-constant table and an Asset_Index subtype so Content (Idx) needs no unchecked bounds reasoning. The served bytes are unchanged (each asset constant carries the identical content), the server routes through the same Find lookup and streams the bodies (see C8), and the bundle-links check still passes.

H6: mdbook detected as a system dev dependency

The SBOM’s system-tool discovery now recognises mdbook: it joined the curated System_Tools table, so a project whose build files reference mdbook (for example a Markdown manual’s mdbook build) gets it registered as a system-scope dev dependency (pkg:generic/mdbook). The detection stays data-driven – adding a tool is one table entry, and the scan remains a generic word-match over build files, not a hardcoded call site.

H7: Read the Docs build deploys again

The .readthedocs.yaml build failed in CI with mdbook: not found even though cargo install mdbook succeeded. Read the Docs runs the install and build jobs in separate shells, and cargo writes the binary into the Rust toolchain’s bin directory, which is not on the build job’s PATH. The build command now resolves the cargo-installed mdbook binary (find under $HOME) and prepends its directory to PATH before building, so the build survives Rust toolchain upgrades without a hardcoded version path.

H10: Docs pages load quickly again

The bundled manual felt slow to open: a ~15-asset page (HTML + several CSS + JS) took roughly six seconds to load. The 4-worker server pool pinned each worker to its keep-alive connection for a 5-second idle receive timeout, so once four sockets were held by the browser’s parallel asset requests, the remaining connections queued in the accept backlog for ~5s until a worker released. The idle timeout is now half a second: a worker that finishes a keep-alive exchange returns to Accept_Socket quickly, the burst fan-outs across the pool, and a docs page loads in well under a second. Workers are released faster on idle connections, which also means a stale or abandoned connection is reaped sooner than before.

H8: HLR tags are no longer read from string literals

The source scanner extracted HLR traceability tags from -- sequences inside string literals, treating them as comment starts. The bundled manual’s generated constants embed examples such as -- HLR-XXXX in HTML and JS string data, so those examples registered as orphan source tags and the self-assessment fell to DAL-C Unmet. The scanner now tracks string literals (including "" escapes) and only starts a comment at a -- outside one; tags inside strings are data, not traces. The self-assessment returns to DAL-C Achieved.

Test Suite

The native suite grows from 1169 to 1173 tests. The server routing category adds four checks for the /docs and /docs/ routes and two near-miss paths (/docs2, /manual) that must stay 404s. The scanner category adds three checks that a -- HLR-* string literal is not a source tag while a real comment tag after a string still is. H9’s query-string handling adds no native assertions (the routing table already pins /docs and the Strip_Query path), and H10’s timeout is timing behaviour the suite cannot assert deterministically – both are covered manually and by the dashboard e2e suite.

The tools unit suite grows to 55 tests: the search-index normalisation, the print-view and SVG-favicon bundling rules, the print-asset link check, and the fresh-build link check (docs/book is a gitignored product, so the gate rebuilds the book to check it).

All 1173 tests pass (1176-1181 when mdbook is on PATH, depending on the system-tool assertions in the SBOM category).

Proof Results

Platinum, 0 unproved, 0 justified, 725 VCs (725 proved) under gnatprove 16.1.0 – the total reported by adacovex prove and mirrored in /api/metrics, the 16.1.0 proof ledger, and the self-assessment docs. The manual-bundling, dashboard, and SBOM changes are build-time or I/O-bound code that adds no analysed Ada, so the VC total stays at the Platinum bar. The Route expression function gains one more elsif for the /docs/ trailing-slash spelling and remains proved by definition.

Traceability

  • HLR-DOC / HLR-DASH – C1 mdBook manual + Read the Docs, C2 bundled offline manual at /docs, C8 mdBook search in the bundle, C10 audience folders, H2 docs links moved to the top bar, H7 Read the Docs build deploy, C13 the gitignored docs/book and the committed spec, tools/gen-docs.py, and the make book target.

  • HLR-DASH – C3 API playground clickable links, C4 yace theme variables, C6 refreshed Charts preview + new API tab preview and the completed dashboard walk-through, C9 the docs-links bar and split API view, C12 the offline print button and the stable search index name.

  • HLR-SBOM – H1 vendored yace.js in the SBOM, H6 mdbook as a system dev dependency, and the vendored/dashboard JavaScript layout separation.

  • HLR-ARCH – C5 complexity-check book directory exclusion, C7 the book-links-check gate and the complete-book restructure, H4 the chunked blob that keeps the bundled manual provable.

  • HLR-SERVER – H3 the Docs_Subpath off-by-one fix, H5 the worker-pool idle-connection timeout, H9 the query-stripped docs asset lookup, H10 the shorter idle timeout that stops the worker pool serialising a page burst.

  • HLR-SCAN – H8 the string-literal HLR-tag fix (tags inside strings are data, not traces).

  • HLR-DOC – H11 the font-link drop that works on subpages (HTML tags wrapped in inline code so mdbook stops warning on the unclosed <mapping> / <aa> / <cache> / <relative-path> spans in the generated pages).

See docs/dashboard.md, docs/THIRD_PARTY_NOTICES.md, and .readthedocs.yaml.