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' + + + mathlib-staging +

mathlib-staging

+ + 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 index bfb30ec..9bda828 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,3 @@ /.lake +/dashboard/.lake +/dashboard/_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 := "", 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 new file mode 100644 index 0000000..e554275 --- /dev/null +++ b/dashboard/UpstreamingBlueprint.lean @@ -0,0 +1 @@ +import UpstreamingBlueprint.Blueprint diff --git a/dashboard/UpstreamingBlueprint/Blueprint.lean b/dashboard/UpstreamingBlueprint/Blueprint.lean new file mode 100644 index 0000000..03cb707 --- /dev/null +++ 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 new file mode 100644 index 0000000..e559780 --- /dev/null +++ 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 new file mode 100644 index 0000000..8b8fca1 --- /dev/null +++ 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%) diff --git a/dashboard/lake-manifest.json b/dashboard/lake-manifest.json new file mode 100644 index 0000000..7afa89e --- /dev/null +++ b/dashboard/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/dashboard/lakefile.toml b/dashboard/lakefile.toml new file mode 100644 index 0000000..8787697 --- /dev/null +++ b/dashboard/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/dashboard/lean-toolchain b/dashboard/lean-toolchain new file mode 100644 index 0000000..18640c8 --- /dev/null +++ b/dashboard/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.31.0 diff --git a/dashboard/scripts/ci-pages.sh b/dashboard/scripts/ci-pages.sh new file mode 100755 index 0000000..5d211af --- /dev/null +++ b/dashboard/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