blueprint-paper.yml

name: Compile blueprint and paper

on:
  push:
    branches:
      - main
    paths:
      - '**/*.lean'
      - '**/blueprint-paper.yml'
      - 'blueprint/**'
      - 'commentary/**'
      - 'home_page/**'
      - 'tools/fme/**'
      - '**/generate_dashboard.py'
      - '**/generate_dashboard_graph_info.rb'
      - '**/generate_equation_implication_js.py'
      - '**/generate_equation_explorer_graph.py'
      - '**/generate_graphiti_data.rb'
      - 'lean-toolchain'
      - 'lakefile.toml'
      - 'lake-manifest.json'
      - 'paper/**'
  pull_request:
    branches:
      - main
    paths:
      - '**/*.lean'
      - '**/blueprint-paper.yml'
      - 'blueprint/**'
      - 'commentary/**'
      - 'home_page/**'
      - 'tools/fme/**'
      - '**/generate_dashboard.py'
      - '**/generate_dashboard_graph_info.rb'
      - '**/generate_equation_implication_js.py'
      - '**/generate_equation_explorer_graph.py'
      - '**/generate_graphiti_data.rb'
      - './scripts/**'
      - 'lean-toolchain'
      - 'lakefile.toml'
      - 'lake-manifest.json'
      - 'paper/**'
  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: Add 'awaiting-CI' label
        if: >
          github.event_name == 'pull_request'
        run: |
          curl --request POST \
            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels \
            --header 'authorization: Bearer ${{ secrets.PAT_TOKEN }}' \
            --header 'Content-Type: application/json' \
            --data '["awaiting-CI"]'

      - 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 Mathlib API docs
        uses: actions/cache@v4
        with:
          path: |
            .lake/build
            !.lake/build/doc-data
            !.lake/build/doc/declarations/declaration-data-equational_theories*
          key: LakeBuild-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
          #restore-keys: LakeBuild-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}

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

      - name: Check environment with lean4checker
        run: |
          : Check Environment with lean4checker
          chmod +x ./scripts/lean4_checker/run_lean4checker.sh
          ./scripts/lean4_checker/run_lean4checker.sh
        shell: bash

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

      - name: Check for `home_page` 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 blueprint and copy to `home_page/blueprint`
        uses: xu-cheng/texlive-action@v2
        with:
          docker_image: ghcr.io/xu-cheng/texlive-full:latest
          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

            # Build the blueprint and copy it to `home_page`
            leanblueprint pdf
            mkdir -p home_page
            cp blueprint/print/print.pdf home_page/blueprint.pdf
            leanblueprint web
            cp -r blueprint/web home_page/blueprint

            # Compile the paper and copy it to `home_page`
            cd paper
            latexmk -pdf main.tex
            cd ..
            cp paper/main.pdf home_page/paper.pdf

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

      - name: Check with lean4lean
        run: |
            python scripts/lean4lean_checker/main.py

      - 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: Generate graph data
        run: |
          mkdir /tmp/raw_data
          ~/.elan/bin/lake exe extract_implications --json > /tmp/raw_data/general.json
          ~/.elan/bin/lake exe extract_implications --json --closure --only-implications > /tmp/raw_data/general_implications_closure.json
          ~/.elan/bin/lake exe extract_implications raw --full-entries > /tmp/raw_data/general_raw_full_entries.json
          ~/.elan/bin/lake exe extract_implications outcomes > /tmp/raw_data/general_outcomes.json

          ~/.elan/bin/lake exe extract_implications --json --finite-only > /tmp/raw_data/finite.json
          ~/.elan/bin/lake exe extract_implications --json --finite-only --closure --only-implications > /tmp/raw_data/finite_implications_closure.json
          ~/.elan/bin/lake exe extract_implications raw --full-entries --finite-only > /tmp/raw_data/finite_raw_full_entries.json
          ~/.elan/bin/lake exe extract_implications outcomes --finite-only > /tmp/raw_data/finite_outcomes.json

      - name: Generate compressed home_page/raw_data files
        if: github.event_name == 'push'
        run: |
          mkdir home_page/raw_data
          gzip -k /tmp/raw_data/*.json
          mv /tmp/raw_data/*.gz home_page/raw_data

      - name: Generate home_page/dashboard.md
        run: |
          pip install pillow
          ruby scripts/generate_dashboard_graph_info.rb > /tmp/graph_info.md
          python scripts/generate_dashboard.py /tmp/graph_info.md
          python scripts/outcomes_to_image.py /tmp/raw_data/general_outcomes.json --out home_page/dashboard/outcomes.png

      - name: Generate equation explorer data
        run: |
          pip install markdown
          python scripts/generate_equation_implication_js.py > home_page/implications/implications.js
          python scripts/generate_equation_explorer_graph.py /tmp/raw_data/general_outcomes.json /tmp/raw_data/general_raw_full_entries.json > home_page/implications/graph.json
          python scripts/generate_equation_explorer_graph.py /tmp/raw_data/finite_outcomes.json /tmp/raw_data/finite_raw_full_entries.json > home_page/implications/finite_graph.json

      - name: Generate the Finite Magma Explorer website
        run: |
          mkdir -p home_page/fme
          cp -r tools/fme/dist/* home_page/fme
          ~/.elan/bin/lake exe extract_implications unknowns --finite-only > home_page/fme/unknowns.json
          COMMIT_HASH=$(git rev-parse --short HEAD)
          sed -i "s/UNKNOWN_VERSION/$COMMIT_HASH/g" home_page/fme/index.html

      - 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: Generate home_page/graphiti/graph.json
        run: |
          ~/.elan/bin/lake exe extract_implications unknowns > /tmp/unknowns.json
          ~/.elan/bin/lake exe extract_implications unknowns --finite-only > /tmp/unknowns.fin.json
          ruby scripts/generate_graphiti_data.rb data/duals.json /tmp/raw_data/general_implications_closure.json /tmp/unknowns.json /tmp/raw_data/finite_implications_closure.json /tmp/unknowns.fin.json > home_page/graphiti/graph.json

      - name: Build website using Jekyll
        if: github.event_name == 'push' && env.HOME_PAGE_EXISTS == 'true'
        working-directory: home_page
        env:
          JEKYLL_GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
        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, paper 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

      # - name: Make sure the API documentation cache works
      #   run: mv home_page/docs .lake/build/doc

      - name: Remove 'awaiting-CI' label
        if: >
          always() &&
          github.event_name == 'pull_request'
        run: |
          curl --request DELETE \
            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels/awaiting-CI \
            --header 'authorization: Bearer ${{ secrets.PAT_TOKEN }}' \
            --header 'Content-Type: application/json'