diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml index 701919a..1d97ab7 100644 --- a/.github/workflows/blueprint.yml +++ b/.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 diff --git a/web/README.md b/web/README.md index d8881d2..36e071d 100644 --- a/web/README.md +++ b/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 `.`.