Conversation
Two things made a publish cost a full render of Mathlib's declaration pages, and often produced nothing at all. The concurrency group cancelled in progress. A render takes hours and a publish pushes here whenever any library moves, so two publishes inside one render left neither finishing: seven of the last twelve runs were cancelled, one of them after more than two hours. The group now queues, which is what GitHub does well here, holding only the newest push behind the running job so the site still converges on the latest pins. And docgen-action's cache of the dependency documentation keys on the whole `lake-manifest.json`, which every publish rewrites, so it could never hit: one library moving re-rendered all of Mathlib. That cache is turned off in favour of a restore and save keyed on the revisions of the packages that are not ours, which is what those pages actually depend on, with the project's own pages deleted after the restore so they are always rendered afresh. The first run after this lands still renders cold and populates the cache; the saving appears on the next one. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
kim-em
force-pushed
the
release-docs-render-cost
branch
from
September 6, 2026 00:57
ef85f79 to
78876ab
Compare
This branch has not been deployed
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 fixes the two things that made
leanprover/hex's documentation render cost hours and frequently produce nothing. Stacked on #10059, which brings that workflow under management here; review this one for the workflow content.The concurrency group cancelled in progress. A render takes hours, and a publish pushes to the aggregate whenever any library moves, so two publishes inside one render left neither finishing. Seven of the last twelve runs were cancelled and two failed; on 5 September a run was killed at 12:30 after more than two hours by the push from the second sync that day. The group now queues, so GitHub keeps the running job and holds only the newest push behind it, and the site still converges on the latest pins without discarding a render that is nearly done.
The dependency-documentation cache could never hit.
docgen-actionkeys it onhashFiles('lake-manifest.json'), and every publish rewrites the pins in that file, so one library moving re-rendered all of Mathlib's declaration pages. Its cache is disabled in favour of a restore and save keyed on the revisions of the packages that are not ours, which is what those pages actually depend on. The project's own pages are deleted after the restore, so they are always rendered afresh and a stale page is not reachable: the key is scoped by upstream revision, and anything of ours is removed regardless.For scale, the last two successful renders: 24 August took 60 minutes (12.6 building, 42.7 rendering); 5 September took 199 minutes (34.5 building, ~165 rendering). Part of that growth is real, since hex-graph-iso, hex-resultant, the number-field pair and hex-rcf joined the published set in between, which is also why the wasted renders matter more than they used to.
The first run after this lands still renders cold and populates the cache; the saving appears on the next one.
🤖 Prepared with Claude Code