Building the documentation

The site renders the repository's canonical Markdown and specification. A generated staging directory preserves their relative paths; it is not a second editable documentation tree.

Build and check

With Nix flakes enabled, run:

nix build .#docs
nix flake check --no-eval-cache
nix run .#docs-check
nix run .#browser-check

The documentation package and checks use the locked shared MkDocs toolchain. The documentation check inspects rendered internal links, section anchors, navigation, speech data and theme assets. Separate model and simulator checks exercise the proved Lean model and its finite corpus, and the model check cross-checks the compiled axiom report against the theorem manifest; none proves application behavior. See the model ledger and simulation for their exact scope.

The browser check launches the pinned Chromium build, serves the standalone simulator on a temporary loopback port, and executes its manual-control and story assertions. The canonical runner is tools/browser-check.mjs; the earlier callback under simulator/ is retained as historical browser evidence. Screenshots use a temporary writable directory; no browser download or external service is required during execution. Set KEEP_BROWSER_EVIDENCE=1 to retain successful browser evidence. CI's build gate realizes the packages, executing checks, and development-shell inputs before the downstream verification jobs.

Ordinary binaries and explicit test builds

As a release operator, I build ordinary singular and open-datum with the manual Cabal test-harness flag disabled. Both executable closures use the ordinary registry CLI modules. The release archive and publication commands select these ordinary outputs.

As a contributor, I exercise crash windows and provider-answer loss with the separately named test outputs. Their registry CLI modules retain the original hold/drop controls and SINGULAR_HARNESS_TRIE_TRACE, an independent observation of the trie capability's actual operations. That diagnostic is a hidden test input and its evidence belongs to the test build.

nix build ./offchain#singular
nix build ./applications/open-datum/offchain#open-datum
nix build ./offchain#singular-test-harness
nix build ./applications/open-datum/offchain#open-datum-test-harness
nix run .#release-build-control
nix run .#demo1-cli-test-harness

The build control strips and inspects both ordinary compiled executables, reads the actual resolved registry CLI flag, and deliberately rejects the hook-bearing test artifacts and opposite flag polarity. CI runs the ordinary extracted-release journey separately from the test journey's unchanged recovery, race, node-loss and trie-observation assertions. CLI recovery and conformance backend controls select the explicit test composition. The separate replay-fault project remains a deliberately altered test build; its named refusal proof retains its published pending cases. Test outputs are never substituted into the ordinary release verifier or published as ordinary release artifacts.

flowchart TB
    Source[Registry CLI source] -->|flag disabled| Ordinary[Ordinary binaries]
    Ordinary -->|inspect bytes and flags| Exclusion[Release build control]
    Exclusion -->|checks pass| Journey[Ordinary archive journey]

flowchart TB
    Source[Registry CLI source] -->|flag enabled explicitly| Tests[Test binaries]
    Tests -->|faults and diagnostics| Recovery[Recovery controls]
    Recovery -->|assertions pass| Evidence[Test receipts]

Generated API references

The site ships a generated reference for each library a contributor calls into, built from the same revision as the pages that link it. Which code has one, and what stands in for it where there is none:

Code	Reference on this site
The off-chain registry library's public modules	Haddock: the off-chain API reference, including the four modules it re-exports from the public local-services library
The Conformance library	Haddock: the Conformance API reference
The registry validators under onchain/	aiken docs from the onchain flake's pinned compiler: the validator API reference
The runtime service modules outside the library's extent	None generated; the Runtime service ownership page records which module owns which concern
The off-chain and Conformance executables and test suites	None generated; the registry command owners and Conformance suite owners pages link their sources
The naming validators under naming-onchain/	None generated; a separate Aiken project, documented by record value and recovery

Executables, test suites and the runtime service modules outside the library's extent have no generated pages here. That coverage gap stays visible, exactly as the off-chain reference's own page records it: wider generated coverage is a separate decision for the epic's owner, not one this page takes. Each generated reference carries a manifest binding its pages to the digests of the source it was generated from, and the documentation check fails when a page, its source or its link targets no longer agree.

The repository code inventory

just inventory maps every file the tree actually holds to its lint policy and its format policy — or, for data and artifacts, to a named non-code class — and fails on anything unmapped. Discovery walks the tree itself (extensions, shebangs, executable mode and component manifests), so a new source file in a covered directory is mapped without editing anything, while a file nobody classified fails with a named diagnostic instead of passing silently. The same inventory runs over the Nix flake source, where no Git directory exists, through nix run .#inventory-check; pull-request CI runs both forms so the two contexts cannot drift. The checked registry lives in tools/code_inventory.py.

The inventory is a mapping, not enforcement: its report names the CI carrier that executes each policy, and every lint and format policy is enforced — no code family is left without a checker, and no source directory is excluded. just inventory-controls runs the negative and positive controls: synthetic orphans injected into scratch copies of the classified tree, each required to produce its intended failure. The controls never touch the working tree.

Haskell formatting

The repository's Haskell trees are formatted with Fourmolu under one house configuration, fourmolu.yaml at the repository root. Every formatter entrypoint — the off-chain lint check, the Conformance format check and the root recipes below — passes that file explicitly, so a missing configuration fails loudly instead of falling back to Fourmolu's defaults, and there is no per-tree configuration to drift from it.

nix develop --quiet -c just format        # apply to every discovered Haskell source
nix develop --quiet -c just format-check  # the same check `just ci` carries

