diff --git a/docs/deploy-runbook.md b/docs/deploy-runbook.md new file mode 100644 index 00000000..42c0ccc4 --- /dev/null +++ b/docs/deploy-runbook.md @@ -0,0 +1,123 @@ +# Deploy runbook — CLRS-Lean Verso site + +This document covers deploying the literate Verso site to +`https://tanktechnology.github.io/CLRS-Lean/`. + +## How deploys work + +- **Trigger**: `workflow_dispatch` only — no push-triggered deploys. +- **Workflow**: `.github/workflows/pages.yml` +- **Deploy environment**: `github-pages` (protected) +- **Concurrency**: `group: pages`, `cancel-in-progress: true` — only one deploy + pipeline runs at a time; a new trigger cancels any in-flight deploy. + +### Pipeline stages + +| Stage | What it does | +|---|---| +| `prepare` | Checkout → `check_repository.py` → `lean-action` (mathlib cache) → Verso patch → literate JSON cache → `lake build :literate` → 4-way shard plan → upload `literate-inputs` | +| `render` (×4) | Each shard downloads inputs, runs `render_literate_shard.py` on its chapter subset, uploads `literate-shard-N` | +| `merge` | Downloads all shards → `merge_literate_shards.py` → weight + freshness checks → `prepare_literate_site.py` → rendering check → upload Pages artifact | +| `deploy` | `actions/deploy-pages@v4` (only on `main` branch) | + +### Cache key + +``` +verso-literate-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.lean', 'literate.toml') }}-${{ github.sha }} +``` + +The key depends on four files: `lean-toolchain`, `lake-manifest.json`, +`lakefile.lean`, and `literate.toml`. **Do not touch `literate.toml`** unless +you are adding or removing a section from the site navigation — a change +invalidates the cache and forces a cold build. + +A secondary restore key drops the SHA suffix, so a warm build can reuse the +literate JSON from the most recent run with the same dependency files. + +## Timing + +| Scenario | Approximate wall-clock | +|---|---| +| Cold build (no literate JSON cache hit) | ~67 minutes | +| Warm build (cache hit, no dep changes) | ~15–20 minutes | +| Cache hit + no `.lean` changes | ~10 minutes | + +## Triggering a deploy + +### Via `gh` CLI + +```bash +gh workflow run pages.yml --repo TankTechnology/CLRS-Lean --ref main +``` + +### Via the GitHub API + +```bash +curl -X POST \ + -H "Authorization: Bearer $GITHUB_TOKEN" \ + -H "Accept: application/vnd.github+json" \ + "https://api.github.com/repos/TankTechnology/CLRS-Lean/actions/workflows/pages.yml/dispatches" \ + -d '{"ref":"main"}' +``` + +### Via the GitHub web UI + +Navigate to the Actions tab → "Build and deploy Verso site" → "Run workflow". + +## Watching a deploy + +```bash +# Get the latest run ID +gh run list --repo TankTechnology/CLRS-Lean --workflow=pages.yml --limit 1 --json databaseId + +# Watch until completion +gh run watch --repo TankTechnology/CLRS-Lean + +# Check the logs if something fails +gh run view --repo TankTechnology/CLRS-Lean --log +``` + +## Verifying the site after deploy + +```bash +# Check the site returns HTTP 200 +curl -s -o /dev/null -w "HTTP %{http_code}\n" https://tanktechnology.github.io/CLRS-Lean/ + +# Check the landing page content +curl -s https://tanktechnology.github.io/CLRS-Lean/ | head -5 +``` + +## Quota caution + +- **Workflow minutes are budgeted.** A cold build costs ~67 minutes. Only + trigger a deploy when the site needs to reflect new commits on `main`. +- The `lean-action` step pulls the mathlib cache on every run regardless of + warm/cold state — this is a fixed cost per run. +- Artifacts are retained for 1 day only. + +## Rollback + +A rollback means redeploying the last known-good SHA: + +```bash +# Trigger a deploy from a specific ref (must be a branch or tag) +# For a specific commit, create a temporary branch pointing at it first: +git checkout -b deploy-rollback +git push origin deploy-rollback +gh workflow run pages.yml --repo TankTechnology/CLRS-Lean --ref deploy-rollback +# Delete the branch after the deploy completes +git push origin --delete deploy-rollback +``` + +Alternatively, if the last known-good SHA is already on `main` (e.g., a revert +was merged), just trigger a normal deploy from `main`. + +## Troubleshooting + +| Symptom | Likely cause | Fix | +|---|---|---| +| `cache-hit` is `false` | `literate.toml`, `lean-toolchain`, `lake-manifest.json`, or `lakefile.lean` changed | Expected if those files were modified; wait for the cold build | +| `merge` fails on weight check | A shard produced fewer pages than expected | Check the `prepare` step's shard plan for anomalies | +| `merge` fails on freshness check | A stale artifact was used | Re-trigger — the concurrency group may have cancelled a previous run | +| `deploy` step doesn't run | The workflow was triggered from a non-`main` branch | Deploy only runs on `refs/heads/main` | +| Site returns 404 or old content | GitHub Pages CDN propagation delay | Wait 1–2 minutes and retry | \ No newline at end of file