ci: split compile vs doc generation into separate jobs (non-blocking docs)#3
Merged
Conversation
lean-toolchain v4.29.0 -> v4.31.0; mathlib and doc-gen4 requires bumped to v4.31.0, with the source migration across the Foundation library (133 files). sorry/admit baseline unchanged (27, all pre-existing upstream). doc-gen4 pinned to its v4.31.0 tag (upstream tracked `main`); flip back to `main` if preferred. Mechanical port produced with Claude Code; not yet human-reviewed. Porting cheat sheet: https://github.com/gotrevor/mathlib-bump-cookbook/blob/main/v4.29.1-to-v4.31.0.md Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Moves doc-gen4 out of the main lakefile into a nested `docbuild/` sub-project, per doc-gen4's own recommended usage pattern. The main `lake build` and lake-manifest.json no longer pull in doc-gen4 + MD4Lean / BibtexQuery / UnicodeBasic / leansqlite; downstream consumers of Foundation no longer inherit them either. Mirrors mathlib, which keeps doc-gen4 out of its own manifest entirely. Docs build moves to `cd docbuild && lake build Foundation:docs` (output at docbuild/.lake/build/doc); CI docs/artifact/deploy steps updated to match. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Separates the single `build` job into: - `build` — compiles the Foundation library (the gate) - `docs` — generates doc-gen4 docs + import graph, continue-on-error so doc-gen4 tooling breakage never blocks a green library build The docs job reuses the library build the `build` job caches (same key), so Foundation isn't recompiled. `deploy` now needs `docs` (the artifact source). Co-Authored-By: Claude Opus 4.8 <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.
Stacked on #2 (docbuild). Splits the monolithic
buildjob so library compilation and documentation generation are separate CI jobs.Why
build), independent of doc-gen4.docsjob iscontinue-on-error: true, so doc-gen4 tooling breakage (the flakiest dep across Lean bumps) shows its own status but never gates a green library PR.Shape
build(needsmk-all-check):lake build Foundation+ pack/cache-save. The gate.docs(needsbuild,continue-on-error): restores the cached library build (no recompile),cd docbuild && lake build Foundation:docs, import graph, uploads artifacts.deploy(master-only): now needsdocs(the artifact source) instead ofbuild.continue-on-errorondocs, a docs failure onmasterletsdeployproceed and fail at the copy step — acceptable signal, but you may prefer to dropcontinue-on-errorand instead markdocsnon-required in branch protection. Mechanical change produced with Claude Code; this PR's CI is the verification.