docs.yml

name: Documentation

on:
  merge_group:
    types: [checks_requested]
  pull_request:
    branches:
      - main

concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}
  cancel-in-progress: true

permissions:
  contents: read
  actions: read

jobs:
  scope:
    runs-on: ubuntu-latest
    outputs:
      applicable: ${{ steps.scope.outputs.applicable }}
    steps:
      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
        with:
          fetch-depth: 0
          persist-credentials: false
      - id: scope
        env:
          EVENT: ${{ github.event_name }}
          BASE: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }}
        run: |
          set -euo pipefail
          applicable=true
          if [ "$EVENT" = merge_group ] || [ "$EVENT" = pull_request ]; then
            applicable=false
            if [ "$EVENT" = pull_request ]; then
              files=$(git diff --name-only --no-renames "$BASE"...HEAD)
            else
              files=$(git diff --name-only --no-renames "$BASE"..HEAD)
            fi
            # Git may quote names containing Unicode or control characters.
            if grep -Eq '^"?(docbuild/|lean-toolchain$|lakefile\.toml$|lake-manifest\.json$|python/lean_pool/(exposition/|documentation\.py$|indexes\.py$|quality\.py$|validation_cache\.py$|ci_artifacts\.py$|ci_cache\.py$|rebase_fastpath\.py$)|python/(pyproject\.toml|uv\.lock)$|scripts/exposition/|\.github/workflows/docs[^/]*\.yml$)' <<< "$files"; then
              applicable=true
            fi
          fi
          echo "applicable=$applicable" >> "$GITHUB_OUTPUT"
  # Cheap configuration/index checks remain independent of daily publication.
  preflight:
    needs: scope
    if: always() && (needs.scope.result != 'success' || needs.scope.outputs.applicable != 'false')
    runs-on: ubuntu-latest
    name: Documentation preflight
    outputs:
      build_revision: ${{ steps.build-identity.outputs.revision }}
      readme_only: ${{ steps.scope.outputs.readme_only }}
      rebase_only: ${{ steps.rebase.outputs.rebase_only }}
    steps:
      - name: Require successful change classification
        env:
          SCOPE_RESULT: ${{ needs.scope.result }}
          APPLICABLE: ${{ needs.scope.outputs.applicable }}
        run: |
          if [ "$SCOPE_RESULT" != success ] || [ "$APPLICABLE" != true ]; then
            echo "::error::Change classification failed; required validation cannot be skipped."
            exit 1
          fi
      - name: Checkout project
        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
        with:
          fetch-depth: 0

      - name: Install Python tooling runtime
        uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
        with:
          enable-cache: true

      - name: Identify compiled Lean sources
        id: build-identity
        run: |
          set -euo pipefail
          revision=$(PYTHONPATH=python python3 -m lean_pool.ci_cache revision)
          echo "revision=$revision" >> "$GITHUB_OUTPUT"

      - name: Detect README-only change
        id: scope
        env:
          BASE_SHA: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }}
          EVENT_NAME: ${{ github.event_name }}
          HEAD_SHA: ${{ github.event.merge_group.head_sha || github.event.pull_request.head.sha }}
        run: |
          set -euo pipefail
          readme_only=false
          if [ "$EVENT_NAME" = "pull_request" ]; then
            files="$(git diff --name-only --no-renames "$BASE_SHA"..."$HEAD_SHA")"
            if [ "$files" = "README.md" ]; then
              readme_only=true
            fi
          fi
          echo "readme_only=$readme_only" >> "$GITHUB_OUTPUT"
          echo "README-only change: $readme_only"

      - name: Verify prior documentation preflight for a content-only rebase
        id: rebase
        if: github.event_name == 'pull_request' && steps.scope.outputs.readme_only != 'true'
        env:
          GH_TOKEN: ${{ github.token }}
          REPOSITORY: ${{ github.repository }}
          PR_NUMBER: ${{ github.event.pull_request.number }}
          HEAD_SHA: ${{ github.event.merge_group.head_sha || github.event.pull_request.head.sha }}
          BASE_SHA: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }}
        run: |
          decision=$(PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath decide \
            --workflow docs.yml --repository "$REPOSITORY" --number "$PR_NUMBER" \
            --head "$HEAD_SHA" --base "$BASE_SHA")
          echo "rebase_only=$(echo "$decision" | python3 -c 'import json,sys; print(str(json.load(sys.stdin)["eligible"]).lower())')" >> "$GITHUB_OUTPUT"
          echo "$decision"

      # docbuild deliberately reuses the root workspace's compiled artifacts.
      # Fail before restoring anything if those workspaces ever diverge.
      - name: Check documentation workspace compatibility
        if: steps.scope.outputs.readme_only != 'true'
        run: |
          set -euo pipefail
          if ! cmp lean-toolchain docbuild/lean-toolchain; then
            echo "::error::Root and documentation workspaces use different Lean toolchains."
            exit 1
          fi
          root_mathlib=$(jq -r '.packages[] | select(.name == "mathlib") | .rev' lake-manifest.json)
          docs_mathlib=$(jq -r '.packages[] | select(.name == "mathlib") | .rev' docbuild/lake-manifest.json)
          if [ -z "$root_mathlib" ] || [ "$root_mathlib" = "null" ]; then
            echo "::error::Root lake-manifest.json has no Mathlib revision."
            exit 1
          fi
          if [ -z "$docs_mathlib" ] || [ "$docs_mathlib" = "null" ]; then
            echo "::error::docbuild/lake-manifest.json has no Mathlib revision."
            exit 1
          fi
          if [ "$root_mathlib" != "$docs_mathlib" ]; then
            echo "::error::Root Mathlib revision $root_mathlib does not match docbuild ($docs_mathlib)."
            exit 1
          fi

      # Preflight needs the toolchain and dependencies, not the pool build.
      # Stable dependencies are shared with CI without a new copy per commit.
      - name: Restore Lean dependencies
        id: dependency-cache
        if: steps.scope.outputs.readme_only != 'true' && steps.rebase.outputs.rebase_only != 'true'
        uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
        with:
          path: |
            ~/.elan
            .lake/packages
          key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}

      - name: Install Lean
        if: steps.scope.outputs.readme_only != 'true' && steps.rebase.outputs.rebase_only != 'true'
        uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
        with:
          auto-config: false
          use-github-cache: false
          use-mathlib-cache: false

      # A package directory from a restored cache does not prove that its
      # oleans match the current manifest. `cache get` is incremental, so run it
      # unconditionally and then verify the checkout revision.
      - name: Install and verify Mathlib cache
        if: steps.scope.outputs.readme_only != 'true' && steps.rebase.outputs.rebase_only != 'true'
        run: |
          set -euo pipefail
          ~/.elan/bin/lake exe cache get
          expected=$(jq -r '.packages[] | select(.name == "mathlib") | .rev' lake-manifest.json)
          actual=$(git -C .lake/packages/mathlib rev-parse HEAD)
          if [ "$actual" != "$expected" ]; then
            echo "::error::Mathlib checkout $actual does not match lake-manifest.json ($expected)."
            exit 1
          fi

      - name: Check generated roots
        if: steps.scope.outputs.readme_only != 'true' && steps.rebase.outputs.rebase_only != 'true'
        run: ~/.elan/bin/lake exe mk_all --check

      - name: Check regenerated LeanPool root without Lean
        if: steps.rebase.outputs.rebase_only == 'true'
        run: PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath check-index