Verso upstreaming dashboard with graph visualisation - #10
Merged
chrisflav merged 8 commits intoJun 29, 2026
Conversation
First component of the upstreaming toolkit. `lake exe upstream report` ranks MathlibStaging units — whole files or individual declarations (`--decls`) — by how ready they are to upstream to mathlib, over the staging-internal dependency graph (edges to mathlib/Lean are ignored as already-upstream): * depth — longest path to a leaf; depth 0 = directly upstreamable; * deps — number of transitive staging dependencies. Filter with `--max-depth N` (e.g. `--max-depth 0` for the worklist) and `--max-deps N`; `--json` for machine output. Reuses import-graph for env loading and the declaration/module APIs. Declaration nodes are source-written decls only (compiler machinery filtered via `isGenerated`); a structure's constructor dependencies are folded into the type node so its true dependencies are counted.
`@[upstreamed N]` tags a staging declaration as being upstreamed in mathlib pull request `N`. `lake exe upstream check` collects the tags, queries the merge status of each PR via `gh api graphql` (Bors-aware: a Bors-merged PR shows as CLOSED with `[Merged by Bors]`), and reports which declarations are in merged PRs and so can be removed from staging (exiting non-zero so CI can flag cleanup). Module-system notes: * The attribute registration must be `meta` to be active during elaboration, but the standalone exe must read the tags from non-`meta` runtime code. So the env-extension + reader live in a non-`meta` `Meta.UpstreamedExt`, and the `meta` attribute in `Meta.Upstreamed` writes to it via a `meta import`. * `withImportModules` loads with `loadExts := false`, so it does not initialize env extensions; `check` uses `importModules (loadExts := true)` with `importAll` to load the (private) extension entries.
`lake exe upstream viz [--decls] [--format json|dot] [--out FILE]` emits the staging dependency graph for visualisation: * JSON — a versioned record (nodes with upstreaming status + presentation colours, edges, module groups), modelled on verso-blueprint's `GraphData` with semantics (`status`) separated from presentation (`visual`); consumed by the Verso blueprint renderer (M4). * DOT — Graphviz, nodes coloured by status (verified it renders). Node status: `upstreamable` (depth 0), `pending` (`@[upstreamed]`, read with `loadExts`), or `blocked`. Refactored the analysis into shared `stagingFileGraph` / `stagingDeclGraph` / `rowsOf` builders used by both `report` and `viz`.
… M4/M5)
A `blueprint-verso/` sub-package renders the staging dependency graph as a Verso
blueprint site, following the integration pattern of chrisflav/proetale.
* It is a self-contained Lake package with its own `lean-toolchain` (v4.31.0, the
latest verso-blueprint supports). It does NOT depend on `MathlibStaging` via
`path = ".."`, because the main library tracks mathlib master (v4.32.0-rc1) and
the toolchains would clash. Instead, `lake exe upstream viz --decls --format
verso` (new) generates the graph as a Verso chapter (`Chapters/Graph.lean`).
* Each declaration becomes a `:::definition` node with `{uses …}` edges. Verso's
automatic ready/blocked status — and its blue/amber colours — coincide with our
upstreaming model: a node with no staging dependencies is *ready* (directly
upstreamable), one that depends on other staging declarations is *blocked*.
* `.github/workflows/verso-blueprint.yml` builds the site in CI (generate the
chapter with the v4.32 toolchain, then build the site with the v4.31 toolchain)
and publishes it to the `gh-pages` branch under `dashboard/`.
Verified locally: the site builds to `_out/site/html-multi`, with the real graph
(24 declaration nodes, 62 edges); the two ready nodes are exactly the depth-0
directly-upstreamable declarations from `upstream report --max-depth 0`.
Purely a rename of the Verso dashboard sub-package directory and its references (`.gitignore`, the CI workflow paths, and the `upstream viz --out` target).
…oard # Conflicts: # Upstream.lean
GitHub Pages allows only one deployment per repository, so the API docs and the Verso dashboard must share it. Consolidate into `pages.yml` (renamed from `dashboard.yml`): on push to master it builds the API docs (`docgen-action` with `deploy: false`) and the dashboard, assembles one site (docs at `/docs`, dashboard at `/dashboard`, with a small landing page), and deploys once via the native GitHub Actions Pages flow (`upload-pages-artifact` + `deploy-pages`). `lean_action_ci.yml` no longer runs docgen or holds the Pages permissions; it is now CI checks only (build, mirror_imports, lint).
2 tasks
chrisflav
added a commit
that referenced
this pull request
Jun 29, 2026
Fixes the GitHub Pages deployment added in #10, which failed on `master`. ## Two bugs 1. **`lake: No such file or directory`** — `pages.yml` installed elan *after* the docs step, but docgen-action's build script invokes `~/.elan/bin/lake` directly. Install elan first. 2. **`409 Conflict` on the `github-pages` artifact** — docgen-action@v1 runs `upload-pages-artifact` on *every push* regardless of its `deploy` input (only its `deploy-pages` step honours the flag). So the workflow's own `upload-pages-artifact` was a second `github-pages` artifact and collided. ## Fix Since GitHub Pages allows only one deployment per repo and docgen-action insists on uploading its `docs/` directory, let docgen own the single upload + deploy instead of deploying separately. The workflow now: 1. builds the dashboard (chapter with Lean v4.32.0-rc1, Verso site with v4.31.0), 2. drops it into docgen's output dir (`docs/dashboard`) and adds a landing `docs/index.html`, 3. runs `docgen-action` (`build-page: false`), which builds the API docs into `docs/docs` and uploads + deploys the whole `docs/` tree. Resulting site: landing page at `/`, API docs at `/docs`, dashboard at `/dashboard`. (docgen's `build_docs.sh` only does `mkdir -p docs` + `cp … docs/docs`, no `rm`, so the pre-placed dashboard survives.) ## Before merging This branch is set up so the site can be deployed and tested from it. Remove the temporary bits before/after merge: - [ ] remove `fix-pages-deploy` from the `push:` trigger in `pages.yml`; - [ ] remove the `fix-pages-deploy` branch from the `github-pages` environment's deployment-branch policies. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
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.
Adds a Verso "upstreaming dashboard" that renders the staging dependency graph as a published site, following the integration pattern of chrisflav/proetale. Builds on the toolkit merged in #9.
Design
verso-blueprint is pinned to Lean v4.31.0 (no v4.32 branch), and proetale's
path = ".."dependency forces a shared toolchain. Since the main library tracks mathlib master (v4.32.0-rc1), a path-dependency would clash. So the dashboard is a self-containeddashboard/Lake package with its ownlean-toolchain(v4.31.0) that does not depend onMathlibStaging. The graph flows through generated data instead:lake exe upstream viz --decls --format versoemits the staging graph as a Verso chapter (dashboard/UpstreamingBlueprint/Chapters/Graph.lean): one:::definitionnode per declaration, with{uses …}dependency edges.Blueprint.leanincludes that chapter plus{blueprint_graph}/{blueprint_summary}.Serendipitously, Verso's automatic ready/blocked status (and its blue/amber colours) coincides with our model: a node with no staging dependencies is ready (directly upstreamable); one that depends on other staging declarations is blocked.
CI / Pages
.github/workflows/verso-blueprint.ymlis dual-toolchain: it generates the chapter with the v4.32 toolchain, then builds the site with the v4.31 toolchain, and publishes to thegh-pagesbranch underdashboard/(viaJamesIves/github-pages-deploy-action, so it coexists with the existing docgen output).Verification
Verified locally end-to-end: verso-blueprint builds, and the site generates to
dashboard/_out/site/html-multi/with the real graph — 24 declaration nodes, 62 edges; the two ready nodes are exactly the depth-0 directly-upstreamable declarations fromupstream report --max-depth 0.Caveats
gh-pagesbranch fordashboard/to serve.@[upstreamed]) status colour isn't expressible through Verso's (closed, env-computed) status enum; pending PRs are shown in the node body text rather than as a distinct colour.🤖 Generated with Claude Code