Skip to content

doc: publish doc-gen4 API documentation to GitHub Pages #4

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
kim-em merged 1 commit into from
Jul 3, 2026
Merged

doc: publish doc-gen4 API documentation to GitHub Pages #4

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
48 changes: 48 additions & 0 deletions .github/workflows/docs.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
3 changes: 3 additions & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1,4 @@
.lake/
# Generated by docgen-action at CI time (copied into docs/docs); never committed.
docs/docs/

2 changes: 2 additions & 0 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,8 @@
Verified computational algebra in Lean 4: an aggregator for the released
`hex` libraries.

API documentation: <https://leanprover.github.io/hex/docs>

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
Expand Down
Empty file added docs/.nojekyll
View file
Open in desktop
Empty file.
5 changes: 5 additions & 0 deletions docs/index.html
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
<!doctype html>
<meta charset="utf-8">
<title>hex — API documentation</title>
<meta http-equiv="refresh" content="0; url=./docs/">
<p><a href="./docs/">hex API documentation</a></p>
Loading