chrisflav · chrisflav · Jun 29, 2026 · Jun 28, 2026 · Jun 28, 2026 · Jun 28, 2026
diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
@@ -5,11 +5,8 @@ on:
   pull_request:
   workflow_dispatch:
 
-# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
 permissions:
   contents: read # Read access to repository contents
-  pages: write # Write access to GitHub Pages
-  id-token: write # Write access to ID tokens
 
 jobs:
   build:
@@ -26,4 +23,6 @@ jobs:
       # Run mathlib's environment linters on the staging library.
       - name: Run environment linters
         run: lake lint
-      - uses: leanprover-community/docgen-action@v1
+      # Building the API documentation and the upstreaming dashboard and
+      # deploying them to GitHub Pages is handled by `pages.yml`, so that both
+      # share the single GitHub Pages deployment.
diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml
@@ -0,0 +1,85 @@
+name: GitHub Pages (docs + dashboard)
+
+# Builds the API documentation and the Verso upstreaming dashboard and publishes
+# them together to GitHub Pages: the docs at `/docs` and the dashboard at
+# `/dashboard`. They share a single GitHub Pages deployment (only one is allowed
+# per repository), so this is the only workflow that deploys to Pages.
+
+on:
+  push:
+    branches: [master]
+  workflow_dispatch:
+
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+concurrency:
+  group: github-pages
+  cancel-in-progress: false
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v5
+      - uses: actions/configure-pages@v5
+
+      # --- API documentation (build only; deployment happens together below). ---
+      - name: Build API documentation
+        uses: leanprover-community/docgen-action@v1
+        with:
+          deploy: false
+
+      # --- Dashboard: generate the graph chapter (Lean v4.32.0-rc1), then build
+      #     the Verso site (Lean v4.31.0). elan selects the toolchain per directory. ---
+      - name: Install elan
+        run: |
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      - name: Get mathlib build cache
+        run: lake exe cache get || true
+
+      - name: Generate the graph chapter
+        run: |
+          lake build MathlibStaging upstream
+          lake exe upstream viz --decls --format verso \
+            --out dashboard/UpstreamingBlueprint/Chapters/Graph.lean
+
+      - name: Build dashboard site
+        run: ./dashboard/scripts/ci-pages.sh
+
+      # --- Assemble the combined site: docs at /docs, dashboard at /dashboard. ---
+      - name: Assemble site
+        run: |
+          mkdir -p _site
+          # docgen-action leaves the built API docs under `docs/` (served at /docs).
+          if [ -d docs ]; then cp -r docs/. _site/; fi
+          mkdir -p _site/dashboard
+          cp -r dashboard/_out/site/html-multi/. _site/dashboard/
+          cat > _site/index.html <<'HTML'
+          <!doctype html>
+          <meta charset="utf-8">
+          <title>mathlib-staging</title>
+          <h1>mathlib-staging</h1>
+          <ul>
+            <li><a href="docs/">API documentation</a></li>
+            <li><a href="dashboard/">Upstreaming dashboard</a></li>
+          </ul>
+          HTML
+
+      - uses: actions/upload-pages-artifact@v3
+        with:
+          path: _site
+
+  deploy:
+    needs: build
+    runs-on: ubuntu-latest
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    steps:
+      - id: deployment
+        uses: actions/deploy-pages@v4
diff --git a/.gitignore b/.gitignore
@@ -1 +1,3 @@
 /.lake
+/dashboard/.lake
+/dashboard/_out
diff --git a/Upstream.lean b/Upstream.lean
@@ -390,6 +390,52 @@ def vizDot (graph : NameMap (Array Name)) (prOf : Name → Option Nat) : String
   lines := lines.push "}"
   return String.intercalate "\n" lines.toList
 
