name: Blueprint (Verso)

# Builds the Verso blueprint in blueprint-verso/ and deploys it to GitHub Pages.
# (Replaces the old leanblueprint LaTeX pipeline, which built the whole project.)
# The blueprint depends on LeanBridge for its `(lean := ...)` links, so Mathlib comes from its
# cache, Tau Ceti from Tau Ceti's public cache (`scripts/tauceti-cache.toml`), and the other
# packages and LeanBridge's own build outputs are kept in the Actions cache.

on:
  push:
    branches: [main]
    paths:
      - 'blueprint-verso/**'
      - 'LeanBridge/**'
      - 'LeanBridge.lean'
      - 'lakefile.toml'
      - 'lake-manifest.json'
      - 'lean-toolchain'
      - 'scripts/tauceti-cache.toml'
      - '.github/workflows/blueprint.yml'
  workflow_dispatch:

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

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

jobs:
  build:
    name: Build blueprint site
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v5
      - uses: actions/configure-pages@v5
      - 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"
      - name: Restore Lake packages and LeanBridge build outputs
        uses: actions/cache/restore@v4
        with:
          path: |
            blueprint-verso/.lake/packages
            !blueprint-verso/.lake/packages/mathlib
            .lake/build
          key: blueprint-lake-${{ hashFiles('blueprint-verso/lake-manifest.json', 'blueprint-verso/lean-toolchain') }}-${{ github.sha }}
          restore-keys: blueprint-lake-${{ hashFiles('blueprint-verso/lake-manifest.json', 'blueprint-verso/lean-toolchain') }}-
      - name: Fetch Mathlib's cache
        working-directory: blueprint-verso
        run: lake exe cache get
      # Only the mappings: the build then fetches the Tau Ceti modules it needs. If the cache is
      # unreachable, the build falls back to building Tau Ceti from source.
      - name: Fetch Tau Ceti's cache mappings
        working-directory: blueprint-verso
        continue-on-error: true
        env:
          LAKE_CONFIG: ${{ github.workspace }}/scripts/tauceti-cache.toml
        run: >-
          lake cache get --service tauceti-public --repo TauCetiProject/TauCeti --package TauCeti
          --mappings-only
      - name: Build and render the blueprint
        working-directory: blueprint-verso
        env:
          LAKE_CONFIG: ${{ github.workspace }}/scripts/tauceti-cache.toml
        run: ./scripts/ci-pages.sh
      - name: Save Lake packages and LeanBridge build outputs
        if: ${{ !cancelled() }}
        uses: actions/cache/save@v4
        with:
          path: |
            blueprint-verso/.lake/packages
            !blueprint-verso/.lake/packages/mathlib
            .lake/build
          key: blueprint-lake-${{ hashFiles('blueprint-verso/lake-manifest.json', 'blueprint-verso/lean-toolchain') }}-${{ github.sha }}
      - uses: actions/upload-pages-artifact@v3
        with:
          path: blueprint-verso/_out/site/html-multi

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