deploy.yml

name: Build and deploy StatLean site

# Builds the doc-gen4 API docs and the interactive website from the source
# repository (StatLean/Stat-Lean) and deploys them to this repo's GitHub Pages,
# which is served at the root domain https://statlean.github.io/.
#
#   https://statlean.github.io/website/   interactive website
#   https://statlean.github.io/docs/      doc-gen4 API reference

on:
  # Manual trigger. By default this reuses the cached doc-gen4 output when the
  # Lean sources are unchanged, so a website-only change deploys in minutes;
  # set rebuild_docs to force the full Lean + doc-gen4 rebuild.
  workflow_dispatch:
    inputs:
      rebuild_docs:
        description: "Rebuild the Lean API docs even if the docs cache is valid"
        type: boolean
        default: false
  # Rebuild when the deploy workflow itself changes.
  push:
    branches: [main]
    paths:
      - '.github/workflows/deploy.yml'
  # Nightly rebuild to pick up changes pushed to StatLean/Stat-Lean.
  schedule:
    - cron: '0 6 * * *'

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

concurrency:
  group: pages
  cancel-in-progress: false

env:
  SOURCE_REPO: StatLean/Stat-Lean

jobs:
  build:
    runs-on: ubuntu-latest
    timeout-minutes: 360
    steps:
      - name: Checkout source repository (StatLean/Stat-Lean)
        uses: actions/checkout@v4
        with:
          repository: StatLean/Stat-Lean
          ref: main
          fetch-depth: 1
          path: src

      # Cache the final prepared docs (site/docs) keyed on Lean source hashes.
      # When Lean sources are unchanged, the heavy Lean+Mathlib build is skipped
      # and the docs are restored from cache; only the website is rebuilt.
      - name: Restore docs cache
        id: docs-cache
        uses: actions/cache@v4
        with:
          path: site/docs
          key: site-docs-${{ hashFiles('src/lean-toolchain', 'src/lakefile.lean', 'src/lake-manifest.json', 'src/StatLean.lean', 'src/StatLean/**/*.lean') }}
          restore-keys: site-docs-

      - name: Determine whether Lean docs need (re)building
        id: need
        run: |
          # Rebuild whenever the exact docs cache key missed (i.e. lean-toolchain,
          # lakefile.lean, or lake-manifest.json changed). A restore-keys hit only
          # brings back stale docs, so `site/docs` being non-empty is not enough.
          if [ "${{ steps.docs-cache.outputs.cache-hit }}" = "true" ]; then
            echo "build_lean=false" >> "$GITHUB_OUTPUT"
          else
            echo "build_lean=true" >> "$GITHUB_OUTPUT"
          fi

      # ── Lean steps: only when docs cache is empty or manually triggered ──
      - name: Install elan
        if: steps.need.outputs.build_lean == 'true' || inputs.rebuild_docs
        run: |
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"

      - name: Show Lean version
        if: steps.need.outputs.build_lean == 'true' || inputs.rebuild_docs
        working-directory: src
        run: lean --version

      - name: Update Lake dependencies (fetch doc-gen4)
        if: steps.need.outputs.build_lean == 'true' || inputs.rebuild_docs
        working-directory: src
        run: lake -Kenv=dev update

      - name: Fetch Mathlib cache
        if: steps.need.outputs.build_lean == 'true' || inputs.rebuild_docs
        working-directory: src
        run: lake exe cache get || true

      - name: Build project
        if: steps.need.outputs.build_lean == 'true' || inputs.rebuild_docs
        working-directory: src
        run: lake build

      - name: Build documentation
        if: steps.need.outputs.build_lean == 'true' || inputs.rebuild_docs
        working-directory: src
        run: lake -Kenv=dev build StatLean:docs

      - name: Generate dependency graphs
        if: steps.need.outputs.build_lean == 'true' || inputs.rebuild_docs
        working-directory: src
        run: lake exe deps || echo "deps extraction failed; site will fall back to doc-gen4 links"
      # ────────────────────────────────────────────────────────────────────

      - name: Set up Node
        uses: actions/setup-node@v4
        with:
          node-version: 20
          cache: npm
          cache-dependency-path: src/website/package-lock.json

      - name: Build the website
        working-directory: src/website
        run: |
          npm ci
          npm run build

      - name: Assemble GitHub Pages site
        run: |
          mkdir -p site/docs site/website
          # Overwrite cached docs with freshly built ones when Lean was rebuilt.
          if [ -d "src/.lake/build/doc" ] && [ "$(ls -A src/.lake/build/doc 2>/dev/null)" ]; then
            rm -rf site/docs && mkdir -p site/docs
            cp -r src/.lake/build/doc/* site/docs/
          fi
          cp -r src/website/dist/* site/website/
          # GitHub Pages: do not run Jekyll over the generated assets.
          touch site/.nojekyll
          # Root landing page redirects visitors to the interactive website.
          cat > site/index.html <<'EOF'
          <!doctype html>
          <html lang="en">
            <head>
              <meta charset="utf-8">
              <meta name="viewport" content="width=device-width, initial-scale=1">
              <title>Statistical Theory in Lean 4</title>
              <meta http-equiv="refresh" content="0; url=./website/">
              <link rel="canonical" href="./website/">
              <style>
                body { font-family: -apple-system, BlinkMacSystemFont, "Segoe UI", Roboto, Helvetica, Arial, sans-serif; max-width: 46rem; margin: 4rem auto; padding: 0 1.25rem; line-height: 1.6; color: #1b1b1b; }
                h1 { font-size: 1.9rem; margin-bottom: 0.25rem; }
                a { color: #b07414; }
                .btn { display: inline-block; margin-top: 1rem; margin-right: 0.5rem; padding: 0.6rem 1.1rem; background: #1b1b1b; color: #fff; border-radius: 999px; text-decoration: none; }
                .btn.alt { background: transparent; color: #1b1b1b; border: 1px solid #ccc; }
                .muted { color: #555; }
              </style>
            </head>
            <body>
              <h1>Statistical Theory in Lean 4</h1>
              <p class="muted">Redirecting to the Stat-Lean website&hellip;</p>
              <p>
                <a class="btn" href="./website/">Open the website &rarr;</a>
                <a class="btn alt" href="./docs/">API documentation</a>
              </p>
              <p class="muted">Source:
              <a href="https://github.com/StatLean/Stat-Lean">github.com/StatLean/Stat-Lean</a></p>
            </body>
          </html>
          EOF

      - name: Upload GitHub Pages artifact
        uses: actions/upload-pages-artifact@v3
        with:
          path: site

  deploy:
    environment:
      name: github-pages
      url: ${{ steps.deployment.outputs.page_url }}
    runs-on: ubuntu-latest
    needs: build
    steps:
      - name: Deploy to GitHub Pages
        id: deployment
        uses: actions/deploy-pages@v4