blueprint.yml

name: Compile blueprint

on:
  push:
    branches:
      - main
    paths:
      - '**/*.lean'
      - '**/blueprint.yml'
      - 'blueprint/**'
      - 'home_page/**'
      - 'lean-toolchain'
      - 'lakefile.toml'
      - 'lake-manifest.json'
  pull_request:
    branches:
      - main
    paths:
      - '**/*.lean'
      - '**/blueprint.yml'
      - 'blueprint/**'
      - 'home_page/**'
      - 'lean-toolchain'
      - 'lakefile.toml'
      - 'lake-manifest.json'
  workflow_dispatch: # Allow manual triggering of the workflow from the GitHub Actions interface

# Cancel previous runs if a new commit is pushed to the same PR or branch
concurrency:
  group: ${{ github.ref }}  # Group runs by the ref (branch or PR)
  cancel-in-progress: true  # Cancel any ongoing runs in the same group

# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages and modify PR labels
permissions:
  contents: read          # Read access to repository contents
  pages: write            # Write access to GitHub Pages
  id-token: write         # Write access to ID tokens
  issues: write           # Write access to issues
  pull-requests: write    # Write access to pull requests

jobs:
  build_project:
    runs-on: ubuntu-latest
    name: Build project
    steps:
      - name: Checkout project
        uses: actions/checkout@v4
        with:
          fetch-depth: 0 # Fetch all history for all branches and tags

      - 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

      - name: Cache build artifacts and API docs
        uses: actions/cache@v4
        with:
          path: |
            .lake/build
          key: LakeBuild-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
          #restore-keys: LakeBuild-

      - name: Build project
        run: ~/.elan/bin/lake build InfinityCosmos

      # .lake/build/doc/Init
      # .lake/build/doc/Lake
      # .lake/build/doc/Lean
      # .lake/build/doc/Std
      # .lake/build/doc/Mathlib
      # .lake/build/doc/declarations
      # .lake/build/doc/find
      # .lake/build/doc/*.*
      # !.lake/build/doc/declarations/declaration-data-InfinityCosmos*

      - name: Build project API documentation
        run: ~/.elan/bin/lake -R -Kenv=dev build InfinityCosmos:docs

      - name: Check for `home_page` folder # this is meant to detect a Jekyll-based website
        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 blueprint and copy to `home_page/blueprint`
        uses: xu-cheng/texlive-action@v2
        with:
          docker_image: ghcr.io/xu-cheng/texlive-full:20231201
          run: |
            # Install necessary dependencies and build the blueprint
            apk update
            apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev
            git config --global --add safe.directory $GITHUB_WORKSPACE
            git config --global --add safe.directory `pwd`
            python3 -m venv env
            source env/bin/activate
            pip install --upgrade pip requests wheel
            pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
            pip install leanblueprint
            leanblueprint pdf
            mkdir -p home_page
            cp blueprint/print/print.pdf home_page/blueprint.pdf
            leanblueprint web
            cp -r blueprint/web home_page/blueprint

      - name: Check declarations mentioned in the blueprint exist in Lean code
        run: |
            ~/.elan/bin/lake exe checkdecls blueprint/lean_decls

      - name: Copy API documentation to `home_page/docs`
        run: cp -r .lake/build/doc home_page/docs

      # - name: Remove unnecessary lake files from documentation in `home_page/docs`
      #   run: |
      #     find home_page/docs -name "*.trace" -delete
      #     find home_page/docs -name "*.hash" -delete

      - name: Bundle dependencies
        if: github.event_name == 'push'
        uses: ruby/setup-ruby@v1
        with:
          working-directory: home_page
          ruby-version: "3.0"  # Specify Ruby version
          bundler-cache: true  # Enable caching for bundler

      - name: Build website using Jekyll
        if: github.event_name == 'push' && env.HOME_PAGE_EXISTS == 'true'
        working-directory: home_page
        run: JEKYLL_ENV=production bundle exec jekyll build  # Note this will also copy the blueprint and API doc into home_page/_site

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

      - name: Deploy to GitHub Pages
        if: github.event_name == 'push'
        id: deployment
        uses: actions/deploy-pages@v4

  # Enable status check to ensure all jobs succeeded
  check:
    if: always()
    name: Check
    needs:
      - build_project
    runs-on: ubuntu-latest
    steps:
    - name: Decide whether the needed jobs succeeded or failed
      uses: re-actors/alls-green@release/v1
      with:
        jobs: ${{ toJSON(needs) }}