From 377d021e705604d363dbb21a966b8a8e21a7daad Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 05:27:30 +0530 Subject: [PATCH 1/7] docs: Build the site with each release series and the development version. --- website/scripts/build-site.sh | 99 +++++++++++++++++++++++++++++++++++ 1 file changed, 99 insertions(+) create mode 100755 website/scripts/build-site.sh diff --git a/website/scripts/build-site.sh b/website/scripts/build-site.sh new file mode 100755 index 0000000000..55af742cda --- /dev/null +++ b/website/scripts/build-site.sh @@ -0,0 +1,99 @@ +#!/usr/bin/env bash +# Build the published site: the latest release at the root, each release +# series at /X.Y/ (its latest release, or its latest candidate before one), +# and this tree, the development version, at /dev/. A banner on every page +# says which version it documents. +# +# usage: build-site.sh [OUT] (default: website/site) +set -euo pipefail + +ROOT="$(cd "$(dirname "$0")/../.." && pwd)" +OUT="${1:-$ROOT/website/site}" +SITE_URL="${CPPVERIFY_SITE_URL:-https://swayaminsync.github.io/cpp-verify}" +WORK="$(mktemp -d)" +trap 'rm -rf "$WORK"' EXIT + +pip install -q -r "$ROOT/website/requirements.txt" + +# Builds the documentation of the tree at $1 into $2: Doxygen, then Sphinx +# with the title and banner given, and the book's sidebar check. +build_tree() { + local tree="$1" out="$2" title="$3" banner="$4" + mkdir -p "$tree/website/build/doxygen" + (cd "$tree/website/doxygen" && doxygen Doxyfile > /dev/null) + sphinx-build -q -W -b html \ + -D "html_title=$title" \ + -D "html_theme_options.announcement=$banner" \ + "$tree/website/source" "$tree/website/build" + python3 "$tree/website/scripts/verify-book-sidebar.py" + mkdir -p "$out" + cp -R "$tree/website/build/." "$out/" +} + +# The release series and the tag each publishes, newest first, as +# "SERIES TAG" lines; a final release is preferred to its candidates. +releases="$(git -C "$ROOT" tag -l 'v[0-9]*' | python3 -c ' +import re, sys +def key(tag): + m = re.fullmatch(r"v(\d+)\.(\d+)\.(\d+)(?:-rc\.(\d+))?", tag) + if not m: + return None + major, minor, patch, rc = m.groups() + # A release sorts after its candidates. + return (int(major), int(minor), int(patch), 1 if rc is None else 0, + int(rc or 0)) +latest = {} +for tag in sys.stdin.read().split(): + k = key(tag) + if k and (k[:2] not in latest or k > latest[k[:2]][0]): + latest[k[:2]] = (k, tag) +for series in sorted(latest, reverse=True): + print("%d.%d %s" % (series + (latest[series][1],))) +')" +# The newest final release, documented at the root. +latest_tag="$(echo "$releases" | awk '$2 !~ /-rc\./ { print $2; exit }')" +latest="${latest_tag#v}" + +rm -rf "$OUT" +mkdir -p "$OUT" + +dev="$(sed -n 's/^set(CPPVERIFY_VERSION \(.*\))$/\1/p' "$ROOT/clang/lib/Verify/CMakeLists.txt")" +if [[ -n "$latest" ]]; then + dev_banner="This is the documentation of the development version, $dev, \ +built from main. The latest release is $latest: \ +its documentation." +else + dev_banner="This is the documentation of the development version, $dev, \ +built from main." +fi +echo "==> dev: $dev" +build_tree "$ROOT" "$OUT/dev" "CppVerify $dev" "$dev_banner" + +while read -r series tag; do + [[ -n "$tag" ]] || continue + version="${tag#v}" + if [[ "$tag" == "$latest_tag" ]]; then + banner="This is the documentation of cpp-verify $version, the latest \ +release. The development version documents \ +what main adds." + else + banner="This is the documentation of cpp-verify $version. The latest \ +release is $latest: its documentation." + fi + echo "==> $series: $tag" + tree="$WORK/$tag" + mkdir -p "$tree" + git -C "$ROOT" archive "$tag" website docs clang/lib/Verify | tar -x -C "$tree" + build_tree "$tree" "$OUT/$series" "CppVerify $version" "$banner" + if [[ "$tag" == "$latest_tag" ]]; then + cp -R "$OUT/$series/." "$OUT/" + fi +done <<< "$releases" + +# Before any release, the development version is the root. +if [[ -z "$latest" ]]; then + cp -R "$OUT/dev/." "$OUT/" +fi + +echo "==> Done" +echo " Site: file://$OUT/index.html" From 91b0318a4165b3a59cefa4fea8d5d90adabe5c80 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 05:27:31 +0530 Subject: [PATCH 2/7] verify: Ignore the built site. --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index 79f2cb7733..ff40edb99a 100644 --- a/.gitignore +++ b/.gitignore @@ -33,6 +33,7 @@ # CppVerify Sphinx site output /website/build/ +/website/site/ /website/source/_build/ #==============================================================================# From a39fa00335641843c982e2b505a8cec389ce6663 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 05:27:32 +0530 Subject: [PATCH 3/7] verify: Publish the versioned site, built from every release tag and main. --- .github/workflows/cppverify-docs.yml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/.github/workflows/cppverify-docs.yml b/.github/workflows/cppverify-docs.yml index d00f6803ef..65b076d784 100644 --- a/.github/workflows/cppverify-docs.yml +++ b/.github/workflows/cppverify-docs.yml @@ -27,9 +27,11 @@ jobs: build: runs-on: ubuntu-latest steps: + # Every tag: each release series is built from its latest tag. - uses: actions/checkout@v4 with: submodules: recursive + fetch-depth: 0 - uses: actions/setup-python@v5 with: @@ -41,11 +43,11 @@ jobs: run: sudo apt-get update && sudo apt-get install -y doxygen - name: Build documentation - run: ./website/scripts/build-docs.sh + run: ./website/scripts/build-site.sh - uses: actions/upload-pages-artifact@v3 with: - path: website/build + path: website/site deploy: if: (github.event_name == 'push' || github.event_name == 'workflow_dispatch') && github.ref == 'refs/heads/main' From 90c6ec24a509b0fea4600482224688148c9ee803 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 05:27:32 +0530 Subject: [PATCH 4/7] verify: Link each release to its own documentation and publish it. --- .github/workflows/cppverify-release.yml | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/.github/workflows/cppverify-release.yml b/.github/workflows/cppverify-release.yml index 5e9368d37d..8b931973ee 100644 --- a/.github/workflows/cppverify-release.yml +++ b/.github/workflows/cppverify-release.yml @@ -86,6 +86,7 @@ jobs: esac llvm="$(dist/cpp-verify/bin/cpp-verify --version | sed -n 's/^ based on LLVM \([0-9.]*\).*/\1/p')" name="cpp-verify-$version-llvm$llvm-${{ matrix.platform }}" + series="$(echo "$version" | cut -d. -f1,2)" mv dist/cpp-verify "dist/$name" cp LICENSE.TXT "dist/$name/LICENSE.TXT" cp third_party/z3/LICENSE.txt "dist/$name/LICENSE-Z3.txt" @@ -98,7 +99,7 @@ jobs: cvc5 (--backend=cvc5, portfolio, race) and Lean (--lean-certify) are found on PATH; cpp-verify --version shows what it finds. - Documentation: https://swayaminsync.github.io/cpp-verify/ + Documentation: https://swayaminsync.github.io/cpp-verify/$series/ EOF tar -C dist -cJf "$name.tar.xz" "$name" shasum -a 256 "$name.tar.xz" > "$name.tar.xz.sha256" @@ -147,6 +148,7 @@ jobs: runs-on: ubuntu-latest permissions: contents: write + actions: write steps: - uses: actions/download-artifact@v4 with: @@ -157,11 +159,12 @@ jobs: GH_TOKEN: ${{ github.token }} run: | version="${TAG#v}" + series="$(echo "$version" | cut -d. -f1,2)" flags=() case "$version" in *-*) flags+=(--prerelease) ;; esac cat > notes.md < Date: Wed, 21 Oct 2026 05:27:33 +0530 Subject: [PATCH 5/7] docs: Describe the versioned site and how it is built and published. --- website/README.md | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/website/README.md b/website/README.md index d019045573..7978a5f1d5 100644 --- a/website/README.md +++ b/website/README.md @@ -1,6 +1,18 @@ # CppVerify documentation site -Published at [swayaminsync.github.io/cpp-verify](https://swayaminsync.github.io/cpp-verify/). +Published at [swayaminsync.github.io/cpp-verify](https://swayaminsync.github.io/cpp-verify/): + +| Path | Documents | Built from | +|------|-----------|------------| +| `/` | The latest release | Its tag | +| `/X.Y/` | Release series X.Y (`/0.1/`) | The series' latest tag; before its release, its latest candidate | +| `/dev/` | The development version | `main` | + +A banner on every page names the version and links to the others. +`scripts/build-site.sh` builds all of them into `website/site/` (each tag from +`git archive`, so tags must be fetched), and `cppverify-docs.yml` publishes +it whenever `main` changes. Only `main` may deploy, so publishing a release +(`cppverify-release.yml`) runs that workflow on `main` to add the new tag. ## Outputs @@ -19,6 +31,13 @@ open website/build/index.html open website/build/doxygen/index.html ``` +The whole site, every version: + +```bash +./website/scripts/build-site.sh +open website/site/index.html +``` + Auto-install Doxygen when possible: ```bash From c859ed76e03a8cd04850f9e589242aa63db40467 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 05:27:33 +0530 Subject: [PATCH 6/7] docs: Link the development version's documentation from the README. --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 7f05b5dfc9..a843119d81 100644 --- a/README.md +++ b/README.md @@ -4,7 +4,7 @@ Formal verification lets you treat correctness as an engineering artifact: you state what should be true, and the tool either proves it or gives you a precise reason it does not. CppVerify brings that discipline to everyday C++ without a separate language or annotation dialect. -📖 **[Documentation](https://swayaminsync.github.io/cpp-verify/)** — install guide, the book (Part I–II), language reference, and Doxygen API. +📖 **[Documentation](https://swayaminsync.github.io/cpp-verify/)** — install guide, the book (Part I–II), language reference, and Doxygen API, for the latest release; [the development version](https://swayaminsync.github.io/cpp-verify/dev/) documents `main`. This repository is an [LLVM/Clang](https://github.com/llvm/llvm-project) fork (base `llvmorg-23.1.3`) with a verification engine in `clang/lib/Verify`, discharged by Z3, cvc5, or Lean. From e824fba6a6c2b5caae47fe136b547c7fbb6f26f7 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 05:27:34 +0530 Subject: [PATCH 7/7] docs: Add the versioned documentation to the 0.2.0 release notes. --- website/source/release-notes.rst | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index b8abf5d90b..889f498cfc 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -147,6 +147,13 @@ queries could run another function's long query, delaying its result and spending its ``--function-timeout``. A waiting function now runs only its own queries (:doc:`language/tooling`). +**Documentation for each version.** The site showed only ``main``, so a user +of a release read about features their binary did not have. Its root now +documents the latest release, ``/X.Y/`` each release series (``/0.1/`` is +0.1.1), and ``/dev/`` the development version on ``main``. A banner on every +page names its version, and each release's archive and notes link to its own +series. + **cvc5 1.4.** Every query over sets, multisets, and maps failed with cvc5 1.4, which requires extended arrays for constant arrays; such a query now enables them itself (:doc:`language/tooling`).