Trigger CI for leanprover/lean4#6329

.github/PULL_REQUEST_TEMPLATE.md

@@ -20,7 +20,7 @@ If you are moving or deleting declarations, please include these lines at the bo
 (that is, before the `---`) using the following format:
 
 Moves:
-- Vector.* -> Mathlib.Vector.*
+- Vector.* -> List.Vector.*
 - ...
 
 Deletions:

.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
@@ -240,7 +238,7 @@ jobs:
 
       - name: check declarations in db files
         run: |
-          python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
+          python3 scripts/yaml_check.py docs/100.yaml docs/1000.yaml docs/overview.yaml docs/undergrad.yaml
           lake exe check-yaml
 
       - name: generate our import graph

.github/workflows/PR_summary.yml

@@ -14,6 +14,27 @@ jobs:
       with:
         fetch-depth: 0
 
+    - name: Update the merge-conflict label
+      run: |
+        printf 'PR number: "%s"\n' "${{ github.event.pull_request.number }}"
+        if git merge origin/master --no-ff --no-commit
+        then
+          git merge --abort || true
+          echo "This PR does not have merge conflicts with master."
+          # we use curl rather than octokit/request-action so that the job won't fail
+          # (and send an annoying email) if the labels don't exist
+          curl --request DELETE \
+            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels/merge-conflict \
+            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
+        else
+          echo "This PR has merge conflicts with main."
+          # we use curl rather than octokit/request-action so that the job won't fail
+          # (and send an annoying email) if the labels don't exist
+          curl --request POST \
+            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels/merge-conflict \
+            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
+        fi
+
     - name: Set up Python
       uses: actions/setup-python@v5
       with:
@@ -99,6 +120,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}"

.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
@@ -250,7 +248,7 @@ jobs:
 
       - name: check declarations in db files
         run: |
-          python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
+          python3 scripts/yaml_check.py docs/100.yaml docs/1000.yaml docs/overview.yaml docs/undergrad.yaml
           lake exe check-yaml
 
       - name: generate our import graph

.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