refactor: switch to verso blueprint

.github/workflows/blueprint.yml

@@ -6,7 +6,7 @@ on:
     paths:
       - '**/*.lean'
       - '.github/workflows/blueprint.yml'
-      - 'blueprint/**'
+      - 'LeanOABlueprint/**'
       - 'home_page/**'
       - 'lean-toolchain'
       - 'lakefile.toml'
@@ -17,7 +17,7 @@ on:
     paths:
       - '**/*.lean'
       - '.github/workflows/blueprint.yml'
-      - 'blueprint/**'
+      - 'LeanOABlueprint/**'
       - 'home_page/**'
       - 'lean-toolchain'
       - 'lakefile.toml'
@@ -88,9 +88,39 @@ jobs:
           project-name: LeanOA
           branch-name: master
 
-      - name: Compile blueprint and documentation
+      # Needed only by `vbp build --pdf`; the HTML site has no LaTeX dependency.
+      - name: Install TeX Live for the blueprint PDF
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y --no-install-recommends \
+            python3-pygments \
+            texlive-luatex \
+            texlive-latex-extra \
+            texlive-fonts-recommended \
+            texlive-fonts-extra \
+            texlive-plain-generic
+
+      # `lake build LeanOABlueprint` is a separate step because the blueprint is not a default
+      # target (see lakefile.toml). It is also the check that replaces `checkdecls`: a statement
+      # whose `(lean := "...")` name does not resolve is a build error here.
+      - name: Build the Verso blueprint
+        run: |
+          lake build LeanOABlueprint
+          lake exe vbp build --pdf
+
+      # Hand the generated site to Jekyll at the same URLs the leanblueprint site used:
+      # `/blueprint/` for the web version and `/blueprint.pdf` for the print version.
+      - name: Stage the blueprint for GitHub Pages
+        run: |
+          test -f _out/site/html-multi/index.html
+          test -f _out/site/html-multi/-verso-data/blueprint-manifest.json
+          rm -rf home_page/blueprint
+          cp -r _out/site/html-multi home_page/blueprint
+          cp _out/site/pdf/main.pdf home_page/blueprint.pdf
+
+      - name: Compile documentation and home page
         uses: leanprover-community/docgen-action@main
         with:
-          blueprint: true
+          blueprint: false # the blueprint is built above by Verso, not by leanblueprint
           homepage: home_page
           ruby-version: default # read home_page/.ruby-version

.gitignore

@@ -1,9 +1,7 @@
 /build
 /lake-packages/*
 .lake/*
-blueprint/src/web.paux
-blueprint/print/
-blueprint/web/
 .venv/
-blueprint/lean_decls
-Ignore/
+Ignore/
+# Verso blueprint output (`lake exe vbp build`)
+_out/

LeanOA.lean

@@ -1,7 +1,6 @@
 module  -- shake: keep-all --deprecated_module: ignore
 
 public import LeanOA.AbsConvex
-public import LeanOA.BlueprintImports
 public import LeanOA.CFC
 public import LeanOA.CStarAlgebra.Extreme
 public import LeanOA.CStarAlgebra.FiniteSpectrum

LeanOABlueprint.lean

@@ -0,0 +1,8 @@
+import LeanOABlueprint.Base
+import LeanOABlueprint.Blueprint
+import LeanOABlueprint.Chapters.NormalityAndUltraweakContinuity
+import LeanOABlueprint.Chapters.OrderLemmas
+import LeanOABlueprint.Chapters.PositiveFunctionalsAndStates
+import LeanOABlueprint.Chapters.ProjectionLemmas
+import LeanOABlueprint.Chapters.StoneanSpacesAndMasas
+import LeanOABlueprint.Chapters.WStarAlgebrasAndTopologies

LeanOABlueprint/Base.lean

@@ -0,0 +1,40 @@
+import Verso
+import VersoManual
+import VersoBlueprint
+
+-- The formalization itself. Blueprint statements refer to its declarations through
+-- `(lean := "...")`, which resolves names in the environment of the chapter module, so the
+-- chapters need these imports to be in scope.
+import LeanOA
+
+-- Mathlib modules providing declarations that the blueprint cites but that LeanOA does not
+-- itself depend on.
+import Mathlib.Analysis.CStarAlgebra.Classes
+import Mathlib.Analysis.CStarAlgebra.GelfandDuality
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
+import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
+import Mathlib.Algebra.Order.Star.Basic
+import Mathlib.Analysis.CStarAlgebra.Projection
+import Mathlib.Geometry.Convex.Cone.Basic
+import Mathlib.Topology.Homeomorph.Lemmas
+
+open Informal
+
+/-
+TeX macros shared by every chapter.
+
+Blueprint math is rendered by KaTeX rather than by a full LaTeX engine, so the macro
+vocabulary of the old `blueprint/src/macros/common.tex` cannot be replayed verbatim.  The
+only project macros defined there were `\spectrum` and `\quasispectrum`, both of which took
+a LaTeX *optional* argument (`\newcommand{\spectrum}[2][]{...}`).  KaTeX's `\newcommand`
+has no optional-argument form, so they are re-expressed below as ordinary two-argument
+macros; write `\spectrum{}{a}` for an unadorned spectrum.
+
+`\providecommand` is used throughout so that a name KaTeX already ships wins over the local
+definition instead of raising a redefinition error.
+-/
+tex_prelude
+  r#"\providecommand{\spectrum}[2]{\sigma_{#1}(#2)}
+\providecommand{\quasispectrum}[2]{\sigma'_{#1}(#2)}"#

LeanOABlueprint/Blueprint.lean

@@ -0,0 +1,33 @@
+import LeanOABlueprint.Base
+import VersoBlueprint.Commands.Graph
+import VersoBlueprint.Commands.Summary
+import LeanOABlueprint.Chapters.WStarAlgebrasAndTopologies
+import LeanOABlueprint.Chapters.OrderLemmas
+import LeanOABlueprint.Chapters.ProjectionLemmas
+import LeanOABlueprint.Chapters.PositiveFunctionalsAndStates
+import LeanOABlueprint.Chapters.StoneanSpacesAndMasas
+import LeanOABlueprint.Chapters.NormalityAndUltraweakContinuity
+
+open Verso.Genre
+open Verso.Genre.Manual
+open Informal
+
+#doc (Manual) "WStarAlgebras have Unique Preduals" =>
+
+This is the blueprint of [LeanOA](https://github.com/j-loreaux/LeanOA), a formalization of
+operator algebra theory in Lean 4, built on top of
+[Mathlib](https://github.com/leanprover-community/mathlib4). Its target is the theorem that a
+$`W^*`-algebra has a unique predual, along with the $`C^*`/$`W^*`-algebra, locally convex,
+and ultraweak-topology infrastructure that goal needs.
+
+The numbering of the results below follows Sakai's *C\*-Algebras and W\*-Algebras*.
+
+{include 0 LeanOABlueprint.Chapters.WStarAlgebrasAndTopologies}
+{include 0 LeanOABlueprint.Chapters.OrderLemmas}
+{include 0 LeanOABlueprint.Chapters.ProjectionLemmas}
+{include 0 LeanOABlueprint.Chapters.PositiveFunctionalsAndStates}
+{include 0 LeanOABlueprint.Chapters.StoneanSpacesAndMasas}
+{include 0 LeanOABlueprint.Chapters.NormalityAndUltraweakContinuity}
+
+{blueprint_graph}
+{blueprint_summary}