feat: Nesbitt's inequality #13737
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 (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@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 "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 |