Skip to content

Add Sphinx documentation site with TikZ figures and CI deploy workflow#13

Merged
ttj merged 1 commit intoverivital:mainfrom
Kiguli:add-sphinx-docs
Apr 24, 2026
Merged

Add Sphinx documentation site with TikZ figures and CI deploy workflow#13
ttj merged 1 commit intoverivital:mainfrom
Kiguli:add-sphinx-docs

Conversation

@Kiguli
Copy link
Copy Markdown
Collaborator

@Kiguli Kiguli commented Apr 20, 2026

Summary

Adds a new docs/ Sphinx site (Furo theme, sphinx_design cards,
MyST, sphinx-autoapi, sphinxcontrib-mermaid) covering everything
BehaVerify offers, plus a GitHub Actions workflow that builds and
publishes it to GitHub Pages on every push to main.

What lands

  • Landing page with a TikZ-rendered pipeline diagram showing the
    five-stage flow: inputs (.tree / .onnx / .smv) →
    core pipeline (TextX parser, model builder, internal IR) →
    code generators (nuxmv / python / cpp / haskell / latex /
    monitor) → artefacts → three verification strategies.
  • Getting started: installation (incl. nuXmv + ONNX), quickstart
    on examples/DrunkenDrone/, first-model tutorial.
  • User guide: DSL reference, component taxonomy with a backend
    coverage matrix, generation modes, specification logics (INVAR /
    LTL / CTL + contingency monitors), neural-network leaves,
    encodings, and verification strategies.
  • Theory (new dedicated section, grounded in the four BehaVerify
    papers): behavior-tree formalism with Colledanchise-style oval
    conditions / rectangle actions, specification logics, BT → SMV
    translation (fast-forwarding + variable staging), model checking
    with nuXmv (BDDs / BMC / IC3), end-to-end soundness argument with a
    two-row serpentine chain diagram, neuro-symbolic encoding, stateful
    BTs, contingency monitors.
  • Examples: DrunkenDrone, Collatz, ACAS-Xu, Simple Robot with NN,
    and Grid-World (the 2055-node scalability benchmark).
  • Developer: architecture, adding-a-mode, adding-a-check, testing,
    contributing.
  • Reference: CLI, file formats, glossary, publications.

Every tree diagram and the pipeline / encoding / soundness figures are
authored in TikZ under docs/_static/tikz/ and pre-rendered to SVG +
PNG, so the Sphinx build does not require a LaTeX toolchain.
Regenerate with make -C docs tikz locally.

CI / deployment

.github/workflows/docs.yml builds the site on:

  • every push to main or master that touches docs/**,
    src/behaverify/**, or the workflow itself;
  • every PR targeting main / master (as a preview — uploads the
    HTML as a downloadable artifact, no deploy);
  • manual trigger from the Actions tab via workflow_dispatch,
    which lets a maintainer rebuild and redeploy without a new commit.

Deployment uses the official GitHub Pages actions
(configure-pages@v5, upload-pages-artifact@v3,
deploy-pages@v4) — no third-party tokens.

Maintainer steps before merging

  1. Go to https://github.com/verivital/behaverify/settings/pages and
    set Source = GitHub Actions.
  2. (Optional) Add a github-pages environment under
    `Settings → Environments` restricting deployment to the `main`
    branch.
  3. Merge this PR — the first build will fire and publish to
    `https://verivital.github.io/behaverify/\`.

Full step-by-step guide (including the manual rebuild path and TikZ
re-render instructions) is in `docs/DEPLOYMENT.md`.

Test plan

  • `sphinx-build -b html -W --keep-going -n docs docs/_build/html` passes locally (0 warnings).
  • `make -C docs tikz` regenerates all 12 figures cleanly.
  • All existing CI (`ci.yml`, `pylint.yml`, `publish.yml`) untouched.
  • After merge: verify the `Documentation` workflow's first run publishes to Pages.
  • After merge: `workflow_dispatch` from the Actions tab triggers a manual rebuild.

docs/ is a new Sphinx site built with Furo + sphinx-design + MyST
+ sphinx-autoapi + sphinxcontrib-mermaid. Landing page includes a
TikZ-rendered pipeline diagram. Theory section covers BT formalism,
specification logics, BT-to-SMV encoding, nuXmv model checking,
soundness, neuro-symbolic BTs, stateful BTs, and contingency monitors.
Every diagram is authored in TikZ and pre-rendered to SVG + PNG so the
Sphinx build has no LaTeX dependency.

.github/workflows/docs.yml builds on push to main, on pull requests
(for preview), and on manual workflow_dispatch from the Actions tab.
Deploys to GitHub Pages via the official actions/deploy-pages@v4.

docs/DEPLOYMENT.md is a step-by-step guide for the maintainer:
enable Pages (Settings -> Pages -> Source: GitHub Actions) once,
then merge this PR.
@ttj ttj merged commit ccd57cc into verivital:main Apr 24, 2026
4 of 5 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants