Conversation
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) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds a
docsworkflow that renders doc-gen4 API documentation for the whole released hex cone (theHexAllumbrella plus all transitively-required split libraries and Mathlib) and deploys it to GitHub Pages at https://leanprover.github.io/hex/docs, linked from the README.The workflow uses
leanprover-community/docgen-action(pinned to a commit), which wraps the standarddocbuild/sub-project pattern, the doc-HTML cache keyed onlake-manifest.json, and the native Pages deploy. It preserves this repo's existing Mathlib-rebuild guard (lake exe cache getthen a guardedlake build) before handing off to the action, runs on push tomainonly, and pins every third-party action. A staticdocs/index.htmlredirect keeps the site root from 404ing; the generateddocs/docs/tree is gitignored.doc-gen4 has no "my library only" mode, so the first run renders the entire Mathlib doc cone (slow); subsequent runs restore that HTML from cache and re-render only the hex pages. GitHub Pages ("GitHub Actions" source) is already enabled on the repo.
🤖 Prepared with Claude Code