Trigger CI for leanprover/lean4#6620

leanprover-community · Jan 17, 2025 · d03e4e1 · d03e4e1
2 parents 36668fc + f059ccd
commit d03e4e1
Show file tree

Hide file tree

Showing 1,847 changed files with 33,258 additions and 20,487 deletions.
diff --git a/.github/build.in.yml b/.github/build.in.yml
@@ -12,19 +12,15 @@ env:
   # not necessarily satisfy this property.
   LAKE_NO_CACHE: true
 
-jobs:
-  # Cancels previous runs of jobs in this file
-  cancel:
-    if: github.repository == 'leanprover-community/mathlib4'
-    name: 'Cancel Previous Runs (CI)'
-    runs-on: ubuntu-latest
-    # timeout-minutes: 3
-    steps:
-      - uses: styfle/[email protected]
-        with:
-          all_but_latest: true
-          access_token: ${{ github.token }}
+concurrency:
+  # label each workflow run; only the latest with each label will run
+  # workflows on master get more expressive labels
+  group: ${{ github.workflow }}-${{ github.ref }}.
+    ${{ ( contains(fromJSON( '["refs/heads/master", "refs/heads/staging"]'), github.ref ) && github.run_id) || ''}}
+  # cancel any running workflow with the same label
+  cancel-in-progress: true
 
+jobs:
   style_lint:
     if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
     name: Lint styleJOB_NAME
@@ -132,7 +128,7 @@ jobs:
         run: |
           rm -rf .lake/build/lib/Mathlib/
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
-          lake exe cache get Mathlib.Init
+          lake exe cache get Mathlib/Init.lean
           lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
@@ -180,10 +176,12 @@ jobs:
           # Because the `lean-pr-testing-NNNN` branches use toolchains that are "updated in place"
           # the cache mechanism is unreliable, so we don't test it if we are on such a branch.
           if [[ ! $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
-            lake exe cache clean!
-            rm -rf .lake/build/lib/Mathlib
+            cd DownstreamTest
+            cp ../lean-toolchain .
+            MATHLIB_NO_CACHE_ON_UPDATE=1 lake update
             lake exe cache get || (sleep 1; lake exe cache get)
-            lake build --no-build
+            lake build Plausible ProofWidgets
+            lake build --no-build Mathlib
           fi
 
       - name: build archive

diff --git a/.github/workflows/PR_summary.yml b/.github/workflows/PR_summary.yml
@@ -99,6 +99,8 @@ jobs:
         ## Technical debt changes
         techDebtVar="$(./scripts/technical-debt-metrics.sh pr_summary)"
 
-        message="$(printf '%s [%s](%s)%s\n\n%s\n\n---\n\n%s\n\n---\n\n%s\n' "${title}" "$(git rev-parse --short HEAD)" "${hashURL}" "${high_percentages}" "${importCount}" "${declDiff}" "${techDebtVar}")"
+        # store in a file, to avoid "long arguments" error.
+        printf '%s [%s](%s)%s\n\n%s\n\n---\n\n%s\n\n---\n\n%s\n' "${title}" "$(git rev-parse --short HEAD)" "${hashURL}" "${high_percentages}" "${importCount}" "${declDiff}" "${techDebtVar}" > messageFile.md
 
-        ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}"
+        cat messageFile.md
+        ./scripts/update_PR_comment.sh messageFile.md "${title}" "${PR}"
diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
@@ -22,19 +22,15 @@ env:
   # not necessarily satisfy this property.
   LAKE_NO_CACHE: true
 
-jobs:
-  # Cancels previous runs of jobs in this file
-  cancel:
-    if: github.repository == 'leanprover-community/mathlib4'
-    name: 'Cancel Previous Runs (CI)'
-    runs-on: ubuntu-latest
-    # timeout-minutes: 3
-    steps:
-      - uses: styfle/[email protected]
-        with:
-          all_but_latest: true
-          access_token: ${{ github.token }}
+concurrency:
+  # label each workflow run; only the latest with each label will run
+  # workflows on master get more expressive labels
+  group: ${{ github.workflow }}-${{ github.ref }}.
+    ${{ ( contains(fromJSON( '["refs/heads/master", "refs/heads/staging"]'), github.ref ) && github.run_id) || ''}}
+  # cancel any running workflow with the same label
+  cancel-in-progress: true
 
+jobs:
   style_lint:
     if: github.repository == 'leanprover-community/mathlib4'
     name: Lint style
@@ -142,7 +138,7 @@ jobs:
         run: |
           rm -rf .lake/build/lib/Mathlib/
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
-          lake exe cache get Mathlib.Init
+          lake exe cache get Mathlib/Init.lean
           lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
@@ -190,10 +186,12 @@ jobs:
           # Because the `lean-pr-testing-NNNN` branches use toolchains that are "updated in place"
           # the cache mechanism is unreliable, so we don't test it if we are on such a branch.
           if [[ ! $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
-            lake exe cache clean!
-            rm -rf .lake/build/lib/Mathlib
+            cd DownstreamTest
+            cp ../lean-toolchain .
+            MATHLIB_NO_CACHE_ON_UPDATE=1 lake update
             lake exe cache get || (sleep 1; lake exe cache get)
-            lake build --no-build
+            lake build Plausible ProofWidgets
+            lake build --no-build Mathlib
           fi
 
       - name: build archive

diff --git a/.github/workflows/bot_fix_style.yaml b/.github/workflows/bot_fix_style.yaml
@@ -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
diff --git a/.github/workflows/bot_fix_style_comment.yaml b/.github/workflows/bot_fix_style_comment.yaml