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:
  style_lint:
    name: Lint style
    runs-on: ubuntu-latest
    steps:
      - name: Check for long lines
        if: always()
        run: |
          ! (find Carleson -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 Carleson -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
        with:
          fetch-depth: 0

      - 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 # Install Lean 4

      - name: Update docgen4
        run: ~/.elan/bin/lake -R -Kenv=dev update «doc-gen4»

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

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

      - name: Cache mathlib docs
        uses: actions/cache@v3
        with:
          path: |
            .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/declarations/declaration-data-Carleson*
          key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
          restore-keys: |
            MathlibDoc- # Cache Mathlib documentation to save rebuild time

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

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

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

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

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

      - name: Remove lake files from documentation
        run: |
          find .lake/build/doc -name "*.trace" -delete
          find .lake/build/doc -name "*.hash" -delete

      - name: Copy documentation to `docs/docs`
        run: |
          sudo chown -R runner docs
          cp -r .lake/build/doc docs/docs # Copy the built documentation to the correct directory

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

      - name: Bundle website
        working-directory: docs
        run: JEKYLL_ENV=production bundle exec jekyll build # Build the Jekyll site for production

      - 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