Fix the GitHub Pages deployment (docs + dashboard) (#11)

Fixes the GitHub Pages deployment added in #10, which failed on
`master`.

## Two bugs
1. **`lake: No such file or directory`** — `pages.yml` installed elan
*after* the docs step, but docgen-action's build script invokes
`~/.elan/bin/lake` directly. Install elan first.
2. **`409 Conflict` on the `github-pages` artifact** — docgen-action@v1
runs `upload-pages-artifact` on *every push* regardless of its `deploy`
input (only its `deploy-pages` step honours the flag). So the workflow's
own `upload-pages-artifact` was a second `github-pages` artifact and
collided.

## Fix
Since GitHub Pages allows only one deployment per repo and docgen-action
insists on uploading its `docs/` directory, let docgen own the single
upload + deploy instead of deploying separately. The workflow now:

1. builds the dashboard (chapter with Lean v4.32.0-rc1, Verso site with
v4.31.0),
2. drops it into docgen's output dir (`docs/dashboard`) and adds a
landing `docs/index.html`,
3. runs `docgen-action` (`build-page: false`), which builds the API docs
into `docs/docs` and uploads + deploys the whole `docs/` tree.

Resulting site: landing page at `/`, API docs at `/docs`, dashboard at
`/dashboard`.

(docgen's `build_docs.sh` only does `mkdir -p docs` + `cp … docs/docs`,
no `rm`, so the pre-placed dashboard survives.)

## Before merging
This branch is set up so the site can be deployed and tested from it.
Remove the temporary bits before/after merge:
- [ ] remove `fix-pages-deploy` from the `push:` trigger in `pages.yml`;
- [ ] remove the `fix-pages-deploy` branch from the `github-pages`
environment's deployment-branch policies.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Author: chrisflav

.github/workflows/pages.yml

@@ -1,9 +1,9 @@
 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.
+# Publishes the API documentation and the Verso upstreaming dashboard together to
+# GitHub Pages: a landing page at `/`, the API docs at `/docs`, and the dashboard
+# at `/dashboard`. GitHub Pages allows only one deployment per repository, so this
+# is the only workflow that deploys, uploading a single combined artifact.
 
 on:
   push:
@@ -26,36 +26,39 @@ jobs:
       - 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. ---
+      # elan provides the `lake` shim used by docgen-action's doc build and the
+      # dashboard build, so install it first.
       - 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"
 
+      # Build the API docs only. We pin docgen-action past its `v1` tag because
+      # only newer revisions honour `deploy: false` (`v1` uploads and deploys
+      # unconditionally); `build-page: false` skips its Jekyll homepage step. We
+      # assemble and deploy the combined site ourselves below.
+      - name: Build API documentation
+        uses: leanprover-community/docgen-action@10db47458f91456d87804787d3dfcd914b9a19e3
+        with:
+          deploy: false
+          build-page: false
+
+      # Build the dashboard: generate the chapter (Lean v4.32.0-rc1) and the Verso
+      # site (Lean v4.31.0). elan selects the toolchain per directory.
       - name: Get mathlib build cache
         run: lake exe cache get || true
-
-      - name: Generate the graph chapter
+      - name: Build dashboard site
         run: |
           lake build MathlibStaging upstream
           lake exe upstream viz --decls --format verso \
             --out dashboard/UpstreamingBlueprint/Chapters/Graph.lean
+          ./dashboard/scripts/ci-pages.sh
 
-      - name: Build dashboard site
-        run: ./dashboard/scripts/ci-pages.sh
-
-      # --- Assemble the combined site: docs at /docs, dashboard at /dashboard. ---
+      # Assemble the combined site: landing at /, 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).
+          # docgen-action leaves the built API docs under `docs/` (i.e. docs/docs).
           if [ -d docs ]; then cp -r docs/. _site/; fi
           mkdir -p _site/dashboard
           cp -r dashboard/_out/site/html-multi/. _site/dashboard/