From 87003aea07f040abd3bca67f7ea91ee2df3ed284 Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Sun, 28 Jun 2026 23:00:58 +0200
Subject: [PATCH 1/7] Add `upstream report`: dependency-readiness analysis
 (toolkit M1)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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.
---
 Upstream.lean | 261 ++++++++++++++++++++++++++++++++++++++++++++++++++
 lakefile.toml |   9 ++
 2 files changed, 270 insertions(+)
 create mode 100644 Upstream.lean

diff --git a/Upstream.lean b/Upstream.lean
new file mode 100644
index 0000000..8969260
--- /dev/null
+++ b/Upstream.lean
@@ -0,0 +1,261 @@
+module
+
+public import Cli.Basic
+import ImportGraph.Imports.RequiredModules
+import ImportGraph.Lean.Environment
+import Lean.DeclarationRange
+import Lean.Data.Json
+import Lean.Util.Path
+
+/-!
+# `lake exe upstream report`
+
+First component of the upstreaming toolkit. Reports MathlibStaging *units* —
+whole files (modules) or individual declarations — ranked by how ready they are
+to be upstreamed to mathlib.
+
+For each unit we look only at its **staging-internal** dependencies: edges to
+mathlib / Lean / Batteries are ignored, because those are already upstream. Over
+that staging-only graph we compute
+
+* **depth** — the longest path to a leaf. A unit with no staging dependencies has
+  depth `0` and is *directly upstreamable*; a unit depending only on depth-`0`
+  units has depth `1`, and so on.
+* **deps** — the number of staging units it transitively depends on.
+
+Filter with `--max-depth N` (e.g. `--max-depth 0` for the directly-upstreamable
+worklist) and `--max-deps N`; use `--decls` for declaration granularity and
+`--json` for machine-readable output.
+
+Staging *infrastructure* modules (`MathlibStaging.Init`, `MathlibStaging.Linter.*`,
+`MathlibStaging.Meta.*`) and the aggregator root are not upstreaming targets and
+are excluded.
+
+Caveat: declaration dependencies are computed from `getUsedConstantsAsSet`, which
+does not see constants used only through tactics or syntax, so the declaration
+graph is a slight under-approximation.
+-/
+
+open Lean Core System Cli
+
+namespace Upstream
+
+/-- Root of the staging hierarchy. -/
+def stagingRoot : Name := `MathlibStaging
+
+/-- Whether `mod` is a staging infrastructure module (the prelude, the linters or
+the meta modules). Mirrors `MirrorImports.isInfraModule`; such modules are not
+upstreaming targets. -/
+def isInfraModule (mod : Name) : Bool :=
+  mod == `MathlibStaging.Init
+    || (`MathlibStaging.Linter).isPrefixOf mod
+    || (`MathlibStaging.Meta).isPrefixOf mod
+
+/-- Whether `mod` is a staging *content* module: under `MathlibStaging`, not the
+aggregator root, and not infrastructure. These are the upstreaming targets. -/
+def isContentModule (mod : Name) : Bool :=
+  stagingRoot.isPrefixOf mod && mod != stagingRoot && !isInfraModule mod
+
+/-- Union of two `NameSet`s. -/
+def nsUnion (a b : NameSet) : NameSet := b.foldl (init := a) fun acc n => acc.insert n
+
+/-- Per-unit metrics over the staging-internal dependency graph. -/
+structure Metrics where
+  /-- Longest path to a leaf (`0` = no staging dependencies). -/
+  depth : Nat
+  /-- The staging units transitively depended on (excluding the unit itself). -/
+  trans : NameSet
+
+instance : Inhabited Metrics := ⟨{ depth := 0, trans := {} }⟩
+
+/-- Memoized depth and transitive-dependency set of `n` in `graph` (a node → its
+direct dependencies, all within the node set). `visiting` guards against cycles
+(e.g. mutual declarations); a back-edge into the current path contributes
+nothing. -/
+partial def metricOf (graph : NameMap (Array Name)) (visiting : NameSet) (n : Name) :
+    StateM (NameMap Metrics) Metrics := do
+  if let some m := (← get).find? n then
+    return m
+  if visiting.contains n then
+    return { depth := 0, trans := {} }
+  let visiting := visiting.insert n
+  let mut depth := 0
+  let mut trans : NameSet := {}
+  for d in (graph.find? n).getD #[] do
+    let md ← metricOf graph visiting d
+    depth := Nat.max depth (md.depth + 1)
+    trans := nsUnion (trans.insert d) md.trans
+  let m := { depth, trans }
+  modify (·.insert n m)
+  return m
+
+/-- Compute metrics for every node of `graph`. -/
+def allMetrics (graph : NameMap (Array Name)) : NameMap Metrics := Id.run do
+  let mut st : NameMap Metrics := {}
+  for (n, _) in graph do
+    st := (metricOf graph {} n |>.run st).2
+  return st
+
+/-- A reported row: a unit with its defining module and metrics. -/
+structure Row where
+  /-- The unit's name (module name for files, declaration name for declarations). -/
+  name : Name
+  /-- The module the unit lives in (equals `name` for files). -/
+  module : Name
+  /-- Dependency depth. -/
+  depth : Nat
+  /-- Number of transitive staging dependencies. -/
+  deps : Nat
+
+/-- The direct import graph of every loaded module, built from module headers
+(robust, independent of which module is "main"). -/
+def fileImportGraph (env : Environment) : NameMap (Array Name) := Id.run do
+  let mut g : NameMap (Array Name) := {}
+  for (mod, idx) in env.header.moduleNames.zipIdx do
+    g := g.insert mod (env.header.moduleData[idx]!.imports.map (·.module))
+  return g
+
+/-- File-level rows: one per staging content module, over the module import graph
+restricted to staging content modules. -/
+def analyzeFiles (env : Environment) : Array Row := Id.run do
+  let graph : NameMap (Array Name) :=
+    (fileImportGraph env).filterMap fun n imps =>
+      if isContentModule n then some (imps.filter isContentModule) else none
+  let metrics := allMetrics graph
+  let mut rows := #[]
+  for (n, _) in graph do
+    let m := (metrics.find? n).getD { depth := 0, trans := {} }
+    rows := rows.push { name := n, module := n, depth := m.depth, deps := m.trans.size }
+  return rows
+
+/-- Whether `n` is an auto-generated declaration (recursor, constructor,
+`noConfusion`, internal machinery, …) rather than a source-written one, and so
+should not be reported as an upstreaming unit in its own right. -/
+def isGenerated (env : Environment) (n : Name) : Bool :=
+  n.isInternalDetail || isAuxRecursor env n || isNoConfusion env n ||
+    match env.find? n with
+    | some (.recInfo _) | some (.ctorInfo _) => true
+    | _ => false
+
+/-- Declaration-level rows: one per source-written declaration in a staging
+content module, over the declaration-use graph restricted to such declarations. -/
+def analyzeDecls (env : Environment) : CoreM (Array Row) := do
+  -- The source-written declarations living in staging content modules.
+  let mut nodes : Array Name := #[]
+  for (mod, idx) in env.header.moduleNames.zipIdx do
+    if isContentModule mod then
+      for n in env.header.moduleData[idx]!.constNames do
+        -- Keep only source-written declarations: drop compiler machinery
+        -- (`.rec`, `.mk`, `.casesOn`, `.noConfusion`, …) and anything without a source range.
+        if !isGenerated env n && (← findDeclarationRanges? n).isSome then
+          nodes := nodes.push n
+  let nodeSet : NameSet := nodes.foldl (init := {}) fun acc n => acc.insert n
+  -- Edges: a declaration depends on the staging declarations it uses.
+  let mut graph : NameMap (Array Name) := {}
+  for n in nodes do
+    let mut used := (← getConstInfo n).getUsedConstantsAsSet
+    -- A structure/inductive's real dependencies (its field types) live in its
+    -- constructors, which are not reported separately; fold them into the type node.
+    if let some (.inductInfo val) := env.find? n then
+      for ctor in val.ctors do
+        used := nsUnion used (← getConstInfo ctor).getUsedConstantsAsSet
+    let deps := used.foldl (init := #[]) fun acc e =>
+      if e != n && nodeSet.contains e then acc.push e else acc
+    graph := graph.insert n deps
+  let metrics := allMetrics graph
+  let mut rows := #[]
+  for n in nodes do
+    let m := (metrics.find? n).getD { depth := 0, trans := {} }
+    rows := rows.push
+      { name := n, module := (env.getModuleFor? n).getD .anonymous, depth := m.depth, deps := m.trans.size }
+  return rows
+
+/-- Render an aligned text table. -/
+def renderTable (headers : Array String) (rows : Array (Array String)) : String := Id.run do
+  let ncol := headers.size
+  let mut widths : Array Nat := headers.map String.length
+  for r in rows do
+    for i in [0:ncol] do
+      widths := widths.set! i (Nat.max widths[i]! (r.getD i "").length)
+  let renderRow (cells : Array String) : String :=
+    String.intercalate "  " <| (List.range ncol).map fun i =>
+      let s := cells.getD i ""
+      -- Do not pad the final column, to avoid trailing whitespace in the output.
+      if i + 1 == ncol then s else s ++ String.ofList (List.replicate (widths[i]! - s.length) ' ')
+  let sep : String :=
+    String.intercalate "  " <| (List.range ncol).map fun i => String.ofList (List.replicate widths[i]! '-')
+  return String.intercalate "\n" (renderRow headers :: sep :: (rows.map renderRow).toList)
+
+/-- The JSON encoding of a row. -/
+def rowJson (r : Row) (decls : Bool) : Json :=
+  Json.mkObj <|
+    [("name", Json.str r.name.toString), ("depth", toJson r.depth), ("transitiveDeps", toJson r.deps)]
+      ++ (if decls then [("module", Json.str r.module.toString)] else [])
+
+/-- Filter, sort and render the rows into the final output string. This must run
+while the loaded environment is still alive, because `Row` names are region
+allocated in the environment's imported data. -/
+def formatReport (rows0 : Array Row) (decls : Bool) (maxDepth? maxDeps? : Option Nat)
+    (asJson : Bool) : String := Id.run do
+  let rows := (rows0.filter fun r => maxDepth?.all (r.depth ≤ ·) && maxDeps?.all (r.deps ≤ ·)).qsort
+    fun a b =>
+      if a.depth != b.depth then a.depth < b.depth
+      else if a.deps != b.deps then a.deps < b.deps
+      else a.name.toString < b.name.toString
+  if asJson then
+    return (Json.arr (rows.map (rowJson · decls))).pretty
+  if rows.isEmpty then
+    return "(no matching units)"
+  let headers := if decls then #["depth", "deps", "declaration", "module"] else #["depth", "deps", "file"]
+  let body := rows.map fun r =>
+    if decls then #[toString r.depth, toString r.deps, r.name.toString, r.module.toString]
+    else #[toString r.depth, toString r.deps, r.name.toString]
+  return renderTable headers body ++ s!"\n\n{rows.size} unit(s); depth 0 = directly upstreamable."
+
+/-- Implementation of `lake exe upstream report`. -/
+def runReport (p : Parsed) : IO UInt32 := do
+  let decls := p.hasFlag "decls"
+  let maxDepth? : Option Nat := (p.flag? "max-depth").map (·.as! Nat)
+  let maxDeps? : Option Nat := (p.flag? "max-deps").map (·.as! Nat)
+  let asJson := p.hasFlag "json"
+  initSearchPath (← findSysroot)
+  unsafe Lean.enableInitializersExecution
+  -- All work that touches environment-owned `Name`s happens inside the closure;
+  -- only the finished `String` escapes (the env's imported data is freed on exit).
+  let output ← unsafe withImportModules #[{module := stagingRoot}] {} (trustLevel := 1024) fun env => do
+    let rows ← if decls then
+        let ctx : Core.Context := { options := {}, fileName := "<upstream>", fileMap := default }
+        Prod.fst <$> CoreM.toIO (analyzeDecls env) ctx { env }
+      else
+        pure (analyzeFiles env)
+    pure (formatReport rows decls maxDepth? maxDeps? asJson)
+  IO.println output
+  return 0
+
+/-- `lake exe upstream report` -/
+def reportCmd : Cmd := `[Cli|
+  report VIA runReport; ["0.1.0"]
+  "List MathlibStaging units by upstreaming readiness: dependency depth and \
+   number of transitive staging dependencies."
+
+  FLAGS:
+    decls;             "Report individual declarations instead of whole files."
+    "max-depth" : Nat; "Only show units with dependency depth ≤ N (0 = directly upstreamable)."
+    "max-deps" : Nat;  "Only show units with at most N transitive staging dependencies."
+    json;              "Emit JSON instead of an aligned table."
+]
+
+/-- The `upstream` command, dispatching to its subcommands. -/
+def upstreamCmd : Cmd := `[Cli|
+  upstream NOOP; ["0.1.0"]
+  "Tooling for upstreaming MathlibStaging content to mathlib."
+
+  SUBCOMMANDS:
+    reportCmd
+]
+
+end Upstream
+
+/-- `lake exe upstream` -/
+public def main (args : List String) : IO UInt32 :=
+  Upstream.upstreamCmd.validate args
diff --git a/lakefile.toml b/lakefile.toml
index c8d3dab..98d8075 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -33,3 +33,12 @@ name = "MathlibStaging"
 [[lean_exe]]
 name = "mirror_imports"
 root = "MirrorImports"
+
+# The upstreaming toolkit (see `Upstream.lean`): `lake exe upstream report`
+# ranks staging files/declarations by how ready they are to upstream to mathlib.
+# `supportInterpreter` is required because it loads the staging environment at
+# runtime via `withImportModules`.
+[[lean_exe]]
+name = "upstream"
+root = "Upstream"
+supportInterpreter = true

From 6561e61064f8dbc6df92614d43a25ee3f28287aa Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Sun, 28 Jun 2026 23:26:40 +0200
Subject: [PATCH 2/7] Add `@[upstreamed]` attribute and `upstream check`
 (toolkit M2)

`@[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.
---
 MathlibStaging.lean                    |   2 +
 MathlibStaging/Init.lean               |   6 +-
 MathlibStaging/Meta/Upstreamed.lean    |  53 +++++++++++++
 MathlibStaging/Meta/UpstreamedExt.lean |  42 ++++++++++
 Upstream.lean                          | 105 ++++++++++++++++++++++++-
 5 files changed, 204 insertions(+), 4 deletions(-)
 create mode 100644 MathlibStaging/Meta/Upstreamed.lean
 create mode 100644 MathlibStaging/Meta/UpstreamedExt.lean

diff --git a/MathlibStaging.lean b/MathlibStaging.lean
index 5b7ab14..4ca4307 100644
--- a/MathlibStaging.lean
+++ b/MathlibStaging.lean
@@ -4,3 +4,5 @@ import MathlibStaging.Algebra.Module.Submodule.Map
 import MathlibStaging.Init
 import MathlibStaging.Linter.Staging
 import MathlibStaging.Meta.Overrides
+import MathlibStaging.Meta.Upstreamed
+import MathlibStaging.Meta.UpstreamedExt
diff --git a/MathlibStaging/Init.lean b/MathlibStaging/Init.lean
index d0aca5a..968e09f 100644
--- a/MathlibStaging/Init.lean
+++ b/MathlibStaging/Init.lean
@@ -2,14 +2,16 @@ module
 
 public import MathlibStaging.Linter.Staging
 public import MathlibStaging.Meta.Overrides
+public import MathlibStaging.Meta.Upstreamed
 
 /-!
 # `MathlibStaging.Init`
 
 Every staging file must import this module (directly or transitively); the
 `mirror_imports` linter enforces this. Importing it registers the staging syntax
-linters (see `MathlibStaging.Linter.Staging`) and the `@[overrides]` attribute
-(see `MathlibStaging.Meta.Overrides`) so that they are available on every staging file.
+linters (see `MathlibStaging.Linter.Staging`) and the `@[overrides]` and
+`@[upstreamed]` attributes (see `MathlibStaging.Meta.Overrides` and
+`MathlibStaging.Meta.Upstreamed`) so that they are available on every staging file.
 
 It plays the same role for the staging library that `Mathlib.Init` plays for
 mathlib.
diff --git a/MathlibStaging/Meta/Upstreamed.lean b/MathlibStaging/Meta/Upstreamed.lean
new file mode 100644
index 0000000..11dacca
--- /dev/null
+++ b/MathlibStaging/Meta/Upstreamed.lean
@@ -0,0 +1,53 @@
+module
+
+public meta import MathlibStaging.Meta.UpstreamedExt
+public meta import Lean.Elab.Command
+
+/-!
+# The `@[upstreamed]` attribute
+
+When a declaration in the staging library has been included in a pull request to
+mathlib, it is tagged with the number of that pull request:
+
+```
+@[upstreamed 12345]
+theorem foo' ... := ...
+```
+
+records that `foo'` is being upstreamed in mathlib pull request `#12345`. Once
+that pull request is merged, the declaration lives in mathlib and can be removed
+from the staging library; `lake exe upstream check` finds such declarations by
+querying the merge status of the recorded pull requests.
+
+The attribute fails if the pull request number is not positive. The recorded
+data lives in `MathlibStaging.upstreamedExt` (see `MathlibStaging.Meta.UpstreamedExt`)
+and is queried with `MathlibStaging.getUpstreamedPR?`. The attribute registration
+here is `meta` (so it is active during elaboration); it writes to the non-`meta`
+extension by calling the non-`meta` `MathlibStaging.recordUpstreamed`.
+-/
+
+namespace MathlibStaging
+
+meta section
+
+open Lean Elab
+
+/-- The `@[upstreamed N]` attribute records that the annotated declaration is part
+of mathlib pull request `N`, opened to upstream it. See the module doc-string. -/
+syntax (name := upstreamed) "upstreamed" ppSpace num : attr
+
+initialize registerBuiltinAttribute {
+  name := `upstreamed
+  descr := "record that this declaration is being upstreamed to mathlib in the given pull request"
+  add := fun decl stx _kind => do
+    let `(attr| upstreamed $prStx:num) := stx
+      | throwError "`@[upstreamed]`: expected `@[upstreamed <pr-number>]`"
+    let pr := prStx.getNat
+    if pr == 0 then
+      throwError "`@[upstreamed]`: the pull request number must be positive"
+    recordUpstreamed decl pr
+}
+
+end
+
+end MathlibStaging
diff --git a/MathlibStaging/Meta/UpstreamedExt.lean b/MathlibStaging/Meta/UpstreamedExt.lean
new file mode 100644
index 0000000..cfbed9b
--- /dev/null
+++ b/MathlibStaging/Meta/UpstreamedExt.lean
@@ -0,0 +1,42 @@
+module
+
+public import Lean.Environment
+public import Lean.EnvExtension
+public import Lean.CoreM
+
+/-!
+# The `@[upstreamed]` tag store
+
+The non-`meta` environment extension backing the `@[upstreamed]` attribute (see
+`MathlibStaging.Meta.Upstreamed`), together with its reader and writer.
+
+These are kept `meta`-free, and separate from the attribute itself, so that the
+standalone `upstream` executable can read the recorded tags from a loaded
+environment at runtime — runtime code cannot reference `meta` declarations, and
+the attribute registration must be `meta` to be active during elaboration.
+-/
+
+open Lean
+
+namespace MathlibStaging
+
+/-- The persistent record of `@[upstreamed]` tags: pairs of a tagged declaration
+and the mathlib pull request number upstreaming it. -/
+public initialize upstreamedExt :
+    SimplePersistentEnvExtension (Name × Nat) (Array (Name × Nat)) ←
+  registerSimplePersistentEnvExtension {
+    addEntryFn := fun s e => s.push e
+    addImportedFn := fun ess => ess.foldl (· ++ ·) #[]
+  }
+
+/-- If `declName` carries an `@[upstreamed N]` attribute, returns the mathlib pull
+request number `N` it is being upstreamed in. -/
+public def getUpstreamedPR? (env : Environment) (declName : Name) : Option Nat :=
+  (upstreamedExt.getState env).find? (·.1 == declName) |>.map (·.2)
+
+/-- Record that `declName` is being upstreamed in pull request `pr`. The
+(`meta`) attribute handler writes to the extension by calling this. -/
+public def recordUpstreamed (declName : Name) (pr : Nat) : CoreM Unit :=
+  modifyEnv (upstreamedExt.addEntry · (declName, pr))
+
+end MathlibStaging
diff --git a/Upstream.lean b/Upstream.lean
index 8969260..10f7fa9 100644
--- a/Upstream.lean
+++ b/Upstream.lean
@@ -3,6 +3,7 @@ module
 public import Cli.Basic
 import ImportGraph.Imports.RequiredModules
 import ImportGraph.Lean.Environment
+import MathlibStaging.Meta.UpstreamedExt
 import Lean.DeclarationRange
 import Lean.Data.Json
 import Lean.Util.Path
@@ -222,7 +223,7 @@ def runReport (p : Parsed) : IO UInt32 := do
   unsafe Lean.enableInitializersExecution
   -- All work that touches environment-owned `Name`s happens inside the closure;
   -- only the finished `String` escapes (the env's imported data is freed on exit).
-  let output ← unsafe withImportModules #[{module := stagingRoot}] {} (trustLevel := 1024) fun env => do
+  let output ← unsafe withImportModules #[{module := stagingRoot, importAll := true}] {} (trustLevel := 1024) fun env => do
     let rows ← if decls then
         let ctx : Core.Context := { options := {}, fileName := "<upstream>", fileMap := default }
         Prod.fst <$> CoreM.toIO (analyzeDecls env) ctx { env }
@@ -232,6 +233,93 @@ def runReport (p : Parsed) : IO UInt32 := do
   IO.println output
   return 0
 
+/-! ## `lake exe upstream check` -/
+
+/-- Whether a pull request with the given `state` and `title` is merged. Accounts
+for mathlib's Bors queue: a Bors-merged PR shows up as `CLOSED` with
+`[Merged by Bors]` in its title rather than `MERGED`. -/
+def prMerged (state title : String) : Bool :=
+  state == "MERGED" || (title.splitOn "[Merged by Bors]").length > 1
+
+/-- A batched GraphQL query for the state and title of every pull request in
+`prs`, in repository `owner/name`. (Built by concatenation rather than `s!` so the
+GraphQL braces are not mistaken for interpolation.) -/
+def mergeQuery (owner name : String) (prs : Array Nat) : String :=
+  let fields := String.intercalate " " <| prs.toList.map fun n =>
+    "pr" ++ toString n ++ ": pullRequest(number: " ++ toString n ++ ") { state title }"
+  "query { repository(owner: \"" ++ owner ++ "\", name: \"" ++ name ++ "\") { " ++ fields ++ " } }"
+
+/-- Parse a `gh api graphql` response, returning whether each pull request in
+`prs` is merged. PRs that are missing/`null` in the response count as not merged. -/
+def parseMerged (out : String) (prs : Array Nat) : Except String (Array (Nat × Bool)) := do
+  let data ← (← Json.parse out).getObjVal? "data"
+  let repo ← data.getObjVal? "repository"
+  return prs.map fun n =>
+    let pr := (repo.getObjVal? s!"pr{n}").toOption.getD Json.null
+    let state := (pr.getObjVal? "state" >>= Json.getStr?).toOption.getD ""
+    let title := (pr.getObjVal? "title" >>= Json.getStr?).toOption.getD ""
+    (n, prMerged state title)
+
+/-- The staging *content* modules, read from the `MathlibStaging.lean` aggregator
+file (one `import` line per module). Avoids loading an environment merely to
+enumerate modules. -/
+def contentModulesFromAggregator : IO (Array Name) := do
+  let src ← IO.FS.readFile "MathlibStaging.lean"
+  return src.splitOn "\n"
+    |>.filterMap (fun line =>
+      if line.startsWith "import " then some (line.drop 7).toName else none)
+    |>.toArray.filter isContentModule
+
+/-- Implementation of `lake exe upstream check`. -/
+def runCheck (p : Parsed) : IO UInt32 := do
+  let repo := (p.flag? "repo").map (·.as! String) |>.getD "leanprover-community/mathlib4"
+  let parts := repo.splitOn "/"
+  unless parts.length == 2 do
+    IO.eprintln s!"--repo must be of the form `owner/name`, got `{repo}`."
+    return 2
+  let owner := parts[0]!
+  let name := parts[1]!
+  initSearchPath (← findSysroot)
+  unsafe Lean.enableInitializersExecution
+  -- Import the content modules with `importAll` so the (private) `@[upstreamed]`
+  -- extension entries are loaded; collect `(declaration, pr)` tags, converting
+  -- names to strings inside the closure (environment data is freed on exit).
+  -- `withImportModules` loads with `loadExts := false`, which does not initialize
+  -- environment extensions; we need `importModules (loadExts := true)` so the
+  -- `@[upstreamed]` extension state is available. `importAll` loads the (private)
+  -- extension entries written during elaboration.
+  let contentMods ← contentModulesFromAggregator
+  let env ← unsafe importModules (contentMods.map ({module := ·, importAll := true})) {}
+    (trustLevel := 1024) (loadExts := true)
+  let mut tags : Array (String × Nat) := #[]
+  for (mod, idx) in env.header.moduleNames.zipIdx do
+    if isContentModule mod then
+      for n in env.header.moduleData[idx]!.constNames do
+        if let some pr := MathlibStaging.getUpstreamedPR? env n then
+          tags := tags.push (n.toString, pr)
+  if tags.isEmpty then
+    IO.println "No `@[upstreamed]` declarations found."
+    return 0
+  let prs := (tags.map (·.2)).toList.eraseDups.toArray
+  let out ← IO.Process.output { cmd := "gh", args := #["api", "graphql", "-f", s!"query={mergeQuery owner name prs}"] }
+  unless out.exitCode == 0 do
+    IO.eprintln s!"`gh api graphql` failed (is `gh` installed and authenticated?):\n{out.stderr}"
+    return 2
+  let merged ← match parseMerged out.stdout prs with
+    | .ok m => pure m
+    | .error e => IO.eprintln s!"Could not parse the GitHub response: {e}"; return 2
+  let mut anyMerged := false
+  for pr in prs.qsort (· < ·) do
+    let decls := (tags.filterMap fun (d, q) => if q == pr then some d else none).qsort (· < ·)
+    if (merged.find? (·.1 == pr)).any (·.2) then
+      anyMerged := true
+      IO.println s!"✓ {repo}#{pr} is merged — {decls.size} declaration(s) can be removed from staging:"
+      for d in decls do IO.println s!"    {d}"
+    else
+      IO.println s!"· {repo}#{pr} is still open — {decls.size} declaration(s)."
+  -- Non-zero exit when cleanup is pending, so CI can flag it.
+  return if anyMerged then 1 else 0
+
 /-- `lake exe upstream report` -/
 def reportCmd : Cmd := `[Cli|
   report VIA runReport; ["0.1.0"]
@@ -245,13 +333,26 @@ def reportCmd : Cmd := `[Cli|
     json;              "Emit JSON instead of an aligned table."
 ]
 
+/-- `lake exe upstream check` -/
+def checkCmd : Cmd := `[Cli|
+  check VIA runCheck; ["0.1.0"]
+  "Report which `@[upstreamed N]` declarations are in already-merged mathlib pull \
+   requests, and so can now be removed from the staging library. Requires the \
+   GitHub CLI `gh` to be installed and authenticated."
+
+  FLAGS:
+    "repo" : String; "The GitHub repository to query, as `owner/name` \
+                      (default: `leanprover-community/mathlib4`)."
+]
+
 /-- The `upstream` command, dispatching to its subcommands. -/
 def upstreamCmd : Cmd := `[Cli|
   upstream NOOP; ["0.1.0"]
   "Tooling for upstreaming MathlibStaging content to mathlib."
 
   SUBCOMMANDS:
-    reportCmd
+    reportCmd;
+    checkCmd
 ]
 
 end Upstream

From f040be9de7cb82d4a560fc11cb8e269d37a0cbee Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Sun, 28 Jun 2026 23:34:08 +0200
Subject: [PATCH 3/7] Add `upstream viz`: graph emission for the Verso
 blueprint (toolkit M3)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`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`.
---
 Upstream.lean | 154 ++++++++++++++++++++++++++++++++++++++++++--------
 1 file changed, 132 insertions(+), 22 deletions(-)

diff --git a/Upstream.lean b/Upstream.lean
index 10f7fa9..fa19878 100644
--- a/Upstream.lean
+++ b/Upstream.lean
@@ -116,19 +116,25 @@ def fileImportGraph (env : Environment) : NameMap (Array Name) := Id.run do
     g := g.insert mod (env.header.moduleData[idx]!.imports.map (·.module))
   return g
 
-/-- File-level rows: one per staging content module, over the module import graph
-restricted to staging content modules. -/
-def analyzeFiles (env : Environment) : Array Row := Id.run do
-  let graph : NameMap (Array Name) :=
-    (fileImportGraph env).filterMap fun n imps =>
-      if isContentModule n then some (imps.filter isContentModule) else none
+/-- Build reported rows from a node graph, attributing each node to a module. -/
+def rowsOf (graph : NameMap (Array Name)) (moduleOf : Name → Name) : Array Row := Id.run do
   let metrics := allMetrics graph
   let mut rows := #[]
   for (n, _) in graph do
-    let m := (metrics.find? n).getD { depth := 0, trans := {} }
-    rows := rows.push { name := n, module := n, depth := m.depth, deps := m.trans.size }
+    let m := (metrics.find? n).getD default
+    rows := rows.push { name := n, module := moduleOf n, depth := m.depth, deps := m.trans.size }
   return rows
 
+/-- The staging-internal file dependency graph: each staging content module mapped
+to its staging content imports. -/
+def stagingFileGraph (env : Environment) : NameMap (Array Name) :=
+  (fileImportGraph env).filterMap fun n imps =>
+    if isContentModule n then some (imps.filter isContentModule) else none
+
+/-- File-level rows: one per staging content module. -/
+def analyzeFiles (env : Environment) : Array Row :=
+  rowsOf (stagingFileGraph env) id
+
 /-- Whether `n` is an auto-generated declaration (recursor, constructor,
 `noConfusion`, internal machinery, …) rather than a source-written one, and so
 should not be reported as an upstreaming unit in its own right. -/
@@ -138,9 +144,11 @@ def isGenerated (env : Environment) (n : Name) : Bool :=
     | some (.recInfo _) | some (.ctorInfo _) => true
     | _ => false
 
-/-- Declaration-level rows: one per source-written declaration in a staging
-content module, over the declaration-use graph restricted to such declarations. -/
-def analyzeDecls (env : Environment) : CoreM (Array Row) := do
+/-- The staging-internal declaration dependency graph: each source-written
+declaration in a staging content module mapped to the staging declarations it
+uses. A structure/inductive's field-type dependencies live in its constructors,
+which are not nodes themselves, so they are folded into the type node. -/
+def stagingDeclGraph (env : Environment) : CoreM (NameMap (Array Name)) := do
   -- The source-written declarations living in staging content modules.
   let mut nodes : Array Name := #[]
   for (mod, idx) in env.header.moduleNames.zipIdx do
@@ -151,25 +159,20 @@ def analyzeDecls (env : Environment) : CoreM (Array Row) := do
         if !isGenerated env n && (← findDeclarationRanges? n).isSome then
           nodes := nodes.push n
   let nodeSet : NameSet := nodes.foldl (init := {}) fun acc n => acc.insert n
-  -- Edges: a declaration depends on the staging declarations it uses.
   let mut graph : NameMap (Array Name) := {}
   for n in nodes do
     let mut used := (← getConstInfo n).getUsedConstantsAsSet
-    -- A structure/inductive's real dependencies (its field types) live in its
-    -- constructors, which are not reported separately; fold them into the type node.
     if let some (.inductInfo val) := env.find? n then
       for ctor in val.ctors do
         used := nsUnion used (← getConstInfo ctor).getUsedConstantsAsSet
     let deps := used.foldl (init := #[]) fun acc e =>
       if e != n && nodeSet.contains e then acc.push e else acc
     graph := graph.insert n deps
-  let metrics := allMetrics graph
-  let mut rows := #[]
-  for n in nodes do
-    let m := (metrics.find? n).getD { depth := 0, trans := {} }
-    rows := rows.push
-      { name := n, module := (env.getModuleFor? n).getD .anonymous, depth := m.depth, deps := m.trans.size }
-  return rows
+  return graph
+
+/-- Declaration-level rows: one per source-written staging declaration. -/
+def analyzeDecls (env : Environment) : CoreM (Array Row) :=
+  return rowsOf (← stagingDeclGraph env) (fun n => (env.getModuleFor? n).getD .anonymous)
 
 /-- Render an aligned text table. -/
 def renderTable (headers : Array String) (rows : Array (Array String)) : String := Id.run do
@@ -320,6 +323,99 @@ def runCheck (p : Parsed) : IO UInt32 := do
   -- Non-zero exit when cleanup is pending, so CI can flag it.
   return if anyMerged then 1 else 0
 
+/-! ## `lake exe upstream viz`
+
+Emits the staging dependency graph for visualisation, either as a versioned JSON
+record (modelled on verso-blueprint's `GraphData`, to be rendered by the Verso
+blueprint site) or as Graphviz DOT. Nodes carry an upstreaming `status` and the
+matching presentation colours, separated as in `GraphData` (semantics vs visual).
+-/
+
+/-- The upstreaming status of a node: `upstreamable` (no staging dependencies,
+ready to upstream now), `pending` (already in an open mathlib PR via
+`@[upstreamed]`), or `blocked` (depends on staging declarations that must be
+upstreamed first). -/
+def statusOf (depth : Nat) (pr : Option Nat) : String :=
+  if pr.isSome then "pending" else if depth == 0 then "upstreamable" else "blocked"
+
+/-- The `(fill, border)` colours for a status. -/
+def statusColors : String → String × String
+  | "upstreamable" => ("#dbeafe", "#2563eb")  -- blue: ready to upstream
+  | "pending"      => ("#ede9fe", "#7c3aed")  -- violet: in an open PR
+  | "blocked"      => ("#fef3c7", "#f59e0b")  -- amber: blocked by staging deps
+  | _              => ("#ffffff", "#334155")
+
+/-- The graph as a versioned JSON record (nodes with status + visual colours,
+edges, and module groups), for the Verso blueprint renderer. -/
+def vizJson (kind : String) (graph : NameMap (Array Name)) (moduleOf : Name → Name)
+    (prOf : Name → Option Nat) : Json := Id.run do
+  let metrics := allMetrics graph
+  let mut nodeObjs := #[]
+  let mut edgeObjs := #[]
+  let mut modules : Array String := #[]
+  let mut nodeMods : Array (String × String) := #[]
+  for (n, deps) in graph do
+    let m := (metrics.find? n).getD default
+    let pr := prOf n
+    let st := statusOf m.depth pr
+    let (fill, border) := statusColors st
+    let modName := (moduleOf n).toString
+    unless modules.contains modName do modules := modules.push modName
+    nodeMods := nodeMods.push (n.toString, modName)
+    nodeObjs := nodeObjs.push <| Json.mkObj
+      [("id", Json.str n.toString), ("label", Json.str n.toString), ("group", Json.str modName),
+       ("depth", toJson m.depth), ("transitiveDeps", toJson m.trans.size), ("status", Json.str st),
+       ("upstreamedPR", (pr.map (toJson ·)).getD Json.null),
+       ("visual", Json.mkObj [("fill", Json.str fill), ("border", Json.str border)])]
+    for d in deps do
+      edgeObjs := edgeObjs.push <|
+        Json.mkObj [("source", Json.str n.toString), ("target", Json.str d.toString)]
+  let groupObjs := modules.map fun modName =>
+    let ids := nodeMods.filterMap fun (id, m) => if m == modName then some (Json.str id) else none
+    Json.mkObj [("id", Json.str modName), ("label", Json.str modName), ("nodes", Json.arr ids)]
+  return Json.mkObj
+    [("schemaVersion", toJson (1 : Nat)), ("kind", Json.str kind),
+     ("nodes", Json.arr nodeObjs), ("edges", Json.arr edgeObjs), ("groups", Json.arr groupObjs)]
+
+/-- The graph as a Graphviz DOT string, nodes coloured by upstreaming status. -/
+def vizDot (graph : NameMap (Array Name)) (prOf : Name → Option Nat) : String := Id.run do
+  let metrics := allMetrics graph
+  let mut lines := #["digraph upstream {", "  rankdir=LR;", "  node [style=filled, shape=box];"]
+  for (n, deps) in graph do
+    let m := (metrics.find? n).getD default
+    let (fill, border) := statusColors (statusOf m.depth (prOf n))
+    lines := lines.push s!"  \"{n}\" [fillcolor=\"{fill}\", color=\"{border}\"];"
+    for d in deps do
+      lines := lines.push s!"  \"{n}\" -> \"{d}\";"
+  lines := lines.push "}"
+  return String.intercalate "\n" lines.toList
+
+/-- Implementation of `lake exe upstream viz`. -/
+def runViz (p : Parsed) : IO UInt32 := do
+  let decls := p.hasFlag "decls"
+  let fmt := (p.flag? "format").map (·.as! String) |>.getD "json"
+  let out? := (p.flag? "out").map (·.as! String)
+  initSearchPath (← findSysroot)
+  unsafe Lean.enableInitializersExecution
+  -- Load with `loadExts` + `importAll` so the `@[upstreamed]` tags are available.
+  let contentMods ← contentModulesFromAggregator
+  let env ← unsafe importModules (contentMods.map ({module := ·, importAll := true})) {}
+    (trustLevel := 1024) (loadExts := true)
+  let prOf := fun n => MathlibStaging.getUpstreamedPR? env n
+  let output ← if decls then 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 (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 (vizJson "files" graph id (fun _ => none)).pretty
+  match out? with
+  | some f => IO.FS.writeFile f output; IO.println s!"wrote {f}"
+  | none => IO.println output
+  return 0
+
 /-- `lake exe upstream report` -/
 def reportCmd : Cmd := `[Cli|
   report VIA runReport; ["0.1.0"]
@@ -345,6 +441,19 @@ def checkCmd : Cmd := `[Cli|
                       (default: `leanprover-community/mathlib4`)."
 ]
 
+/-- `lake exe upstream viz` -/
+def vizCmd : Cmd := `[Cli|
+  viz VIA runViz; ["0.1.0"]
+  "Emit the staging dependency graph for visualisation: a versioned JSON record \
+   (modelled on verso-blueprint's `GraphData`, for the Verso blueprint site) or \
+   Graphviz DOT. Nodes are coloured by upstreaming status."
+
+  FLAGS:
+    decls;             "Graph individual declarations instead of whole files."
+    "format" : String; "Output format, `json` (default) or `dot`."
+    "out" : String;    "Write to this file instead of stdout."
+]
+
 /-- The `upstream` command, dispatching to its subcommands. -/
 def upstreamCmd : Cmd := `[Cli|
   upstream NOOP; ["0.1.0"]
@@ -352,7 +461,8 @@ def upstreamCmd : Cmd := `[Cli|
 
   SUBCOMMANDS:
     reportCmd;
-    checkCmd
+    checkCmd;
+    vizCmd
 ]
 
 end Upstream

From 671de820b955c3ae1f9f202f4dfa7c85c59a3112 Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Mon, 29 Jun 2026 00:07:57 +0200
Subject: [PATCH 4/7] Add the Verso upstreaming dashboard with graph
 visualisation (toolkit M4/M5)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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`.
---
 .github/workflows/verso-blueprint.yml         |  89 ++++++++++++
 .gitignore                                    |   2 +
 Upstream.lean                                 |  50 ++++++-
 blueprint-verso/UpstreamingBlueprint.lean     |   1 +
 .../UpstreamingBlueprint/Blueprint.lean       |  22 +++
 .../UpstreamingBlueprint/Chapters/Graph.lean  | 130 ++++++++++++++++++
 blueprint-verso/UpstreamingBlueprintMain.lean |  12 ++
 blueprint-verso/lake-manifest.json            |  86 ++++++++++++
 blueprint-verso/lakefile.toml                 |  27 ++++
 blueprint-verso/lean-toolchain                |   1 +
 blueprint-verso/scripts/ci-pages.sh           |  15 ++
 11 files changed, 434 insertions(+), 1 deletion(-)
 create mode 100644 .github/workflows/verso-blueprint.yml
 create mode 100644 blueprint-verso/UpstreamingBlueprint.lean
 create mode 100644 blueprint-verso/UpstreamingBlueprint/Blueprint.lean
 create mode 100644 blueprint-verso/UpstreamingBlueprint/Chapters/Graph.lean
 create mode 100644 blueprint-verso/UpstreamingBlueprintMain.lean
 create mode 100644 blueprint-verso/lake-manifest.json
 create mode 100644 blueprint-verso/lakefile.toml
 create mode 100644 blueprint-verso/lean-toolchain
 create mode 100755 blueprint-verso/scripts/ci-pages.sh

diff --git a/.github/workflows/verso-blueprint.yml b/.github/workflows/verso-blueprint.yml
new file mode 100644
index 0000000..bff7d00
--- /dev/null
+++ b/.github/workflows/verso-blueprint.yml
@@ -0,0 +1,89 @@
+name: Verso upstreaming dashboard
+
+on:
+  push:
+    branches: [master]
+  pull_request:
+    paths:
+      - "MathlibStaging/**"
+      - "Upstream.lean"
+      - "blueprint-verso/**"
+      - ".github/workflows/verso-blueprint.yml"
+  workflow_dispatch:
+
+permissions:
+  contents: write
+
+concurrency:
+  group: ${{ github.repository }}-verso-blueprint-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v5
+
+      - 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"
+
+      # --- Generate the graph chapter from the main library (Lean v4.32.0-rc1). ---
+      - name: Cache main-repo Lake packages
+        uses: actions/cache@v4
+        with:
+          path: .lake/packages
+          key: ${{ runner.os }}-lake-main-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}
+
+      - 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 blueprint-verso/UpstreamingBlueprint/Chapters/Graph.lean
+
+      # --- Build the Verso site (Lean v4.31.0). ---
+      - name: Cache blueprint Lake packages
+        uses: actions/cache@v4
+        with:
+          path: blueprint-verso/.lake/packages
+          key: ${{ runner.os }}-lake-blueprint-${{ hashFiles('blueprint-verso/lean-toolchain', 'blueprint-verso/lake-manifest.json') }}
+
+      - name: Cache blueprint build
+        uses: actions/cache@v4
+        with:
+          path: blueprint-verso/.lake/build
+          key: ${{ runner.os }}-build-blueprint-${{ hashFiles('blueprint-verso/lean-toolchain', 'blueprint-verso/lake-manifest.json', 'blueprint-verso/**/*.lean') }}
+
+      - name: Build blueprint site
+        run: ./blueprint-verso/scripts/ci-pages.sh
+
+      - name: Upload site artifact
+        uses: actions/upload-artifact@v4
+        with:
+          name: verso-dashboard
+          path: blueprint-verso/_out/site/html-multi
+
+  deploy:
+    if: github.event_name != 'pull_request'
+    needs: build
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/download-artifact@v4
+        with:
+          name: verso-dashboard
+          path: site
+      # Publish to the `gh-pages` branch under `dashboard/`, so it coexists with
+      # any other GitHub Pages content (e.g. the API docs) on the same site.
+      - name: Deploy to GitHub Pages
+        uses: JamesIves/github-pages-deploy-action@v4
+        with:
+          branch: gh-pages
+          folder: site
+          target-folder: dashboard
+          clean: true
+          clean-exclude: |
+            !dashboard/**
diff --git a/.gitignore b/.gitignore
index bfb30ec..268d777 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,3 @@
 /.lake
+/blueprint-verso/.lake
+/blueprint-verso/_out
diff --git a/Upstream.lean b/Upstream.lean
index fa19878..4b12bd6 100644
--- 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/blueprint-verso/UpstreamingBlueprint.lean b/blueprint-verso/UpstreamingBlueprint.lean
new file mode 100644
index 0000000..e554275
--- /dev/null
+++ b/blueprint-verso/UpstreamingBlueprint.lean
@@ -0,0 +1 @@
+import UpstreamingBlueprint.Blueprint
diff --git a/blueprint-verso/UpstreamingBlueprint/Blueprint.lean b/blueprint-verso/UpstreamingBlueprint/Blueprint.lean
new file mode 100644
index 0000000..03cb707
--- /dev/null
+++ b/blueprint-verso/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/blueprint-verso/UpstreamingBlueprint/Chapters/Graph.lean b/blueprint-verso/UpstreamingBlueprint/Chapters/Graph.lean
new file mode 100644
index 0000000..e559780
--- /dev/null
+++ b/blueprint-verso/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/blueprint-verso/UpstreamingBlueprintMain.lean b/blueprint-verso/UpstreamingBlueprintMain.lean
new file mode 100644
index 0000000..8b8fca1
--- /dev/null
+++ b/blueprint-verso/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%)
diff --git a/blueprint-verso/lake-manifest.json b/blueprint-verso/lake-manifest.json
new file mode 100644
index 0000000..7afa89e
--- /dev/null
+++ b/blueprint-verso/lake-manifest.json
@@ -0,0 +1,86 @@
+{"version": "1.2.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover/verso-blueprint",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "e203d9df24004d71bbff25521f8a9b7540bd9aca",
+   "name": "VersoBlueprint",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.31.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "2db6054a44326f8c0230ee0570e2ddb894816511",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.98",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/verso-slides.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "f3a071c24d67e5ca812cdb929a77e0aefd627bf5",
+   "name": "«verso-slides»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.31.0",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/verso",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "b677415e8a0becccc0b850137c2d8f6205132a91",
+   "name": "verso",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.31.0",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/illuminate",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "20b8493528eed2fac9827ce18d41c475f0e1c50a",
+   "name": "illuminate",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/acmepjz/md4lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5",
+   "name": "MD4Lean",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/subverso",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "0bd508e8362f56d4a05cbf63614d4c97db954041",
+   "name": "subverso",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"}],
+ "name": "UpstreamingBlueprint",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/blueprint-verso/lakefile.toml b/blueprint-verso/lakefile.toml
new file mode 100644
index 0000000..8787697
--- /dev/null
+++ b/blueprint-verso/lakefile.toml
@@ -0,0 +1,27 @@
+name = "UpstreamingBlueprint"
+defaultTargets = ["UpstreamingBlueprint"]
+
+# This is a self-contained Lake package, separate from the top-level
+# `mathlib-staging` library, with its own `lean-toolchain`. It renders the
+# upstreaming dependency graph as a Verso blueprint site.
+#
+# It deliberately does NOT depend on the `MathlibStaging` library: verso-blueprint
+# is pinned to Lean v4.31.0 while the main library tracks mathlib master
+# (v4.32.0-rc1), so a `path = ".."` dependency would force a toolchain clash.
+# Instead the graph data is produced by `lake exe upstream viz` in the main repo
+# and consumed here as JSON.
+
+[leanOptions]
+experimental.module = true
+
+[[require]]
+name = "VersoBlueprint"
+git = "https://github.com/leanprover/verso-blueprint"
+rev = "v4.31.0"
+
+[[lean_lib]]
+name = "UpstreamingBlueprint"
+
+[[lean_exe]]
+name = "blueprint-gen"
+root = "UpstreamingBlueprintMain"
diff --git a/blueprint-verso/lean-toolchain b/blueprint-verso/lean-toolchain
new file mode 100644
index 0000000..18640c8
--- /dev/null
+++ b/blueprint-verso/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.31.0
diff --git a/blueprint-verso/scripts/ci-pages.sh b/blueprint-verso/scripts/ci-pages.sh
new file mode 100755
index 0000000..5d211af
--- /dev/null
+++ b/blueprint-verso/scripts/ci-pages.sh
@@ -0,0 +1,15 @@
+#!/usr/bin/env bash
+
+# Build the Verso upstreaming-dashboard site into `_out/site/html-multi`.
+# Assumes `UpstreamingBlueprint/Chapters/Graph.lean` has already been generated
+# by `lake exe upstream viz --decls --format verso` in the main repository.
+
+set -euo pipefail
+
+cd "$(dirname "$0")/.."
+
+lake build UpstreamingBlueprint
+lake env lean --run UpstreamingBlueprintMain.lean --output _out/site
+
+test -f _out/site/html-multi/index.html
+test -f _out/site/html-multi/-verso-data/blueprint-manifest.json

From 9db0285623831adc5b61b0fb29300ed3b74a584c Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Mon, 29 Jun 2026 09:40:41 +0200
Subject: [PATCH 5/7] =?UTF-8?q?Rename=20the=20dashboard=20sub-package=20di?=
 =?UTF-8?q?rectory=20blueprint-verso=20=E2=86=92=20dashboard?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Purely a rename of the Verso dashboard sub-package directory and its references
(`.gitignore`, the CI workflow paths, and the `upstream viz --out` target).
---
 .github/workflows/verso-blueprint.yml            | 16 ++++++++--------
 .gitignore                                       |  4 ++--
 .../UpstreamingBlueprint.lean                    |  0
 .../UpstreamingBlueprint/Blueprint.lean          |  0
 .../UpstreamingBlueprint/Chapters/Graph.lean     |  0
 .../UpstreamingBlueprintMain.lean                |  0
 .../lake-manifest.json                           |  0
 {blueprint-verso => dashboard}/lakefile.toml     |  0
 {blueprint-verso => dashboard}/lean-toolchain    |  0
 .../scripts/ci-pages.sh                          |  0
 10 files changed, 10 insertions(+), 10 deletions(-)
 rename {blueprint-verso => dashboard}/UpstreamingBlueprint.lean (100%)
 rename {blueprint-verso => dashboard}/UpstreamingBlueprint/Blueprint.lean (100%)
 rename {blueprint-verso => dashboard}/UpstreamingBlueprint/Chapters/Graph.lean (100%)
 rename {blueprint-verso => dashboard}/UpstreamingBlueprintMain.lean (100%)
 rename {blueprint-verso => dashboard}/lake-manifest.json (100%)
 rename {blueprint-verso => dashboard}/lakefile.toml (100%)
 rename {blueprint-verso => dashboard}/lean-toolchain (100%)
 rename {blueprint-verso => dashboard}/scripts/ci-pages.sh (100%)

diff --git a/.github/workflows/verso-blueprint.yml b/.github/workflows/verso-blueprint.yml
index bff7d00..8ccee92 100644
--- a/.github/workflows/verso-blueprint.yml
+++ b/.github/workflows/verso-blueprint.yml
@@ -7,7 +7,7 @@ on:
     paths:
       - "MathlibStaging/**"
       - "Upstream.lean"
-      - "blueprint-verso/**"
+      - "dashboard/**"
       - ".github/workflows/verso-blueprint.yml"
   workflow_dispatch:
 
@@ -43,29 +43,29 @@ jobs:
         run: |
           lake build MathlibStaging upstream
           lake exe upstream viz --decls --format verso \
-            --out blueprint-verso/UpstreamingBlueprint/Chapters/Graph.lean
+            --out dashboard/UpstreamingBlueprint/Chapters/Graph.lean
 
       # --- Build the Verso site (Lean v4.31.0). ---
       - name: Cache blueprint Lake packages
         uses: actions/cache@v4
         with:
-          path: blueprint-verso/.lake/packages
-          key: ${{ runner.os }}-lake-blueprint-${{ hashFiles('blueprint-verso/lean-toolchain', 'blueprint-verso/lake-manifest.json') }}
+          path: dashboard/.lake/packages
+          key: ${{ runner.os }}-lake-blueprint-${{ hashFiles('dashboard/lean-toolchain', 'dashboard/lake-manifest.json') }}
 
       - name: Cache blueprint build
         uses: actions/cache@v4
         with:
-          path: blueprint-verso/.lake/build
-          key: ${{ runner.os }}-build-blueprint-${{ hashFiles('blueprint-verso/lean-toolchain', 'blueprint-verso/lake-manifest.json', 'blueprint-verso/**/*.lean') }}
+          path: dashboard/.lake/build
+          key: ${{ runner.os }}-build-blueprint-${{ hashFiles('dashboard/lean-toolchain', 'dashboard/lake-manifest.json', 'dashboard/**/*.lean') }}
 
       - name: Build blueprint site
-        run: ./blueprint-verso/scripts/ci-pages.sh
+        run: ./dashboard/scripts/ci-pages.sh
 
       - name: Upload site artifact
         uses: actions/upload-artifact@v4
         with:
           name: verso-dashboard
-          path: blueprint-verso/_out/site/html-multi
+          path: dashboard/_out/site/html-multi
 
   deploy:
     if: github.event_name != 'pull_request'
diff --git a/.gitignore b/.gitignore
index 268d777..9bda828 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,3 @@
 /.lake
-/blueprint-verso/.lake
-/blueprint-verso/_out
+/dashboard/.lake
+/dashboard/_out
diff --git a/blueprint-verso/UpstreamingBlueprint.lean b/dashboard/UpstreamingBlueprint.lean
similarity index 100%
rename from blueprint-verso/UpstreamingBlueprint.lean
rename to dashboard/UpstreamingBlueprint.lean
diff --git a/blueprint-verso/UpstreamingBlueprint/Blueprint.lean b/dashboard/UpstreamingBlueprint/Blueprint.lean
similarity index 100%
rename from blueprint-verso/UpstreamingBlueprint/Blueprint.lean
rename to dashboard/UpstreamingBlueprint/Blueprint.lean
diff --git a/blueprint-verso/UpstreamingBlueprint/Chapters/Graph.lean b/dashboard/UpstreamingBlueprint/Chapters/Graph.lean
similarity index 100%
rename from blueprint-verso/UpstreamingBlueprint/Chapters/Graph.lean
rename to dashboard/UpstreamingBlueprint/Chapters/Graph.lean
diff --git a/blueprint-verso/UpstreamingBlueprintMain.lean b/dashboard/UpstreamingBlueprintMain.lean
similarity index 100%
rename from blueprint-verso/UpstreamingBlueprintMain.lean
rename to dashboard/UpstreamingBlueprintMain.lean
diff --git a/blueprint-verso/lake-manifest.json b/dashboard/lake-manifest.json
similarity index 100%
rename from blueprint-verso/lake-manifest.json
rename to dashboard/lake-manifest.json
diff --git a/blueprint-verso/lakefile.toml b/dashboard/lakefile.toml
similarity index 100%
rename from blueprint-verso/lakefile.toml
rename to dashboard/lakefile.toml
diff --git a/blueprint-verso/lean-toolchain b/dashboard/lean-toolchain
similarity index 100%
rename from blueprint-verso/lean-toolchain
rename to dashboard/lean-toolchain
diff --git a/blueprint-verso/scripts/ci-pages.sh b/dashboard/scripts/ci-pages.sh
similarity index 100%
rename from blueprint-verso/scripts/ci-pages.sh
rename to dashboard/scripts/ci-pages.sh

From 60c4031cde6528986ef0dad3e6ff2f2a082794dc Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Mon, 29 Jun 2026 09:48:08 +0200
Subject: [PATCH 6/7] =?UTF-8?q?Rename=20the=20dashboard=20workflow=20file?=
 =?UTF-8?q?=20verso-blueprint.yml=20=E2=86=92=20dashboard.yml?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .github/workflows/{verso-blueprint.yml => dashboard.yml} | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)
 rename .github/workflows/{verso-blueprint.yml => dashboard.yml} (98%)

diff --git a/.github/workflows/verso-blueprint.yml b/.github/workflows/dashboard.yml
similarity index 98%
rename from .github/workflows/verso-blueprint.yml
rename to .github/workflows/dashboard.yml
index 8ccee92..587e919 100644
--- a/.github/workflows/verso-blueprint.yml
+++ b/.github/workflows/dashboard.yml
@@ -8,7 +8,7 @@ on:
       - "MathlibStaging/**"
       - "Upstream.lean"
       - "dashboard/**"
-      - ".github/workflows/verso-blueprint.yml"
+      - ".github/workflows/dashboard.yml"
   workflow_dispatch:
 
 permissions:

From 961cd940f5d42ff3fd196f73f2a901838d96fdf6 Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Mon, 29 Jun 2026 10:07:01 +0200
Subject: [PATCH 7/7] Publish docs and the dashboard together via one GitHub
 Pages workflow

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).
---
 .github/workflows/dashboard.yml      | 89 ----------------------------
 .github/workflows/lean_action_ci.yml |  7 +--
 .github/workflows/pages.yml          | 85 ++++++++++++++++++++++++++
 3 files changed, 88 insertions(+), 93 deletions(-)
 delete mode 100644 .github/workflows/dashboard.yml
 create mode 100644 .github/workflows/pages.yml

diff --git a/.github/workflows/dashboard.yml b/.github/workflows/dashboard.yml
deleted file mode 100644
index 587e919..0000000
--- a/.github/workflows/dashboard.yml
+++ /dev/null
@@ -1,89 +0,0 @@
-name: Verso upstreaming dashboard
-
-on:
-  push:
-    branches: [master]
-  pull_request:
-    paths:
-      - "MathlibStaging/**"
-      - "Upstream.lean"
-      - "dashboard/**"
-      - ".github/workflows/dashboard.yml"
-  workflow_dispatch:
-
-permissions:
-  contents: write
-
-concurrency:
-  group: ${{ github.repository }}-verso-blueprint-${{ github.ref }}
-  cancel-in-progress: true
-
-jobs:
-  build:
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v5
-
-      - 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"
-
-      # --- Generate the graph chapter from the main library (Lean v4.32.0-rc1). ---
-      - name: Cache main-repo Lake packages
-        uses: actions/cache@v4
-        with:
-          path: .lake/packages
-          key: ${{ runner.os }}-lake-main-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}
-
-      - 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
-
-      # --- Build the Verso site (Lean v4.31.0). ---
-      - name: Cache blueprint Lake packages
-        uses: actions/cache@v4
-        with:
-          path: dashboard/.lake/packages
-          key: ${{ runner.os }}-lake-blueprint-${{ hashFiles('dashboard/lean-toolchain', 'dashboard/lake-manifest.json') }}
-
-      - name: Cache blueprint build
-        uses: actions/cache@v4
-        with:
-          path: dashboard/.lake/build
-          key: ${{ runner.os }}-build-blueprint-${{ hashFiles('dashboard/lean-toolchain', 'dashboard/lake-manifest.json', 'dashboard/**/*.lean') }}
-
-      - name: Build blueprint site
-        run: ./dashboard/scripts/ci-pages.sh
-
-      - name: Upload site artifact
-        uses: actions/upload-artifact@v4
-        with:
-          name: verso-dashboard
-          path: dashboard/_out/site/html-multi
-
-  deploy:
-    if: github.event_name != 'pull_request'
-    needs: build
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/download-artifact@v4
-        with:
-          name: verso-dashboard
-          path: site
-      # Publish to the `gh-pages` branch under `dashboard/`, so it coexists with
-      # any other GitHub Pages content (e.g. the API docs) on the same site.
-      - name: Deploy to GitHub Pages
-        uses: JamesIves/github-pages-deploy-action@v4
-        with:
-          branch: gh-pages
-          folder: site
-          target-folder: dashboard
-          clean: true
-          clean-exclude: |
-            !dashboard/**
diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
index a8944df..131c045 100644
--- 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
new file mode 100644
index 0000000..a187aa8
--- /dev/null
+++ 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