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: 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@v4
        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 none

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

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

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

      # - name: Cache mathlib documentation
      #   uses: actions/cache@v4
      #   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/find
      #       .lake/build/doc/*.*
      #       !.lake/build/doc/declarations/declaration-data-Carleson*
      #     key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
      #     restore-keys: MathlibDoc-

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

      - name: Setup symlinks between project and docbuild
        working-directory: docbuild
        run: |
          mkdir -p .lake/packages
          for package_path in ../.lake/packages/*; do
            package=$(basename $package_path)
            ln -s ../../../.lake/packages/$package .lake/packages/$package
          done

      - name: Build project documentation
        working-directory: docbuild
        run: |
          ~/.elan/bin/lake update carleson || true
          ~/.elan/bin/lake build Carleson:docs

      - name: Build blueprint and copy to `docs/blueprint`
        uses: xu-cheng/texlive-action@v2
        with:
          docker_image: ghcr.io/xu-cheng/texlive-full:20231201
          run: |
            export PIP_BREAK_SYSTEM_PACKAGES=1
            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
            cp blueprint/print/print.pdf docs/blueprint.pdf
            leanblueprint web
            cp -r blueprint/web docs/blueprint

      - name: Check declarations
        run: ~/.elan/bin/lake exe checkdecls blueprint/lean_decls

      - name: Copy documentation to `docs/docs`
        run: |
          sudo chown -R runner docs
          cp -r docbuild/.lake/build/doc docs/docs

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

      - 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
        env:
            JEKYLL_GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
        run: JEKYLL_ENV=production bundle exec jekyll build

      # - name: Upload docs & blueprint artifact to `docs/`
      #   uses: actions/upload-pages-artifact@v3
      #   with:
      #     path: docs/

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

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

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