push.yml

on:
  push:
    branches:
      - master

# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
permissions:
  contents: read
  pages: write
  id-token: write

jobs:
  build_project:
    runs-on: ubuntu-latest
    name: Build project
    concurrency:
      group: ${{ github.workflow }}-${{ github.ref }}
      cancel-in-progress: true
    steps:
      # - name: Free disk space
      #   uses: jlumbroso/free-disk-space@main
      #   with:
      #     # this might remove tools that are actually needed,
      #     # if set to "true" but frees about 6 GB
      #     tool-cache: false

      #     # all of these default to true, but feel free to set to
      #     # "false" if necessary for your workflow
      #     android: true
      #     dotnet: true
      #     haskell: true
      #     large-packages: true
      #     docker-images: true
      #     swap-storage: true

      - name: Checkout project
        uses: actions/checkout@v2
        with:
          fetch-depth: 0

      - name: Print files to upstream
        run: |
          grep -r --files-without-match 'import LeanAPAP' LeanAPAP | sort > 1.txt
          grep -r --files-with-match 'sorry' LeanAPAP | sort > 2.txt
          comm -23 1.txt 2.txt | sed -e 's/^\(.*\)$/- [`\1`](https:\/\/github.com\/YaelDillies\/LeanAPAP\/blob\/main\/\1)/' > docs/_includes/files_to_upstream.md
          rm 1.txt 2.txt

      - name: Count sorries
        run: python scripts/count_sorry.py

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

      - name: Get cache
        run: ~/.elan/bin/lake -Kenv=dev exe cache get

      - name: Build project
        run: ~/.elan/bin/lake -Kenv=dev build LeanAPAP

      - name: Cache mathlib docs
        uses: actions/cache@v3
        with:
          path: build/doc/Mathlib
          key: DocGen4-${{ hashFiles('lake-manifest.json') }}
          restore-keys: |
            DocGen4-

      - name: Build documentation
        run: ~/.elan/bin/lake -Kenv=dev build LeanAPAP:docs

      - name: Install Python
        uses: actions/setup-python@v4
        with:
          python-version: '3.9'
          cache: 'pip' # caching pip dependencies

      - name: Install blueprint apt dependencies
        run: |
          sudo apt-get update
          sudo apt-get install -y graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full

      - name: Install blueprint dependencies
        run: |
          cd blueprint && pip install -r requirements.txt

      - name: Build blueprint and copy to `docs/blueprint`
        run: |
          inv all

      - name: Copy documentation to `docs/docs`
        run: |
          mv build/doc docs/docs

      - name: Bundle dependencies
        uses: ruby/setup-ruby@v1
        with:
          working-directory: docs
          ruby-version: "3.0" # Not needed with a .ruby-version file
          bundler-cache: true # runs 'bundle install' and caches installed gems automatically

      - name: Bundle website
        working-directory: docs
        run: JEKYLL_ENV=production bundle exec jekyll build

      - name: Upload docs & blueprint artifact
        uses: actions/upload-pages-artifact@v1
        with:
          path: docs/_site

      - name: Deploy to GitHub Pages
        id: deployment
        uses: actions/deploy-pages@v1