pages.yml

name: Pages

# Renders HexManual to static HTML and publishes it to GitHub Pages.
#
# Push-to-main only (plus manual dispatch), deliberately omitting the
# `pull_request:` trigger the gating workflows use (SPEC/CI.md "Triggers").
# This is a publish step, not a check: a pull request cannot deploy, and
# rendering is a full Mathlib-backed build (~20 min), so running it on every
# PR commit would duplicate that cost for no added safety. Manual content
# errors -- broken cross-references, missing docstrings, non-compiling
# example blocks -- fail in `ci.yml`'s dedicated `lake build HexManual` PR
# gate. Use `workflow_dispatch` to render a branch on demand.
on:
  push:
    branches: [main]
  workflow_dispatch:

concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}
  # A render takes ~20 min. Let an in-flight publish finish and queue the
  # next push behind it, rather than cancelling it: cancelling on every
  # push left the published site several commits behind `main` on busy days.
  cancel-in-progress: false

permissions:
  contents: read
  pages: write
  id-token: write

jobs:
  publish:
    runs-on: ubuntu-latest
    environment:
      name: github-pages
      url: ${{ steps.deployment.outputs.page_url }}
    steps:
      - uses: actions/checkout@v4
        with:
          fetch-depth: 0
      - run: sudo apt-get install -y libgmp-dev libntl-dev pkg-config
      - name: Set up pinned Lean toolchain (no build)
        run: bash scripts/ci/setup_lean_toolchain.sh
      - name: Fetch Mathlib cache
        # The cache endpoint flakes occasionally; a failed fetch costs a
        # whole CI lap, so retry before giving up. The populated-cache
        # hard-fail check below still rejects a triple failure.
        run: |
          for attempt in 1 2 3; do
            lake exe cache get && break
            echo "lake exe cache get failed (attempt $attempt); retrying in 30s"
            sleep 30
          done
      - name: Verify Mathlib cache populated (hard fail on miss)
        run: bash scripts/ci/check_no_mathlib_rebuild.sh
      - name: Configure Lean shared library path
        run: |
          lean_prefix="$(lean --print-prefix)"
          test -d "$lean_prefix/lib/lean"
          echo "LD_LIBRARY_PATH=$lean_prefix/lib/lean:${LD_LIBRARY_PATH:-}" \
            >> "$GITHUB_ENV"
      - name: Restore .lake/build (Hex modules only)
        uses: actions/cache/restore@v4
        with:
          path: |
            .lake/build/lib/lean/Hex*
            .lake/build/ir/Hex*
          key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}-${{ github.sha }}
          restore-keys: |
            lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}-
      - name: Render the manual
        run: lake exe hexmanual --output _out
      - name: Upload Pages artifact
        uses: actions/upload-pages-artifact@v3
        with:
          path: _out/html-multi
      - name: Deploy to GitHub Pages
        id: deployment
        uses: actions/deploy-pages@v4