chore(blueprint): regenerate web + pdf artifacts (5-month refresh)#127
Merged
Conversation
The checked-in blueprint artifacts under `blueprint/web/` and `blueprint/print/print.pdf` were last regenerated 2026-01-09 (commit 27cfbbc, "fix(ci): Commit pre-built blueprint, simplify workflow to just deploy"); 5 months and ~120 PRs of content drift have accumulated since. Re-ran `leanblueprint pdf` and `leanblueprint web` against the current `blueprint/src/content.tex` (which IS up-to-date per `python3 blueprint/check_blueprint.py`). The refreshed artifacts now reflect content like: * "Comparing the two endings" section, the new theorem splits, the promoted bridge lemmas, and other content added in PR #89 and follow-ups. * sect0004.html alone gains ~1,800 lines (the big proofs section), and dep_graph_document.html gains ~1,100 lines. * print.pdf grew from 57,629 → 90,504 bytes. Net: 9 files, +3,576 / −315. ### Not refreshed in this PR Four import-graph artifacts under `blueprint/web/` are produced by **doc-gen4** (in the CI `Deploy documentation` workflow), not by `leanblueprint`, so they cannot be refreshed locally: * `import_graph_colored.html` * `import_graph_colored.png` * `import_graph_colored.svg` * `import_graph_full_declarations.html` The last of these still mentions deleted declarations like `contractable_map_single` / `contractable_map_pair` / `contractable_comp` / `map_coords_apply` from PRs #120/#121. Tracking as a follow-up issue; the live GitHub Pages site at the Pages deploy URL is the source of truth for those four files and IS current via the CI workflow. ### Sanity checks * `lake build` — 3527/3527, 0 warnings * `lake exe checkdecls blueprint/lean_decls` — passes * `python3 blueprint/check_blueprint.py` — 52 cites / 52 labels / 50 refs/uses / 52 lean_decls, consistent * 0 sorries
`leanblueprint web` (via plasTeX) emits a fair amount of trailing
whitespace on the HTML it produces. The first commit on this branch
inherited that, so `git diff --check main...HEAD` flagged it as
whitespace error.
Strip with `sed -i -E 's/[[:space:]]+$//' blueprint/web/{index,sect0001
..sect0006,dep_graph_document}.html`. No visible HTML difference.
`python3 blueprint/check_blueprint.py` and `lake exe checkdecls
blueprint/lean_decls` still pass.
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
The checked-in blueprint artifacts under
blueprint/web/andblueprint/print/print.pdfwere last regenerated 2026-01-09 (commit27cfbbc5, "fix(ci): Commit pre-built blueprint, simplify workflow to just deploy"); 5 months and ~120 PRs of content drift have accumulated since.Re-ran
leanblueprint pdfandleanblueprint webagainst the currentblueprint/src/content.tex(which IS up-to-date — verified bypython3 blueprint/check_blueprint.py).What refreshed
blueprint/print/print.pdfblueprint/web/dep_graph_document.htmlblueprint/web/sect0004.htmlblueprint/web/sect0002.htmlblueprint/web/sect0006.htmlblueprint/web/sect0005.htmlblueprint/web/index.htmlblueprint/web/sect0003.htmlblueprint/web/sect0001.htmlThe refresh picks up content added in PR #89 and follow-ups: the "Comparing the two endings" section, the new theorem splits, the promoted bridge lemmas, etc.
Not refreshed in this PR
Four import-graph artifacts under
blueprint/web/are produced by doc-gen4 (in the CIDeploy documentationworkflow), not byleanblueprint, so they cannot be refreshed locally:import_graph_colored.htmlimport_graph_colored.pngimport_graph_colored.svgimport_graph_full_declarations.htmlThe last of these still mentions deleted declarations like
contractable_map_single/contractable_map_pair/contractable_comp/map_coords_applyfrom PRs #120/#121. The live GitHub Pages deploy IS current (theDeploy documentationworkflow runs doc-gen4 on every push tomain), so the canonical view is fresh — only the checked-in mirror is stale. Worth a tracking issue.Sanity checks
lake build— 3527/3527, 0 warningslake exe checkdecls blueprint/lean_decls— passespython3 blueprint/check_blueprint.py— 52 cites / 52 labels / 50 refs/uses / 52 lean_decls, all consistent(
blueprint/lean_declsitself was untouched — leanblueprint had stripped its trailing newline, which I restored.)