ci: Documentation generation with doc-gen4 - #34
Merged
Conversation
Re-add doc-gen4 documentation generation, previously reverted in #4 after `lake build ProvabilityLogic:docs` OOM'd building `coreDocs` and every subsequently forked process failed with ENOMEM. This time the docs build lives in its own job (isolated from `build`, `check-references`, `mk-all-check` so a slow/flaky docs build can't take those down too), gets extra swap for headroom against doc-gen4's memory spike, and only runs on pushes to main or manual dispatch rather than every PR. `deploy` treats it as a soft dependency: a failed docs job no longer blocks the rest of the pages site from deploying. Co-Authored-By: Claude <noreply@anthropic.com>
The runner image already ships an active /swapfile, so fallocate on that path failed with "Text file busy". Add extra swap under a different name instead. Co-Authored-By: Claude <noreply@anthropic.com>
Replace the separate swap-provisioned docs job with the layout Foundation uses and that passes there: `lake build <lib>:docs` as a step of the build job, `.lake/build/doc` in the uploaded artifacts, and `cp -r` into pages/docs on deploy. The docs step runs after the project cache is packed so the cache archive does not carry doc-gen4's HTML output. Co-Authored-By: Claude <noreply@anthropic.com>
The docs build failed with "resource exhausted (error code: 12, cannot allocate memory)" on every `<pkg>:srcUri.github` target while every `docInfo` target succeeded, so the Lean work itself fits: what fails is fork(). doc-gen4 holds the whole Mathlib+Foundation environment in one process and forks a git child per package, and the kernel's default overcommit heuristic refuses a fork that large. Set vm.overcommit_memory=1 so the copy-on-write forks are allowed, and add swap for headroom at the peak. Co-Authored-By: Claude <noreply@anthropic.com>
Every `docInfo` target succeeded even when the build failed, so RAM was never the constraint and the swap was a leftover from the initial misdiagnosis. Only the overcommit setting addresses the actual failure, which is fork() being refused. Co-Authored-By: Claude <noreply@anthropic.com>
Test whether matching Foundation's runner removes the need for the overcommit workaround: the docs build failed only on ubuntu-26.04, and Foundation builds its own docs on ubuntu-latest with no such step. Drops the overcommit step along with the pin. Co-Authored-By: Claude <noreply@anthropic.com>
SnO2WMaN
changed the title
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.
Summary
Re-adds doc-gen4 documentation generation to CI, previously merged in #1 and reverted in #4 because the docs build broke CI.
The setup now matches
Foundation, where the same thing has been passing all along:lake build ProvabilityLogic:docsas a step of thebuildjob..lake/build/docadded to the uploadedlean-artifacts.cp -r .lake/build/doc pages/docson deploy.The docs step runs after
lake pack/Save project cache(the one deviation from Foundation), so the cached archive doesn't carry doc-gen4's HTML output.Why #1 broke, and what actually fixes it
The failure was
resource exhausted (error code: 12, cannot allocate memory), but only on the<pkg>:srcUri.githubtargets — everydocInfotarget succeeded. So the Lean work itself fit fine; what failed wasfork(). doc-gen4 holds the whole environment in one process and forks a git child per package to resolve source URIs, many at once under lake's parallelism, and the kernel's overcommit heuristic refused forks that large.That turned out to be specific to the
ubuntu-26.04runner pin. Foundation builds its docs onubuntu-latestand never hits it. Moving the Lean jobs toubuntu-latestfixes the docs build on its own, with no workaround step, so the pin is dropped.Verified by CI on this branch:
Build docssrcUriENOMEM🤖 This PR was written with the assistance of Claude Code.
Test plan
Build docscompletes onubuntu-latestwith no workaround (run 32196695941, all steps green).build,check-references,mk-all-checkall pass.deploypublishespages/docsand https://formalizedformallogic.github.io/ProvabilityLogic/docs/ is live.