blueprint.yml

name: Compile blueprint

on:
  push:
    branches: ["main"]
    paths:
      - ".github/workflows/blueprint.yml"
      - "blueprint/**"
      - "home_page/**"
      - "scripts/docs/**"
      - "scripts/checks/dependency_audit.py"
      - "lakefile.lean"
      - "lake-manifest.json"
      - "lean-toolchain"
      - "README.md"
  pull_request:
    branches: ["main"]
    paths:
      - ".github/workflows/blueprint.yml"
      - "blueprint/**"
      - "home_page/**"
      - "scripts/docs/**"
      - "scripts/checks/dependency_audit.py"
      - "lakefile.lean"
      - "lake-manifest.json"
      - "lean-toolchain"
      - "README.md"
  workflow_dispatch:

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

permissions:
  contents: read

env:
  FORCE_JAVASCRIPT_ACTIONS_TO_NODE24: true

jobs:
  build_project:
    runs-on: ubuntu-latest
    name: Build project
    steps:
      - name: Checkout project
        uses: actions/checkout@v4
        with:
          fetch-depth: 1

      - name: Free runner disk space
        run: |
          df -h
          sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc /opt/hostedtoolcache/CodeQL || true
          sudo apt-get clean
          rm -rf ~/.cache/mathlib
          df -h

      - name: Install elan
        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y

      - name: Get Mathlib cache
        run: |
          ~/.elan/bin/lake exe cache get || true
          rm -f ~/.cache/mathlib/*.ltar || true

      - name: Repo lint (TorchLean policies)
        run: ~/.elan/bin/lake lint

      - name: Build curated library surface
        run: ~/.elan/bin/lake build NN.Library

      - name: Cache API docs
        uses: actions/cache@v4
        with:
          path: |
            .lake/build/doc/Aesop
            .lake/build/doc/Batteries
            .lake/build/doc/find
            .lake/build/doc/Init
            .lake/build/doc/Lake
            .lake/build/doc/Lean
            .lake/build/doc/Mathlib
            .lake/build/doc/Std
          key: Docs-${{ hashFiles('lake-manifest.json') }}

      - name: Build project API documentation
        run: |
          rm -rf .lake/build/doc-data .lake/build/api-docs.db
          DISABLE_EQUATIONS=1 ~/.elan/bin/lake -R -Kenv=dev build NN:docs
      
      - name: Detect homepage folder
        id: check_home_page
        run: |
          if [ -d home_page ]; then
            echo "The 'home_page' folder exists in the repository."
            echo "HOME_PAGE_EXISTS=true" >> $GITHUB_ENV
          else
            echo "The 'home_page' folder does not exist in the repository."
            echo "HOME_PAGE_EXISTS=false" >> $GITHUB_ENV
          fi

      - name: Build Verso guide (blueprint package) and copy to `home_page/blueprint`
        run: |
          cd blueprint
          ~/.elan/bin/lake exe cache get || true
          rm -f ~/.cache/mathlib/*.ltar || true
          ~/.elan/bin/lake exe blueprint-gen --output ../_out/blueprint
          cd ..
          if [ -d blueprint/TorchLeanBlueprint/Guide/Assets ]; then
            mkdir -p _out/blueprint/html-multi/Guide/Assets
            cp -r blueprint/TorchLeanBlueprint/Guide/Assets/* _out/blueprint/html-multi/Guide/Assets/
          fi
          python3 scripts/docs/polish_verso_guide.py --guide _out/blueprint/html-multi
          rm -rf home_page/blueprint
          mkdir -p home_page/blueprint
          cp -r _out/blueprint/html-multi/* home_page/blueprint/

      - name: Copy API documentation to `home_page/docs`
        run: |
          rm -rf home_page/docs
          cp -r .lake/build/doc home_page/docs
          python3 scripts/docs/polish_docgen.py --docs home_page/docs
          du -sh home_page/docs

      - name: Trim Lake build metadata from docs
        run: |
          find home_page/docs -name "*.trace" -delete
          find home_page/docs -name "*.hash" -delete

      - name: Reset generated manual output
        run: rm -rf home_page/manual

      - name: Build dependency graph audit
        run: |
          python3 scripts/checks/dependency_audit.py \
            --root "$PWD" \
            --json home_page/graphs/dependency-audit.json \
            --markdown home_page/graphs/dependency-audit.md \
            --fail-on-error

      - name: Build interactive import graph HTML
        run: |
          mkdir -p home_page/importgraph
          ~/.elan/bin/lake exe graph --to NN.Library home_page/importgraph/index.html
          python3 - <<'PY'
          from pathlib import Path

          page = Path("home_page/importgraph/index.html")
          html = page.read_text(encoding="utf-8")
          html = html.replace('  <link rel="stylesheet" href="style.css" />\n', "")
          html = html.replace(
              'var docs_url = params.get("docs_url") || "https://leanprover-community.github.io/mathlib4_docs/";',
              'var docs_url = params.get("docs_url") || new URL("../docs/", window.location.href).href;',
          )
          page.write_text(html, encoding="utf-8")
          PY

      - name: Bundle dependencies
        uses: ruby/setup-ruby@v1
        with:
          working-directory: home_page
          ruby-version: "3.0"
          bundler-cache: true

      - name: Build website using Jekyll
        if: env.HOME_PAGE_EXISTS == 'true'
        working-directory: home_page
        env:
          JEKYLL_GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
        run: JEKYLL_ENV=production bundle exec jekyll build

      - name: "Upload website (API documentation, blueprint and any home page)"
        if: github.event_name != 'pull_request'
        uses: actions/upload-pages-artifact@v3
        with:
          path: ${{ env.HOME_PAGE_EXISTS == 'true' && 'home_page/_site' || 'home_page/' }}

  deploy_pages:
    runs-on: ubuntu-latest
    name: Deploy GitHub Pages
    needs: build_project
    if: github.event_name != 'pull_request'
    permissions:
      pages: write
      id-token: write
    environment:
      name: github-pages
      url: ${{ steps.deployment.outputs.page_url }}
    steps:
      - name: Deploy to GitHub Pages
        id: deployment
        uses: actions/deploy-pages@v4