push_master.yml

name: Build Lean project

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:
  style_lint:
    name: Lint style
    runs-on: ubuntu-latest
    steps:
      - name: Check for long lines
        if: always()
        run: |
          ! (find LeanCamCombi -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')

      - name: Don't 'import Mathlib', use precise imports
        if: always()
        run: |
          ! (find LeanCamCombi -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$')

  build_project:
    runs-on: ubuntu-latest
    name: Build project
    steps:
      - name: Checkout project
        uses: actions/checkout@v2

      - name: Copy README.md to website/index.md
        run: cp README.md website/index.md

      - 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 exe cache get || true

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

      - name: Print files to upstream
        run: |
          mkdir -p website/_includes
          python3 scripts/upstreaming_dashboard.py
          python3 scripts/import_graph.py

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

      - name: Build documentation
        working-directory: docbuild
        run: |
          ~/.elan/bin/lake exe cache get || true
          ~/.elan/bin/lake build LeanCamCombi:docs

      # - name: Build blueprint and copy to `website/blueprint`
      #   uses: xu-cheng/texlive-action@v2
      #   with:
      #     scheme: full
      #     run: |
      #       apk update
      #       apk add --update make py3-pip git
      #       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 pip install --upgrade pip requests wheel
      #       python3 -m pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
      #       pip install -r blueprint/requirements.txt
      #       python3 -m pip install invoke
      #       inv all

      - name: Copy documentation to `website/docs`
        run: |
          mv docbuild/.lake/build/doc website/docs

      - name: Bundle dependencies
        uses: ruby/setup-ruby@v1
        with:
          working-directory: website
          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: website
        run: JEKYLL_ENV=production bundle exec jekyll build

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

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

      - name: Make sure the cache works
        run: |
          mv website/docs docbuild/.lake/build/doc