docs: nest doc-gen4 in a docbuild/ sub-project (mathlib pattern)#2
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>
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 #1 (the v4.31 bump) — the diff/CI here also includes #1's commits until that merges, then self-cleans.
Re-wires doc-gen4 per its own recommended usage pattern: build docs from a nested
docbuild/sub-project instead of a direct[[require]]in the main lakefile. Benefits:lake buildandlake-manifest.json.Foundationno longer inherit doc-gen4 in their dependency graph.Changes
lakefile.toml: drop the doc-gen4 require.lake-manifest.json: regenerated — doc-gen4 + its 4 deps gone, mathlib pin unchanged.docbuild/lakefile.toml+docbuild/lake-manifest.json: new nested docs project (doc-gen4 pinnedv4.31.0,Foundationrequired by path, shares../.lake/packages).Build docs→cd docbuild && lake build Foundation:docs; artifact + deploy paths →docbuild/.lake/build/doc.