# 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. ### C3: API playground endpoints are clickable links The API playground endpoint buttons now carry a real link on the endpoint path: clicking the path opens the raw URL in a new tab, while clicking the rest of the button still runs the endpoint live in the playground. JSON responses that reference endpoint paths (for example the `/api/...` and `/badge/...` values in `/api/endpoints`) get those paths linkified too, so a user can jump straight from a URL in the payload to the live endpoint. The endpoint catalog now lists `/docs` as an `html` endpoint. ### 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. ### C7: book-links-check gate keeps the bundled manual sound A new `make book-links-check` gate (wired into `make check`, via `tools/check-book-links.py`) verifies that every link inside the bundled offline manual resolves against the bundled assets or the deliberately-not-bundled prefixes shared with `tools/gen-docs.py`. The check runs against a **fresh** `mdbook build` from a temp copy of `docs/`, so a stale local `docs/book` can never mask a broken link. The committed artifact is the generated spec itself, gated by `python3 tools/gen-docs.py --check` (also wired into `make check`), which rebuilds the book and fails when `src/adacovex-docs_template.ads` is stale. The manual is now **complete**: every page under `docs/` (the 64 API-reference pages, the 39 changelogs, the compliance outputs, the proof ledger, the test report, credits, and third-party notices) is a book chapter, so the index pages no longer link to pages the book never builds (previously 131 broken links in the built site). Links from the manual to repo-root files (`README.md`, `CONTRIBUTING.md`, `AGENTS.md`) now point at the repository URLs instead of `../` paths that cannot resolve inside the book. The tools unit tests grow from 41 to 48. ### 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-.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. ### C9: Dashboard shows obvious docs links and a split API view The dashboard header gains a prominent **docs links bar** below the title/actions and above the tab selection. The API playground is rearranged into a split-screen layout (endpoint nav left, live response preview right), and the footer no longer carries the raw `/api/*` links or the `?theme=` embed hint -- see H2. ### 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-.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-.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/` 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. ### H2: Dashboard docs links moved from the footer to a top bar The dashboard no longer lists the raw `/api/*` URIs or the `?theme=` embed hint in the footer. The footer now carries a single "Generated by adacovex" line, and two obvious links -- **Documentation (offline manual)** (`/docs`) and **Explore the API** (jumps to the API tab) -- sit in a prominent bar at the **top of the page**, below the dashboard title and above the tab selection, where a user sees them immediately. The API playground is now a **split-screen** layout mirroring the Dependencies tab: endpoints grouped by purpose in a left-hand nav, live JSON/SVG/HTML response preview docked on the right (stacking on narrow screens). ### 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. ### H9: Docs search-result links resolve again Clicking an mdBook search result in the bundled manual returned 404. The `/docs` router dispatched on the query-string-stripped path (so `?highlight=` reached the docs route), but the asset lookup that followed read the *raw* request path, so every search result carrying `?highlight=...` (mdBook's mark-the-search-term parameter) was looked up in the wrong book-relative shape and never found. The docs asset key now derives from the query-stripped path, so a search-result link such as `/docs/usage/cli-reference.html?highlight=serve#--serve` resolves to the page, then the browser's own fragment + mark handling scrolls to the heading and highlights the term -- exactly as it does under `mdbook serve`. ### 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. ### H11: Offline manual subpages drop their font links `tools/gen-docs.py` dropped the bundling-irrelevant font stylesheet link from each bundled page, but its pattern only matched the index page's un-prefixed `fonts/` href shape. Subpages link the same stylesheet with a `path_to_root` prefix (for example `../fonts/`), so those kept the reference and the browser issued a `/fonts/...css` 404 on every subpage. The drop now matches any leading `../` prefix, so no bundled page references the unbundled font asset. ### 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 `` / `` / `` / `` spans in the generated pages). See `docs/dashboard.md`, `docs/THIRD_PARTY_NOTICES.md`, and `.readthedocs.yaml`.