docs: Publish the documentation of each release, and of main at /dev/

.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'

.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,15 +159,23 @@ 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 <<EOF
           cpp-verify $version. What changed, what is supported, and what is not yet:
-          https://swayaminsync.github.io/cpp-verify/release-notes.html
+          https://swayaminsync.github.io/cpp-verify/$series/release-notes.html
 
           Unpack an archive and run \`bin/cpp-verify --version\`. Each archive
           has a \`.sha256\` file to check it with \`shasum -a 256 -c\`.
           EOF
           gh release create "$TAG" --repo "$GITHUB_REPOSITORY" \
             --title "cpp-verify $version" --notes-file notes.md "${flags[@]}" \
             ./*.tar.xz ./*.tar.xz.sha256
+
+      # The site documents each release series at /X.Y/, built from its tags;
+      # only main may deploy it.
+      - name: Publish the release's documentation
+        env:
+          GH_TOKEN: ${{ github.token }}
+        run: gh workflow run cppverify-docs.yml --repo "$GITHUB_REPOSITORY" --ref main

.gitignore

@@ -33,6 +33,7 @@
 
 # CppVerify Sphinx site output
 /website/build/
+/website/site/
 /website/source/_build/
 
 #==============================================================================#

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.
 

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

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 <code>main</code>. The latest release is $latest: \
+<a href=\"$SITE_URL/\">its documentation</a>."
+else
+  dev_banner="This is the documentation of the development version, $dev, \
+built from <code>main</code>."
+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. <a href=\"$SITE_URL/dev/\">The development version</a> documents \
+what <code>main</code> adds."
+  else
+    banner="This is the documentation of cpp-verify $version. The latest \
+release is $latest: <a href=\"$SITE_URL/\">its documentation</a>."
+  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"

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`).