forked from leanprover-community/mathlib4
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
4,785 changed files
with
123,228 additions
and
208,689 deletions.
The diff you're trying to view is too large. We only load the first 3000 changed files.
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
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,93 @@ | ||
| name: bot fix style (comment) | ||
|
|
||
| on: | ||
| issue_comment: | ||
| types: [created, edited] | ||
|
|
||
| jobs: | ||
| fix_style: | ||
| name: Fix style issues from lint | ||
| 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: | ||
| - id: user_permission | ||
| uses: actions-cool/check-user-permission@v2 | ||
| with: | ||
| require: 'write' | ||
|
|
||
| - name: Add reaction | ||
| if: steps.user_permission.outputs.require-result == 'true' | ||
| uses: peter-evans/create-or-update-comment@v4 | ||
| with: | ||
| comment-id: ${{ github.event.comment.id }} | ||
| reactions: rocket | ||
|
|
||
| - 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.issue.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 |
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,99 @@ | ||
| 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 |
Oops, something went wrong.