+/-- A Verso blueprint label for a node: its name with every non-alphanumeric
+character replaced by `_`. -/
+def sanitizeLabel (n : Name) : String :=
+  String.ofList (n.toString.toList.map fun c => if c.isAlphanum || c == '_' then c else '_')
+
+/-- The graph as a Verso blueprint chapter (`#doc`): one `:::definition` node per
+unit, with `{uses …}` edges for its staging dependencies. Verso renders these as a
+graph and colours each node by status — a node with no staging dependencies is
+*ready* (blue, directly upstreamable); one that depends on other staging
+declarations is *blocked* (amber) — which matches our upstreaming model. -/
+def vizVerso (kind : String) (graph : NameMap (Array Name)) (prOf : Name → Option Nat) : String :=
+  Id.run do
+  let metrics := allMetrics graph
+  -- Assign each node a unique, readable label.
+  let mut labelOf : NameMap String := {}
+  let mut used : Array String := #[]
+  for (n, _) in graph do
+    let base := let b := sanitizeLabel n; if b.isEmpty then "node" else b
+    let mut lbl := base
+    let mut i := 2
+    while used.contains lbl do
+      lbl := base ++ "_" ++ toString i
+      i := i + 1
+    used := used.push lbl
+    labelOf := labelOf.insert n lbl
+  let header :=
+    "import Verso\nimport VersoManual\nimport VersoBlueprint\n\n\
+     open Verso.Genre\nopen Verso.Genre.Manual\nopen Informal\n\n\
+     #doc (Manual) \"Staging dependency graph (" ++ kind ++ ")\" =>\n\n\
+     Staging-internal dependency graph of `MathlibStaging` " ++ kind ++ ". \
+     Nodes with no staging dependencies are *ready* (directly upstreamable); nodes \
+     depending on other staging declarations are *blocked* until those land upstream.\n"
+  let mut blocks := #[header]
+  for (n, deps) in graph do
+    let lbl := (labelOf.find? n).getD "node"
+    let m := (metrics.find? n).getD default
+    let prNote := match prOf n with | some p => s!", in mathlib PR #{p}" | none => ""
+    let usesLine :=
+      if deps.isEmpty then ""
+      else "\n" ++ String.intercalate " "
+        (deps.filterMap fun d => (labelOf.find? d).map fun dl => "{uses \"" ++ dl ++ "\"}[]").toList
+    blocks := blocks.push <|
+      ":::definition \"" ++ lbl ++ "\"\n`" ++ n.toString ++ "` — depth " ++ toString m.depth ++
+      ", " ++ toString m.trans.size ++ " transitive staging deps" ++ prNote ++ "." ++ usesLine ++ "\n:::"
+  return String.intercalate "\n\n" blocks.toList ++ "\n"
+
 /-- Implementation of `lake exe upstream viz`. -/
 def runViz (p : Parsed) : IO UInt32 := do
   let decls := p.hasFlag "decls"
@@ -406,10 +452,12 @@ def runViz (p : Parsed) : IO UInt32 := do
       let ctx : Core.Context := { options := {}, fileName := "<upstream>", fileMap := default }
       let graph ← Prod.fst <$> CoreM.toIO (stagingDeclGraph env) ctx { env }
       pure <| if fmt == "dot" then vizDot graph prOf
+        else if fmt == "verso" then vizVerso "declarations" graph prOf
         else (vizJson "decls" graph (fun n => (env.getModuleFor? n).getD .anonymous) prOf).pretty
     else
       let graph := stagingFileGraph env
       pure <| if fmt == "dot" then vizDot graph (fun _ => none)
+        else if fmt == "verso" then vizVerso "files" graph (fun _ => none)
         else (vizJson "files" graph id (fun _ => none)).pretty
   match out? with
   | some f => IO.FS.writeFile f output; IO.println s!"wrote {f}"
