From c2e1efc0f88c588ac3c36d5e470fb6db3abd9aea Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 3 Jul 2026 08:20:24 +0000 Subject: [PATCH] doc: publish doc-gen4 API documentation to GitHub Pages Add a `docs` workflow that renders doc-gen4 API documentation for the whole released hex cone (the HexAll umbrella plus Mathlib) via leanprover-community/docgen-action and deploys it to GitHub Pages at https://leanprover.github.io/hex/docs, linked from the README. Co-Authored-By: Claude Opus 4.8 (1M context) --- .github/workflows/docs.yml | 48 ++++++++++++++++++++++++++++++++++++++ .gitignore | 3 +++ README.md | 2 ++ docs/.nojekyll | 0 docs/index.html | 5 ++++ 5 files changed, 58 insertions(+) create mode 100644 .github/workflows/docs.yml create mode 100644 docs/.nojekyll create mode 100644 docs/index.html diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml new file mode 100644 index 0000000..35d7b06 --- /dev/null +++ b/.github/workflows/docs.yml @@ -0,0 +1,48 @@ +name: docs +on: + push: + branches: [main] +# No `workflow_dispatch`: docgen-action gates its doc build, artifact upload, +# and Pages deploy on `github.event_name == 'push'`, so a manual dispatch would +# run the Lean build and then silently skip publishing. Re-render by pushing an +# empty commit to `main`. +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true +permissions: + contents: read + pages: write + id-token: write +jobs: + docs: + runs-on: ubuntu-latest + environment: + name: github-pages + steps: + # Mathlib's generated doc HTML is large; free space so the runner doesn't fill up. + - uses: jlumbroso/free-disk-space@54081f138730dfa15788a46383842cd2f914a1be # v1.3.1 + with: + tool-cache: false + - uses: actions/checkout@v4 + with: + fetch-depth: 0 # doc-gen4 source links need full history + # Preserve the Mathlib-rebuild guard from ci.yml: fetch the olean cache and + # hard-fail if a cache miss would recompile Mathlib from source. + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + - run: lake exe cache get + - name: Build the aggregate (fail if Mathlib rebuilds from source) + run: | + set -o pipefail + lake build 2>&1 | tee build.log + if grep -qE 'Building Mathlib\b' build.log; then + echo "ERROR: Mathlib rebuilt from source (cache miss)"; exit 1; fi + # doc-gen4 renders declaration pages for the whole import cone (Mathlib + # included) in a docbuild/ sub-project that reuses ../.lake/packages, caches + # the generated HTML keyed on lake-manifest.json, and deploys to Pages. + - name: Build and deploy API documentation + uses: leanprover-community/docgen-action@10db47458f91456d87804787d3dfcd914b9a19e3 + with: + build-page: false diff --git a/.gitignore b/.gitignore index 01f8cdb..dccac6d 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,4 @@ .lake/ +# Generated by docgen-action at CI time (copied into docs/docs); never committed. +docs/docs/ + diff --git a/README.md b/README.md index bb16efe..f77ee9c 100644 --- a/README.md +++ b/README.md @@ -3,6 +3,8 @@ Verified computational algebra in Lean 4: an aggregator for the released `hex` libraries. +API documentation: + Requiring this package pulls in the whole released `hex-lll-mathlib` closure at a single coherent pinned set. The Mathlib-free computational libraries (what used to be a single `HexMatrix` is now split into a matrix layer and diff --git a/docs/.nojekyll b/docs/.nojekyll new file mode 100644 index 0000000..e69de29 diff --git a/docs/index.html b/docs/index.html new file mode 100644 index 0000000..ce4a836 --- /dev/null +++ b/docs/index.html @@ -0,0 +1,5 @@ + + +hex — API documentation + +

hex API documentation