ci: cache the docbuild incremental state around API generation - #208
Open
cameronfreer wants to merge 1 commit into
Open
ci: cache the docbuild incremental state around API generation#208cameronfreer wants to merge 1 commit into
cameronfreer wants to merge 1 commit into
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.
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.
Cache the nested
docbuild/.lake/buildaround API generation, and guard the docbuild workspace against drifting from the root.Why. Master pushes take 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). The same pattern ininfinitary-logiccut API generation from 18:43 to 1:19 on a nearby commit.What.
actions/cache/restorebeforelake build Graphon:docs,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_dispatch(not only master pushes) so the cache can be exercised from this 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. Currently in sync.Not included, deliberately: weekly docs split, committed
lean_decls,docgen-action, exact doc-gen4 commit pin, apt caching (separate PR if wanted).Validation plan:
gh workflow run build.yml --ref ci/docbuild-cachetwice (cold, then warm), then measure two or three master pushes including one touching a low module.