Discovery is dynamic: every Haskell source under offchain/ and conformance/ — the formerly fenced verifier sources and the evaluation spike included — with no directory exclusions, so a new file or component directory is covered with nothing to edit. The Conformance tree gets the same check in its own Nix source context through nix run .#format-check from conformance/ (CI job 'Conformance Haskell format and lint check'). just format-controls runs the negative and positive controls: a source that Fourmolu's defaults accept but the house configuration rejects must fail the check — proving the configuration is read — and its formatter correction must pass it again; a tree without the configuration must fail loudly rather than format with defaults; a newly tracked component tree outside the old directories joins the check through the Git index, while ignored untracked build noise never enters it and a tracked file under an ignored path stays. The controls run over scratch copies and never touch the working tree.

HLint runs over the same discovered extent with no exclusions and no ignore file: nix run .#lint from offchain/ (CI job 'Off-chain lint') checks both formats and hints, and nix run .#hlint-check from conformance/ runs beside the Conformance format check.

Other languages

Every other code family the inventory discovers is linted and format-checked by one command, over the inventory's own extent, with the tools the development shell pins:

nix develop --quiet -c just lint           # the check `just ci` carries
nix develop --quiet -c just lint-fix       # apply the formatters in place
nix develop --quiet -c just lint-controls  # planted defects must fail it

Family	Format	Lint
Nix	nixfmt	statix, deadnix, Conformance lock equal to the off-chain lock
Python	ruff format	ruff check
Shell	shfmt -i 2 -ci -bn	shellcheck
JavaScript, CSS	Biome (biome.json)	Biome recommended rules
justfiles	just --fmt	the same parse
Workflow YAML	yamlfmt	actionlint with shellcheck
Lean, HTML templates	style rules	style rules

Lean and HTML have no general formatter here, so the explicit style rules are the policy: no tab, no carriage return, no trailing whitespace, and exactly one final newline. Aiken sources are checked by aiken fmt --check inside the onchain/ and naming-onchain/ flake checks, with the Aiken each flake pins; formatting leaves every compiled validator and its hash unchanged. Generated files — the shipped simulator page, the Lean mirror and the cage vectors — are regenerated from their formatted sources, and their freshness checks stay the policy. A code family nobody checks fails just lint instead of passing silently.

Edit and serve

The development shell has a separate CI build because packaged builds do not exercise it:

nix develop --quiet -c just ci
nix develop --quiet -c just serve-docs

just build-docs and just serve-docs stage the generated API references from the packaged site build, nix build .#docs, so the local site links the same generated pages the packaged site and its checks carry; the Markdown pages still reload live as they are edited.

To serve the packaged output without a live-reload editor, run the docs-serve tool (marked not-a-guarantee) with the port as its argument and open http://127.0.0.1:8000.

Publication and accessibility

Pull requests publish to a live preview with the candidate revision recorded alongside the generated site. Preview publication does not post PR comments. The default branch publishes through workflow-mode GitHub Pages after merge; the same documentation build supplies both routes.

The Terminal theme follows the system light/dark preference until a reader chooses with the toggle, and remembers that choice. Diagrams follow the same palette and open at full size in a viewer. Each section has a play button that speaks the recorded narration of its paragraphs in the Puck voice. The voice says the page text word for word: the speech companions are written by the extraction tool, which reads the prose of each rendered page, and tables, code blocks and diagrams are not spoken. The documentation check fails when a paragraph changed without its recording. just extract-speech rewrites the companions after a page edit and just narrate records the paragraphs that changed; recording needs a DeepInfra key. Diagrams are Mermaid, rendered by the copy the shared toolchain pins as a fixed-output Nix input and served from the site itself; no page loads a script or stylesheet from outside the site, and the site check fails if one does.

Documentation releases

The documentation version is the one version.txt, the release manifest and the changelog agree on; a prepared version is not evidence that an archive was tagged or published. Release-please's simple strategy updates those three surfaces together for later versions, and Nix requires the version and manifest to agree. These are documentation versions, not deployed protocol versions.

After a successful main-branch gate, repository-scoped App credentials let release-please prepare a release PR whose changes trigger normal CI. It plans PRs only: release creation is disabled because upstream release creation posts a PR comment. Merging the release PR prepares the version but does not tag or publish it. An operator-authorized v<version> tag on that merged release PR's exact commit triggers publication. The commit must belong to main, and tag, manifest and version must agree.

The tag workflow builds and checks a Nix-produced documentation archive and checksum, publishes them to the matching GitHub release, downloads and verifies the uploaded bytes, then changes the release PR's pending label to tagged. It accepts a pending or already-tagged matching PR so interrupted publication can be retried. It does not post PR comments. CI has a manual recovery trigger; no release workflow or tag is dispatched merely by adding this automation.

Build the documentation archive locally with nix build .#docs-release, and run version, workflow and artifact checks with nix run .#release-check. The archive contains the rendered site and speech data plus a complete review workspace under artifacts/review/: model and theorem sources, finite corpora, scenarios, simulator and replay sources, checkers, and a minimal flake with its exact lock. The inner artifacts/SHA256SUMS authenticates every review input plus the separately served corpus and identity files; the outer SHA256SUMS authenticates the archive.

Packaging checks alone do not establish reproduction. Extract the built singular-docs-<version>.tar.gz into a fresh directory, change to that directory, run sha256sum --check artifacts/SHA256SUMS, then run nix run --no-write-lock-file ./artifacts/review#check. Nix may acquire the exact locked toolchain when it is not cached; the model, scenario, simulator, replay, checker, and configuration inputs all come from the archive. Provenance comes from the validated tag and build binding. Published releases, each produced by this workflow from a tag on main, are listed at https://github.com/lambdasistemi/singular/releases.

The initial empty-manifest behavior and version override follow the release-please manifest documentation. Publishing remains a separate action from reviewing this documentation.