bot fix style #361
Workflow file for this run
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: bot fix style | |
| # triggers the action when | |
| on: | |
| issue_comment: | |
| # the PR receives a comment, or a comment is edited | |
| types: [created, edited] | |
| pull_request_review: | |
| # triggers on a review, whether or not it is accompanied by a comment | |
| types: [submitted] | |
| pull_request_review_comment: | |
| # triggers on a review comment | |
| types: [created, edited] | |
| jobs: | |
| fix_style: | |
| # we set some variables. The ones of the form `${{ X }}${{ Y }}` are typically not | |
| # both set simultaneously: depending on the event that triggers the PR, usually only one is set | |
| env: | |
| AUTHOR: ${{ github.event.comment.user.login }}${{ github.event.review.user.login }} | |
| COMMENT_EVENT: ${{ github.event.comment.body }} | |
| COMMENT_REVIEW: ${{ github.event.review.body }} | |
| COMMENT_REVIEW_COMMENT: ${{ github.event.pull_request_review_comment.body }} | |
| name: Fix style issues from lint | |
| # the `if` works with `comment`s, but not with `review`s or `review_comment`s | |
| # if: github.event.issue.pull_request | |
| # && (startsWith(github.event.comment.body, 'bot fix style') || contains(toJSON(github.event.comment.body), '\nbot fix style')) | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Find bot fix style | |
| id: bot_fix_style | |
| run: | | |
| COMMENT="${COMMENT_EVENT}${COMMENT_REVIEW}${COMMENT_REVIEW_COMMENT}" | |
| # we strip `\r` since line endings from GitHub contain this character | |
| COMMENT="${COMMENT//$'\r'/}" | |
| # for debugging, we print some information | |
| printf '%s' "${COMMENT}" | hexdump -cC | |
| printf 'Comment:"%s"\n' "${COMMENT}" | |
| bot_fix_style="$(printf '%s' "${COMMENT}" | | |
| sed -n 's=^bot fix style$=bot-fix-style=p' | head -1)" | |
| printf $'"bot fix style"? \'%s\'\n' "${bot_fix_style}" | |
| printf $'AUTHOR: \'%s\'\n' "${AUTHOR}" | |
| printf $'PR_NUMBER: \'%s\'\n' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}" | |
| printf $'%s' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}" | hexdump -cC | |
| printf $'bot_fix_style=%s\n' "${bot_fix_style}" >> "${GITHUB_OUTPUT}" | |
| # these final variables are probably not relevant for the bot_fix_style action | |
| if [ "${AUTHOR}" == 'leanprover-community-mathlib4-bot' ] || | |
| [ "${AUTHOR}" == 'leanprover-community-bot-assistant' ] | |
| then | |
| printf $'bot=true\n' | |
| printf $'bot=true\n' >> "${GITHUB_OUTPUT}" | |
| else | |
| printf $'bot=false\n' | |
| printf $'bot=false\n' >> "${GITHUB_OUTPUT}" | |
| fi | |
| - id: user_permission | |
| if: steps.bot_fix_style.outputs.bot_fix_style == 'bot-fix-style' | |
| uses: actions-cool/check-user-permission@v2 | |
| with: | |
| require: 'write' | |
| # from now on, it is sufficient to just check `user_permission`: | |
| # if the comment did not contain `bot fix style`, | |
| # then `user_permission` would not have ran | |
| - name: Add reaction (comment) | |
| # reactions are only supported for `comment`s and `review_comment`s? | |
| # This action only runs on `comment`s rather than `review`s or `review_comment`s | |
| # Is the `id` check a good way to check that this is a `comment`? | |
| if: ${{ steps.user_permission.outputs.require-result == 'true' && | |
| ! github.event.comment.id == '' }} | |
| uses: peter-evans/create-or-update-comment@v4 | |
| with: | |
| comment-id: ${{ github.event.comment.id }} | |
| reactions: rocket | |
| - name: Add reaction (review comment) | |
| # this action only runs on `review_comment`s | |
| # is the `id` check a good way to check that this is a `review_comment`? | |
| if: ${{ steps.user_permission.outputs.require-result == 'true' && | |
| ! github.event.pull_request_review_comment.id == '' }} | |
| 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/comments/${{ github.event.comment.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: | | |
| # covers `comment`s | |
| gh pr checkout ${{ github.event.issue.number }} || | |
| # covers `review`s and `review_comment`s | |
| 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@v5 | |
| 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 "[email protected]" | |
| git add . | |
| # Don't fail if there's nothing to commit | |
| git commit -m "commit changes from style linters" || true | |
| git push origin HEAD |