Keep the library's API docs pages when the docs cache replays

.github/workflows/blueprint.yml

@@ -113,9 +113,12 @@ jobs:
       # the assembly step instead of being copied into a Jekyll folder.
       #
       # This step: the package name, the docs facets (each default target with `:docs`) and the
-      # paths to cache, in docgen-action's order, so that a cache it saved under the same key is
-      # restored. A manifest package maps to its module names through docgen-action's table, else
-      # through the UpperCamelCase rule of `lake new`.
+      # paths to cache. A manifest package maps to its module names through docgen-action's table,
+      # else through the UpperCamelCase rule of `lake new`.
+      #
+      # The cached `doc-data` holds Lake's record of the docs built for this project too, so the
+      # project's own pages are cached with it. Without them, a run whose Lean sources match the
+      # cache replays that record and regenerates no pages, and the project's pages are missing.
       - name: Determine the project metadata for the API docs
         id: docs-metadata
         run: |
@@ -143,6 +146,9 @@ jobs:
           deps = [m for p in manifest["packages"] for m in modules(p["name"])]
           deps += ["Init", "Lake", "Lean", "Std"]
           paths = [f"docbuild/.lake/build/doc/{d}" for d in deps]
+          for lib in lakefile["lean_lib"]:
+              paths.append(f"docbuild/.lake/build/doc/{lib['name']}")
+              paths.append(f"docbuild/.lake/build/doc/{lib['name']}.html")
           paths.append("docbuild/.lake/build/doc-data")
           paths.append("docbuild/.lake/build/doc/declarations/declaration-data.bmp")
           paths.append("docbuild/.lake/build/api-docs.db")
@@ -244,6 +250,18 @@ jobs:
           cp blueprint/print/print.pdf "$SITE"/blueprint.pdf
           cp -R docbuild/.lake/build/doc "$SITE"/docs
           cp -R web/redirects/. "$SITE"/
+          # Stop before deploying if the API docs lack a page of the library: the root module's
+          # page and the page of each module it imports.
+          modules=$(sed -n 's/^import \(Physicslib4\.[^ ]*\).*/\1/p' Physicslib4.lean)
+          test -n "$modules"
+          missing=0
+          for page in Physicslib4.html $(echo "$modules" | sed 's/\./\//g; s/$/.html/'); do
+            if [ ! -f "$SITE/docs/$page" ]; then
+              echo "::error::API docs page missing: docs/$page"
+              missing=$((missing + 1))
+            fi
+          done
+          test "$missing" -eq 0
           du -sh "$SITE" "$SITE"/*/
 
       # The API docs get the look of the rest of the site: the script rewrites the HTML under

web/README.md

@@ -307,13 +307,13 @@ placed at `/tmp/srv/physicslib4/docs` in the layout of "Build and view locally".
   4. builds the API docs with doc-gen4 the way `leanprover-community/docgen-action` does: a
      `docbuild/` Lake package requiring physicslib4 from `../` and doc-gen4 at the tag matching
      `lean-toolchain`, sharing `../.lake/packages`, built with `lake build Physicslib4:docs` into
-     `docbuild/.lake/build/doc`; the API docs of the dependencies are cached, keyed by
-     `lake-manifest.json`. Swap and memory overcommit are switched on first, for doc-gen4's many
+     `docbuild/.lake/build/doc`; the API docs are cached, keyed by `lake-manifest.json`. Swap and memory overcommit are switched on first, for doc-gen4's many
      `git` processes;
   5. step "Assemble the site": copies `web/_out/site/.` to `_site/`, `web/_out/tutorial/html-multi`
      to `_site/tutorial`, `web/_out/manual/html-multi` to `_site/manual`, `blueprint/web` to
      `_site/blueprint`, `blueprint/print/print.pdf` to `_site/blueprint.pdf` and the API docs to
-     `_site/docs`, then `web/redirects/.` over `_site/`;
+     `_site/docs`, then `web/redirects/.` over `_site/`, and stops
+     the run if the API docs lack the page of the library's root module or of a module it imports;
   6. step "Restyle the API docs": runs `python3 scripts/restyle_api_docs.py _site/docs` (see "The
      API docs"); it rewrites the copy in `_site/`, so the cached doc-gen4 output is not changed;
   7. uploads `_site/` with `actions/upload-pages-artifact`, which leaves out names starting with `.`.