Repository navigation
ci: cache the docbuild incremental state around API generation - #208
Merged
Merged
Conversation
doc-gen4's incremental state lives in docbuild/.lake, a separate Lake workspace from the root .lake that lean-action caches, so every master push regenerated the API docs from scratch — nearly the whole of the 45–64 minute master runs against 6–7 minute PR runs. Restore docbuild/.lake/build before `lake build Graphon:docs` and save it immediately after successful generation, keyed by format version, OS, architecture, both toolchains, both manifests, both Lake configurations, and the exact commit, with a dependency-compatible fallback prefix that restores the latest compatible prior state. The save reuses the restore step's primary key and runs only when that key was not already restored. API generation also runs on manual dispatch so the cache can be exercised from a branch; assembly and deployment remain master-only. Add scripts/check_docbuild_sync.py, run right after checkout: the nested workspace must resolve the same toolchain and Mathlib as the root.
Retrieve the small docs entry, refreshing its last-access time, before this run adds another large root cache; eviction is by last access under the repository limit. Saving stays immediately after successful API generation.
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
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.
Cache the nested
docbuild/.lake/buildaround API generation, and guard the docbuild workspace against drifting from the root.Why. Master pushes took 45–64 minutes against 6–7 for PRs, and the gap is
lake build Graphon:docsin thedocbuildworkspace, whose incremental statelean-actionnever caches (it caches the root.lakeonly).What.
actions/cache/restoreofdocbuild/.lake/buildright after the sync guard and beforelean-action, so the small docs entry is retrieved and its last-access time refreshed before the run saves another ~2.6 GB root cache (GitHub evicts by last access under the repository limit; a two-day-old docs entry was evicted between the first two dispatches, before this reordering).actions/cache/saveimmediately after successful generation, so a later TeX/Jekyll/Pages failure cannot discard a valid cache. Keydocbuild-v1-<os>-<arch>-<hash of both toolchains, both manifests, both Lake configs>-<sha>; fallback prefix without the SHA restores the latest compatible prior state. Save only when the exact key was not already restored, using the restore step'scache-primary-key.workflow_dispatchso the cache can be exercised from a branch; assembly and deployment stay master-only.scripts/check_docbuild_sync.py, run right after checkout: docbuild's toolchain and Mathlib must match the root's.Measured on this branch (
gh workflow run build.yml):Not included, deliberately: weekly docs split, committed
lean_decls,docgen-action, exact doc-gen4 commit pin, apt caching, root-cache policy (the 2.6 GB per-SHA root cacheslean-actionsaves on PR runs are the real storage pressure; separate change).Post-merge master runs are the production check; the second master push is the decisive one.