@@ -450,7 +498,7 @@ def vizCmd : Cmd := `[Cli|
 
   FLAGS:
     decls;             "Graph individual declarations instead of whole files."
-    "format" : String; "Output format, `json` (default) or `dot`."
+    "format" : String; "Output format: `json` (default), `dot`, or `verso` (a blueprint chapter)."
     "out" : String;    "Write to this file instead of stdout."
 ]
 

diff --git a/dashboard/UpstreamingBlueprint.lean b/dashboard/UpstreamingBlueprint.lean
@@ -0,0 +1 @@
+import UpstreamingBlueprint.Blueprint
diff --git a/dashboard/UpstreamingBlueprint/Blueprint.lean b/dashboard/UpstreamingBlueprint/Blueprint.lean
@@ -0,0 +1,22 @@
+import Verso
+import VersoManual
+import VersoBlueprint
+import VersoBlueprint.Commands.Graph
+import VersoBlueprint.Commands.Summary
+import UpstreamingBlueprint.Chapters.Graph
+
+open Verso.Genre
+open Verso.Genre.Manual
+open Informal
+
+#doc (Manual) "MathlibStaging upstreaming dashboard" =>
+
+This dashboard visualises the staging-internal dependency graph of the
+`MathlibStaging` library, to help decide what can be upstreamed to mathlib next.
+The graph is generated by `lake exe upstream viz --decls --format verso` in the
+main repository.
+
+{include 0 UpstreamingBlueprint.Chapters.Graph}
+
+{blueprint_graph}
+{blueprint_summary}
diff --git a/dashboard/UpstreamingBlueprint/Chapters/Graph.lean b/dashboard/UpstreamingBlueprint/Chapters/Graph.lean
@@ -0,0 +1,130 @@
+import Verso
+import VersoManual
+import VersoBlueprint
+
+open Verso.Genre
+open Verso.Genre.Manual
+open Informal
+
+#doc (Manual) "Staging dependency graph (declarations)" =>
+
+Staging-internal dependency graph of `MathlibStaging` declarations. Nodes with no staging dependencies are *ready* (directly upstreamable); nodes depending on other staging declarations are *blocked* until those land upstream.
+
+
+:::definition "PresheafOfModules_Submodule_toPresheafOfModules"
+`PresheafOfModules.Submodule.toPresheafOfModules` — depth 5, 5 transitive staging deps.
+{uses "PresheafOfModules_Submodule"}[] {uses "PresheafOfModules_restrict__"}[] {uses "PresheafOfModules_Submodule_obj"}[] {uses "PresheafOfModules_Submodule_map_mem"}[]
+:::
+
+:::definition "PresheafOfModules_Submodule__"
+`PresheafOfModules.Submodule.ι` — depth 6, 6 transitive staging deps.
+{uses "PresheafOfModules_Submodule_toPresheafOfModules"}[] {uses "PresheafOfModules_Submodule"}[] {uses "PresheafOfModules_Submodule_obj"}[]
+:::
+
+:::definition "PresheafOfModules_Submodule"
+`PresheafOfModules.Submodule` — depth 1, 1 transitive staging deps.
+{uses "PresheafOfModules_restrict__"}[]
+:::
+
+:::definition "PresheafOfModules_Submodule_ext"
+`PresheafOfModules.Submodule.ext` — depth 3, 3 transitive staging deps.
+{uses "PresheafOfModules_Submodule"}[] {uses "PresheafOfModules_restrict__"}[] {uses "PresheafOfModules_Submodule_obj"}[]
+:::
+
+:::definition "PresheafOfModules_Submodule_sSup_obj"
+`PresheafOfModules.Submodule.sSup_obj` — depth 5, 5 transitive staging deps.
+{uses "PresheafOfModules_Submodule"}[] {uses "PresheafOfModules_Submodule_instCompleteLattice"}[] {uses "PresheafOfModules_Submodule_obj"}[]
+:::
+
+:::definition "PresheafOfModules_Submodule_bot_obj"
+`PresheafOfModules.Submodule.bot_obj` — depth 5, 5 transitive staging deps.
+{uses "PresheafOfModules_Submodule"}[] {uses "PresheafOfModules_Submodule_instCompleteLattice"}[] {uses "PresheafOfModules_Submodule_obj"}[]
+:::
+
+:::definition "PresheafOfModules_Submodule_ext_iff"
+`PresheafOfModules.Submodule.ext_iff` — depth 4, 4 transitive staging deps.
+{uses "PresheafOfModules_Submodule"}[] {uses "PresheafOfModules_Submodule_ext"}[] {uses "PresheafOfModules_Submodule_obj"}[]
+:::
+
+:::definition "PresheafOfModules_Submodule_sInf_obj"
+`PresheafOfModules.Submodule.sInf_obj` — depth 5, 5 transitive staging deps.
+{uses "PresheafOfModules_Submodule"}[] {uses "PresheafOfModules_Submodule_instCompleteLattice"}[] {uses "PresheafOfModules_Submodule_obj"}[]
+:::
+
+:::definition "PresheafOfModules_Submodule_instCompleteLattice"
+`PresheafOfModules.Submodule.instCompleteLattice` — depth 4, 4 transitive staging deps.
+{uses "PresheafOfModules_Submodule"}[] {uses "PresheafOfModules_Submodule_obj"}[] {uses "PresheafOfModules_Submodule_instPartialOrder"}[]
+:::
+
+:::definition "PresheafOfModules_Submodule_toPresheafOfModules_map_apply"
+`PresheafOfModules.Submodule.toPresheafOfModules_map_apply` — depth 6, 6 transitive staging deps.
+{uses "PresheafOfModules_Submodule_toPresheafOfModules"}[] {uses "PresheafOfModules_Submodule"}[] {uses "PresheafOfModules_Submodule_obj"}[]
+:::
+
+:::definition "PresheafOfModules_restrict___apply"
+`PresheafOfModules.restrictₛₗ_apply` — depth 1, 1 transitive staging deps.
+{uses "PresheafOfModules_restrict__"}[]
+:::
+
+:::definition "PresheafOfModules_Submodule_le_iff"
+`PresheafOfModules.Submodule.le_iff` — depth 4, 4 transitive staging deps.
+{uses "PresheafOfModules_Submodule"}[] {uses "PresheafOfModules_Submodule_obj"}[] {uses "PresheafOfModules_Submodule_instPartialOrder"}[]
+:::
+
+:::definition "PresheafOfModules_restrict__"
+`PresheafOfModules.restrictₛₗ` — depth 0, 0 transitive staging deps.
+:::
+
+:::definition "PresheafOfModules_Submodule___app_hom_apply"
+`PresheafOfModules.Submodule.ι_app_hom_apply` — depth 7, 7 transitive staging deps.
+{uses "PresheafOfModules_Submodule_toPresheafOfModules"}[] {uses "PresheafOfModules_Submodule__"}[] {uses "PresheafOfModules_Submodule"}[] {uses "PresheafOfModules_Submodule_obj"}[]
+:::
+
+:::definition "PresheafOfModules_Submodule_map"
+`PresheafOfModules.Submodule.map` — depth 3, 3 transitive staging deps.
+{uses "PresheafOfModules_Submodule"}[] {uses "PresheafOfModules_restrict__"}[] {uses "PresheafOfModules_Submodule_obj"}[]
+:::
+
+:::definition "PresheafOfModules_Submodule_obj"
+`PresheafOfModules.Submodule.obj` — depth 2, 2 transitive staging deps.
+{uses "PresheafOfModules_Submodule"}[]
+:::
+
+:::definition "PresheafOfModules_Submodule_top_obj"
+`PresheafOfModules.Submodule.top_obj` — depth 5, 5 transitive staging deps.
+{uses "PresheafOfModules_Submodule"}[] {uses "PresheafOfModules_Submodule_instCompleteLattice"}[] {uses "PresheafOfModules_Submodule_obj"}[]
+:::
+
+:::definition "PresheafOfModules_Submodule_sup_obj"
+`PresheafOfModules.Submodule.sup_obj` — depth 5, 5 transitive staging deps.
+{uses "PresheafOfModules_Submodule"}[] {uses "PresheafOfModules_Submodule_instCompleteLattice"}[] {uses "PresheafOfModules_Submodule_obj"}[]
+:::
+
+:::definition "PresheafOfModules_Submodule_toPresheafOfModules_obj"
+`PresheafOfModules.Submodule.toPresheafOfModules_obj` — depth 6, 6 transitive staging deps.
+{uses "PresheafOfModules_Submodule_toPresheafOfModules"}[] {uses "PresheafOfModules_Submodule"}[] {uses "PresheafOfModules_Submodule_obj"}[]
+:::
+
+:::definition "PresheafOfModules_Submodule_map_mem"
+`PresheafOfModules.Submodule.map_mem` — depth 4, 4 transitive staging deps.
+{uses "PresheafOfModules_Submodule"}[] {uses "PresheafOfModules_Submodule_map"}[] {uses "PresheafOfModules_Submodule_obj"}[]
+:::
+
+:::definition "Submodule_comap_iInf_"
+`Submodule.comap_iInf'` — depth 0, 0 transitive staging deps.
+:::
+
+:::definition "PresheafOfModules_Submodule_inf_obj"
+`PresheafOfModules.Submodule.inf_obj` — depth 5, 5 transitive staging deps.
+{uses "PresheafOfModules_Submodule"}[] {uses "PresheafOfModules_Submodule_instCompleteLattice"}[] {uses "PresheafOfModules_Submodule_obj"}[]
+:::
+
+:::definition "PresheafOfModules_Submodule_instMono_"
+`PresheafOfModules.Submodule.instMonoι` — depth 7, 7 transitive staging deps.
+{uses "PresheafOfModules_Submodule_toPresheafOfModules"}[] {uses "PresheafOfModules_Submodule__"}[] {uses "PresheafOfModules_Submodule"}[] {uses "PresheafOfModules_Submodule_obj"}[]
+:::
+
+:::definition "PresheafOfModules_Submodule_instPartialOrder"
+`PresheafOfModules.Submodule.instPartialOrder` — depth 3, 3 transitive staging deps.
+{uses "PresheafOfModules_Submodule"}[] {uses "PresheafOfModules_Submodule_obj"}[]
+:::
diff --git a/dashboard/UpstreamingBlueprintMain.lean b/dashboard/UpstreamingBlueprintMain.lean
@@ -0,0 +1,12 @@
+import VersoManual
+import VersoBlueprint.PreviewManifest
+import UpstreamingBlueprint.Blueprint
+
+open Verso Doc
+open Verso.Genre Manual
+
+def main (args : List String) : IO UInt32 :=
+  Informal.PreviewManifest.blueprintMainWithPreviewData
+    (%doc UpstreamingBlueprint.Blueprint)
+    args
+    (extensionImpls := by exact extension_impls%)