chore(blueprint): regenerate import_graph_colored {svg,png} (refresh)#129
Merged
Conversation
…refresh) The colored module-import graph artifacts in `blueprint/web/` were last regenerated 2026-01-13 (commit 1537048); the module list they showed was missing PRs from the past 5 months of restructuring. Procedure: 1. Generate a fresh DOT via `lake exe graph /tmp/g.dot` — gives 104 `Exchangeability.*` modules from the current import graph. 2. Apply 3-way proof-based coloring: blue (#6baed6) for ViaMartingale, green (#74c476) for ViaL2, orange (#fd8d3c) for ViaKoopman, red-ish (#fc9272) for the top-level `Theorem*` files, gray (#e0e0e0) for shared infrastructure. 3. Render: `dot -Tsvg colored.dot -o ...svg` and `dot -Tpng -Gsize="24,5" colored.dot -o ...png` (the `-Gsize` bound keeps PNG dimensions and file size close to the previous artifact). 4. Post-process SVG via `scripts/make_svg_clickable.py` to add `<a xlink:href>` per node pointing at the doc page. Result: SVG has 105 clickable nodes (one per current `Exchangeability/` `.lean` file); PNG is 2304×456 / 272 KB (was 2400×508 / 293 KB). ### Still deferred * `blueprint/web/import_graph_colored.html` — the interactive sigma.js viewer. `lake exe graph file.html` produces a valid HTML with the current module list, but its node-coloring scheme is the lake default (uncolored / grayscale by `decl_count`), not the per-proof palette. Reproducing the proof colors in the interactive view would need additional sigma.js attribute injection; left for follow-up to avoid downgrading the existing colored interactive view. * `blueprint/web/import_graph_full_declarations.html` — produced by doc-gen4 inside the `docgen-action` CI step; can't be regenerated locally. The live GitHub Pages copy is refreshed on every push to main. Sanity gates pass: * `lake build` 3527/3527, 0 warnings * `lake exe checkdecls blueprint/lean_decls` passes * `python3 blueprint/check_blueprint.py` passes
…oot node Reviewer caught that the SVG had 105 node groups but only 104 \`<a>\` wrappers — the umbrella module node \`<!-- Exchangeability -->\` was left unlinked because the regex required a dot-separated suffix. Loosen the regex from \`^<!-- (Exchangeability\\.[^\\s]+) -->$\` to \`^<!-- (Exchangeability(?:\\.[^\\s]+)?) -->$\` so a bare \`Exchangeability\` matches too. Reran the script on the existing colored SVG; node groups and link wrappers are now both 105, and the root \`Exchangeability\` node links to \`https://cameronfreer.github.io/exchangeability/docs/Exchangeability.html\`.
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 colored module-import graph artifacts in
blueprint/web/were last regenerated on 2026-01-13 (commit15370489); the module list has drifted ~5 months. This PR refreshes the two static artifacts that are actually embedded as<img>inREADME.mdandhome_page/index.md:blueprint/web/import_graph_colored.svg— 105 clickable nodes (matches currentExchangeability/**/*.leancount)blueprint/web/import_graph_colored.png— 2304×456 / 272 KB (was 2400×508 / 293 KB)Procedure
lake exe graph /tmp/g.dot→ fresh uncolored DOT#6baed6for ViaMartingale, green#74c476for ViaL2, orange#fd8d3cfor ViaKoopman, red-ish#fc9272for the top-levelTheorem*files, gray#e0e0e0for shared infrastructuredot -Tsvg colored.dot -o ...svganddot -Tpng -Gsize="24,5" colored.dot -o ...pngscripts/make_svg_clickable.pyto add<a xlink:href>per nodeThis isn't a pixel-perfect reproduction of the Jan 2026 palette (the original used ~14 distinct shades subdividing each proof family); this is a simpler 3-way scheme matching the user-facing claim "Modules colored by proof".
Still deferred to a follow-up
blueprint/web/import_graph_colored.htmllake exe graph file.htmlproduces a valid sigma.js viewer with the current module list, but uses the lake-default grayscale palette (bydecl_count), not per-proof coloring. Replacing the existing colored HTML with an uncolored one would be a quality regression on the "Interactive" link. Keeping the existing file for now; proper fix needs sigma.js attribute injection.blueprint/web/import_graph_full_declarations.htmldocgen-actionCI step. Can't be regenerated locally. The live GitHub Pages copy is refreshed by the CI deploy on every push to main, so the user-facing version IS current; only the checked-in mirror is stale.Test plan
lake buildclean (3527/3527, 0 warnings)lake exe checkdecls blueprint/lean_declspassespython3 blueprint/check_blueprint.pypasses<g class="node">elements with one<a xlink:href>eachNet: 2 files (svg + png), +1,073 / −1,037 lines for SVG; binary delta for PNG.