-
Notifications
You must be signed in to change notification settings - Fork 369
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'master' into ACL/CombNS
- Loading branch information
Showing
2,606 changed files
with
65,494 additions
and
34,279 deletions.
There are no files selected for viewing
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
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
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
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,164 @@ | ||
| 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 |
This file was deleted.
Oops, something went wrong.
Oops, something went wrong.