Trigger CI for leanprover/lean4#8405

Author: leanprover-community-mathlib4-bot

.devcontainer/devcontainer.json

@@ -1,9 +1,7 @@
 {
   "name": "Mathlib4 dev container",
 
-  "build": {
-    "dockerfile": "Dockerfile"
-  },
+  "image": "ghcr.io/leanprover-community/mathlib4/gitpod",
 
   "onCreateCommand": "lake exe cache get!",
 

.github/build.in.yml

@@ -286,54 +286,10 @@ jobs:
     name: Lint styleJOB_NAME
     runs-on: ubuntu-latest
     steps:
-      - name: cleanup
-        run: |
-          find . -name . -o -prune -exec rm -rf -- {} +
-
-      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
-
-      # Run the case checker action
-      - name: Check Case Sensitivity
-        uses: credfeto/action-case-checker@cb652aeab29ed363bbdb7d9ee1bfcc010c46cac5 # v1.3.0
-
-      - name: Look for ignored files
-        uses: credfeto/action-no-ignored-files@4fccae50720d89bef0cd9dc99a85a19b765d2e70 # v1.2.0
-
-      - name: "Check for Lean files with the executable bit set"
-        shell: bash
-        run: |
-          executable_files="$(find . -name '*.lean' -type f \( -perm -u=x -o -perm -g=x -o -perm -o=x \))"
-          if [[ -n "$executable_files" ]]
-          then
-            echo "ERROR: The following Lean files have the executable bit set."
-            echo "$executable_files"
-            exit 1
-          fi
-
-      - name: install Python
-        uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5.6.0
+      - uses: leanprover-community/lint-style-action@f2e7272aad56233a642b08fe974cf09dd664b0c8 # 2025-05-22
         with:
-          python-version: 3.8
-
-      - name: Configure Lean
-        uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # 2025-04-24
-        with:
-          auto-config: false
-          use-github-cache: false
-          use-mathlib-cache: false
-
-      - name: "run style linters"
-        run: |
-          lake exe lint-style
-
-      - name: Install bibtool
-        run: |
-          sudo apt-get update
-          sudo apt-get install -y bibtool
-
-      - name: lint references.bib
-        run: |
-          ./scripts/lint-bib.sh
+          mode: check
+          lint-bib-file: true
 
   final:
     name: Post-CI jobJOB_NAME

.github/workflows/bors.yml

@@ -296,54 +296,10 @@ jobs:
     name: Lint style
     runs-on: ubuntu-latest
     steps:
-      - name: cleanup
-        run: |
-          find . -name . -o -prune -exec rm -rf -- {} +
-
-      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
-
-      # Run the case checker action
-      - name: Check Case Sensitivity
-        uses: credfeto/action-case-checker@cb652aeab29ed363bbdb7d9ee1bfcc010c46cac5 # v1.3.0
-
-      - name: Look for ignored files
-        uses: credfeto/action-no-ignored-files@4fccae50720d89bef0cd9dc99a85a19b765d2e70 # v1.2.0
-
-      - name: "Check for Lean files with the executable bit set"
-        shell: bash
-        run: |
-          executable_files="$(find . -name '*.lean' -type f \( -perm -u=x -o -perm -g=x -o -perm -o=x \))"
-          if [[ -n "$executable_files" ]]
-          then
-            echo "ERROR: The following Lean files have the executable bit set."
-            echo "$executable_files"
-            exit 1
-          fi
-
-      - name: install Python
-        uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5.6.0
+      - uses: leanprover-community/lint-style-action@f2e7272aad56233a642b08fe974cf09dd664b0c8 # 2025-05-22
         with:
-          python-version: 3.8
-
-      - name: Configure Lean
-        uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # 2025-04-24
-        with:
-          auto-config: false
-          use-github-cache: false
-          use-mathlib-cache: false
-
-      - name: "run style linters"
-        run: |
-          lake exe lint-style
-
-      - name: Install bibtool
-        run: |
-          sudo apt-get update
-          sudo apt-get install -y bibtool
-
-      - name: lint references.bib
-        run: |
-          ./scripts/lint-bib.sh
+          mode: check
+          lint-bib-file: true
 
   final:
     name: Post-CI job

.github/workflows/bot_fix_style.yaml

@@ -27,136 +27,8 @@ jobs:
     # && (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@7b90a27f92f3961b368376107661682c441f6103 # v2.3.0
-        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@71345be0265236311c031f5c7866368bd1eff043 # v4.0.0
-        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@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
-        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@a26af69be951a213d495a4c3e4e4022e16d87065 # v5.6.0
+      - uses: leanprover-community/lint-style-action@f2e7272aad56233a642b08fe974cf09dd664b0c8 # 2025-05-22
         with:
-          python-version: 3.8
-
-      - name: Configure Lean
-        uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # 2025-04-24
-        with:
-          auto-config: false
-          use-github-cache: false
-          use-mathlib-cache: false
-
-      # 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 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
+          mode: fix
+          lint-bib-file: true
+          bot-fix-style-token: ${{ secrets.GITHUB_TOKEN }}

.github/workflows/build.yml

@@ -303,54 +303,10 @@ jobs:
     name: Lint style
     runs-on: ubuntu-latest
     steps:
-      - name: cleanup
-        run: |
-          find . -name . -o -prune -exec rm -rf -- {} +
-
-      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
-
-      # Run the case checker action
-      - name: Check Case Sensitivity
-        uses: credfeto/action-case-checker@cb652aeab29ed363bbdb7d9ee1bfcc010c46cac5 # v1.3.0
-
-      - name: Look for ignored files
-        uses: credfeto/action-no-ignored-files@4fccae50720d89bef0cd9dc99a85a19b765d2e70 # v1.2.0
-
-      - name: "Check for Lean files with the executable bit set"
-        shell: bash
-        run: |
-          executable_files="$(find . -name '*.lean' -type f \( -perm -u=x -o -perm -g=x -o -perm -o=x \))"
-          if [[ -n "$executable_files" ]]
-          then
-            echo "ERROR: The following Lean files have the executable bit set."
-            echo "$executable_files"
-            exit 1
-          fi
-
-      - name: install Python
-        uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5.6.0
+      - uses: leanprover-community/lint-style-action@f2e7272aad56233a642b08fe974cf09dd664b0c8 # 2025-05-22
         with:
-          python-version: 3.8
-
-      - name: Configure Lean
-        uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # 2025-04-24
-        with:
-          auto-config: false
-          use-github-cache: false
-          use-mathlib-cache: false
-
-      - name: "run style linters"
-        run: |
-          lake exe lint-style
-
-      - name: Install bibtool
-        run: |
-          sudo apt-get update
-          sudo apt-get install -y bibtool
-
-      - name: lint references.bib
-        run: |
-          ./scripts/lint-bib.sh
+          mode: check
+          lint-bib-file: true
 
   final:
     name: Post-CI job

.github/workflows/build_fork.yml

@@ -300,54 +300,10 @@ jobs:
     name: Lint style (fork)
     runs-on: ubuntu-latest
     steps:
-      - name: cleanup
-        run: |
-          find . -name . -o -prune -exec rm -rf -- {} +
-
-      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
-
-      # Run the case checker action
-      - name: Check Case Sensitivity
-        uses: credfeto/action-case-checker@cb652aeab29ed363bbdb7d9ee1bfcc010c46cac5 # v1.3.0
-
-      - name: Look for ignored files
-        uses: credfeto/action-no-ignored-files@4fccae50720d89bef0cd9dc99a85a19b765d2e70 # v1.2.0
-
-      - name: "Check for Lean files with the executable bit set"
-        shell: bash
-        run: |
-          executable_files="$(find . -name '*.lean' -type f \( -perm -u=x -o -perm -g=x -o -perm -o=x \))"
-          if [[ -n "$executable_files" ]]
-          then
-            echo "ERROR: The following Lean files have the executable bit set."
-            echo "$executable_files"
-            exit 1
-          fi
-
-      - name: install Python
-        uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5.6.0
+      - uses: leanprover-community/lint-style-action@f2e7272aad56233a642b08fe974cf09dd664b0c8 # 2025-05-22
         with:
-          python-version: 3.8
-
-      - name: Configure Lean
-        uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # 2025-04-24
-        with:
-          auto-config: false
-          use-github-cache: false
-          use-mathlib-cache: false
-
-      - name: "run style linters"
-        run: |
-          lake exe lint-style
-
-      - name: Install bibtool
-        run: |
-          sudo apt-get update
-          sudo apt-get install -y bibtool
-
-      - name: lint references.bib
-        run: |
-          ./scripts/lint-bib.sh
+          mode: check
+          lint-bib-file: true
 
   final:
     name: Post-CI job (fork)