bot_fix_style_review.yaml

name: bot fix style (review)

on:
  pull_request_review:
    # triggers on a review, whether or not it is accompanied by a comment
    types: [submitted]

jobs:
  fix_style:
    name: Fix style issues from lint
    if: (startsWith(github.event.review.body, 'bot fix style') || contains(toJSON(github.event.review.body), '\nbot fix style'))
    runs-on: ubuntu-latest
    steps:
      - id: user_permission
        uses: actions-cool/check-user-permission@v2
        with:
          require: 'write'

      # Maybe no API exists for this yet?
      # - name: Add reaction
      #   if: steps.user_permission.outputs.require-result == 'true'
      #   run: |
      #       gh api --method POST \
      #         -H "Accept: application/vnd.github+json" \
      #         -H "X-GitHub-Api-Version: 2022-11-28" \
      #         /repos/${{ github.repository_owner }}/${{ github.event.repository.name }}/pulls/${{ github.event.pull_request.number }}/reviews/${{ github.event.review.id }}/reactions \
      #         -f "content=rocket"
      #   env:
      #       GH_TOKEN: ${{ secrets.BOT_FIX_STYLE_TOKEN }}

      - name: cleanup
        if: steps.user_permission.outputs.require-result == 'true'
        run: |
          find . -name . -o -prune -exec rm -rf -- {} +

      - uses: actions/checkout@v4
        if: steps.user_permission.outputs.require-result == 'true'
        with:
          token: ${{ secrets.BOT_FIX_STYLE_TOKEN }}

      - name: Checkout PR branch
        if: steps.user_permission.outputs.require-result == 'true'
        run: |
            gh pr checkout ${{ github.event.pull_request.number }}
        env:
            GH_TOKEN: ${{ secrets.BOT_FIX_STYLE_TOKEN }}

      - name: install Python
        if: steps.user_permission.outputs.require-result == 'true'
        uses: actions/setup-python@v4
        with:
          python-version: 3.8

      - name: install elan
        if: steps.user_permission.outputs.require-result == 'true'
        run: |
          set -o pipefail
          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
          ./elan-init -y --default-toolchain none
          echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"

      # run the same linting steps as in lint_and_suggest_pr.yaml

      - name: lint
        if: steps.user_permission.outputs.require-result == 'true'
        run: |
          lake exe lint-style --fix

      - name: Install bibtool
        if: steps.user_permission.outputs.require-result == 'true'
        run: |
          sudo apt-get update
          sudo apt-get install -y bibtool

      - name: lint references.bib
        if: steps.user_permission.outputs.require-result == 'true'
        run: |
          # ignoring the return code allows the following `reviewdog` step to add GitHub suggestions
          ./scripts/lint-bib.sh || true

      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
        if: steps.user_permission.outputs.require-result == 'true'
        run: |
          # ignoring the return code allows the following `reviewdog` step to add GitHub suggestions
          lake exe mk_all || true

      - name: Commit and push changes
        if: steps.user_permission.outputs.require-result == 'true'
        run: |
          # cleanup junk from build
          rm elan-init
          rm docs/references.bib.old
          # setup commit and push
          git config user.name "leanprover-community-mathlib4-bot"
          git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
          git add .
          # Don't fail if there's nothing to commit
          git commit -m "commit changes from style linters" || true
          git push origin HEAD