Merge branch 'greedoid-for-contrib-with-finset-arrow-prop' into greed…

…oid-for-contrib

Further work on greedoid-for-contrib will be done on its own branch.

.github/workflows/build.yml.in → .github/build.in.yml

@@ -1,3 +1,8 @@
+### NB: This is the master file for autogenerating
+### NB: `.github/workflows/{bors, build_fork, build}.yml`.
+### NB: If you need to edit any of those files, you should edit this file instead,
+### NB: and regenerate those files by manually running
+### NB: .github/workflows/mk_build_yml.sh
 
 jobs:
   # Cancels previous runs of jobs in this file
@@ -30,6 +35,17 @@ jobs:
       - name: Look for ignored files
         uses: credfeto/action-no-ignored-files@v1.1.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
         if: ${{ 'STYLE_LINT_RUNNER' == 'ubuntu-latest' }}
         uses: actions/setup-python@v5
@@ -43,9 +59,9 @@ jobs:
           ./elan-init -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 
-      - name: "run style linters: Python ones and their Lean rewrite"
+      - name: "run style linters"
         run: |
-          ./scripts/lint-style.sh
+          lake exe lint-style
 
       - name: Install bibtool
         if: ${{ 'STYLE_LINT_RUNNER' == 'ubuntu-latest' }}
@@ -57,25 +73,6 @@ jobs:
         run: |
           ./scripts/lint-bib.sh
 
-  check_workflows:
-    if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
-    name: check workflowsJOB_NAME
-    runs-on: ubuntu-latest
-    steps:
-      - name: cleanup
-        run: |
-          find . -name . -o -prune -exec rm -rf -- {} +
-
-      - uses: actions/checkout@v4
-
-      - name: update workflows
-        run: |
-          cd .github/workflows/
-          ./mk_build_yml.sh
-
-      - name: check that workflows were consistent
-        run: git diff --exit-code
-
   build:
     if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
     name: BuildJOB_NAME
@@ -118,9 +115,6 @@ jobs:
           lean --version
           lake --version
 
-      - name: check {Mathlib, Tactic, Counterexamples, Archive}.lean are up to date
-        run: lake exe mk_all --check
-
       - name: build cache
         run: |
           lake build cache
@@ -137,8 +131,22 @@ jobs:
       - name: get cache
         id: get
         run: |
-          lake exe cache clean
-          lake exe cache get
+          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 build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
+
+      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
+        id: mk_all
+        run: |
+
+          if ! lake exe mk_all --check
+          then
+            echo "Not all lean files are in the import all files"
+            echo "mk_all=false" >> "${GITHUB_OUTPUT}"
+          else
+            echo "mk_all=true" >> "${GITHUB_OUTPUT}"
+          fi
 
       - name: build mathlib
         id: build
@@ -202,6 +210,14 @@ jobs:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
+      - name: Check {Mathlib, Tactic, Counterexamples, Archive}.lean
+        run: |
+          if [ ${{ steps.mk_all.outputs.mk_all }} == "false" ]
+          then
+            echo "Please run 'lake exe mk_all' to regenerate the import all files"
+            exit 1
+          fi
+
       - name: check for noisy stdout lines
         id: noisy
         run: |
@@ -262,7 +278,7 @@ jobs:
       # Output is posted to the zulip topic
       # https://leanprover.zulipchat.com/#narrow/stream/345428-mathlib-reviewers/topic/lean4checker
 
-      - name: Post comments for lean-pr-testing branch
+      - name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
         if: always()
         env:
           TOKEN: ${{ secrets.LEAN_PR_TESTING }}
@@ -275,7 +291,8 @@ jobs:
           LINT_OUTCOME: ${{ steps.lint.outcome }}
           TEST_OUTCOME: ${{ steps.test.outcome }}
         run: |
-          scripts/lean-pr-testing-comments.sh
+          scripts/lean-pr-testing-comments.sh lean
+          scripts/lean-pr-testing-comments.sh batteries
 
   final:
     name: Post-CI jobJOB_NAME
@@ -305,7 +322,7 @@ jobs:
 
       - if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
         name: If `auto-merge-after-CI` is present, add a `bors merge` comment.
-        uses: GrantBirki/comment@v2.0.1
+        uses: GrantBirki/comment@v2
         with:
           token: ${{ secrets.AUTO_MERGE_TOKEN }}
           issue-number: ${{ steps.PR.outputs.number }}

.github/workflows/PR_summary.yml

@@ -55,12 +55,27 @@ jobs:
         PR="${{ github.event.pull_request.number }}"
         title="### PR summary"
 
+        graphAndHighPercentReports=$(python ./scripts/import-graph-report.py base.json head.json changed_files.txt)
+
         ## Import count comment
         importCount=$(
-          python ./scripts/import-graph-report.py base.json head.json changed_files.txt
+          printf '%s\n' "${graphAndHighPercentReports}" | sed '/^Import changes exceeding/Q'
           ./scripts/import_trans_difference.sh
         )
 
+        ## High percentage imports
+        high_percentages=$(
+          printf '%s\n' "${graphAndHighPercentReports}" | sed -n '/^Import changes exceeding/,$p'
+        )
+        # if there are files with large increase in transitive imports, then we add the `large-import` label
+        if [ -n "${high_percentages}" ]
+        then
+          high_percentages=$'\n\n'"${high_percentages}"
+          gh pr edit "${PR}" --add-label large-import
+        else # otherwise, we remove the label
+          gh pr edit "${PR}" --remove-label large-import
+        fi
+
         if [ "$(printf '%s' "${importCount}" | wc -l)" -gt 12 ]
         then
           importCount="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "#### Import changes for modified files" "${importCount}")"
@@ -80,6 +95,6 @@ jobs:
         currentHash="$(git rev-parse HEAD)"
         hashURL="https://github.com/${{ github.repository }}/pull/${{ github.event.pull_request.number }}/commits/${currentHash}"
 
-        message="$(printf '%s [%s](%s)\n\n%s\n\n---\n\n%s\n' "${title}" "$(git rev-parse --short HEAD)" "${hashURL}" "${importCount}" "${declDiff}")"
+        message="$(printf '%s [%s](%s)%s\n\n%s\n\n---\n\n%s\n' "${title}" "$(git rev-parse --short HEAD)" "${hashURL}" "${high_percentages}" "${importCount}" "${declDiff}")"
 
         ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}"

.github/workflows/actionlint.yml

@@ -1,10 +1,5 @@
-name: Actionlint
+name: Check workflows
 on:
-  push:
-    branches:
-      - 'master'
-    paths:
-      - '.github/**'
   pull_request:
     paths:
       - '.github/**'
@@ -14,7 +9,28 @@ jobs:
   actionlint:
     runs-on: ubuntu-latest
     steps:
-    - name: Checkout
-      uses: actions/checkout@v4
-    - name: actionlint
-      uses: raven-actions/actionlint@v1
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: suggester / actionlint
+        uses: reviewdog/action-actionlint@v1
+        with:
+          tool_name: actionlint
+          fail_on_error: true
+
+  check_build_yml:
+    name: check workflows generated by build.in.yml
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: update workflows
+        run: |
+          cd .github/workflows/
+          ./mk_build_yml.sh
+
+      - name: suggester / build.in.yml
+        uses: reviewdog/action-suggester@v1
+        with:
+          tool_name: mk_build_yml.sh
+          fail_on_error: true

.github/workflows/add_label_from_comment.yml

@@ -7,50 +7,15 @@ on:
 jobs:
   add_ready_to_merge_label:
     name: Add ready-to-merge label
-    if: (toJSON(github.event.issue.pull_request) != 'null') && (startsWith(github.event.comment.body, 'bors r+') || contains(toJSON(github.event.comment.body), '\r\nbors r+') || startsWith(github.event.comment.body, 'bors merge') || contains(toJSON(github.event.comment.body), '\r\nbors merge'))
+    if: github.event.issue.pull_request && (startsWith(github.event.comment.body, 'bors r+') || contains(toJSON(github.event.comment.body), '\nbors r+') || startsWith(github.event.comment.body, 'bors merge') || contains(toJSON(github.event.comment.body), '\nbors merge'))
     runs-on: ubuntu-latest
     steps:
-      - uses: octokit/request-action@v2.x
-        name: Get PR head
-        id: get_pr_head
+      - id: user_permission
+        uses: actions-cool/check-user-permission@v2
         with:
-          route: GET /repos/:repository/pulls/:pull_number
-          repository: ${{ github.repository }}
-          pull_number: ${{ github.event.issue.number }}
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-
-      # Parse steps.get_pr_head.outputs.data, since it is a string
-      - id: parse_pr_head
-        name: Parse PR head
-        uses: gr2m/get-json-paths-action@v1.x
-        with:
-          json: ${{ steps.get_pr_head.outputs.data }}
-          head_user: 'head.user.login'
-
-      # we skip the rest if this PR is from a fork,
-      # since the GITHUB_TOKEN doesn't have write perms
-      - if: steps.parse_pr_head.outputs.head_user == 'leanprover-community'
-        uses: octokit/request-action@v2.x
-        name: Get comment author
-        id: get_user
-        with:
-          route: GET /repos/:repository/collaborators/:username/permission
-          repository: ${{ github.repository }}
-          username: ${{ github.event.comment.user.login }}
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-
-      # Parse steps.get_user.outputs.data, since it is a string
-      - if: steps.parse_pr_head.outputs.head_user == 'leanprover-community'
-        id: parse_user
-        name: Parse comment author permission
-        uses: gr2m/get-json-paths-action@v1.x
-        with:
-          json: ${{ steps.get_user.outputs.data }}
-          permission: 'permission'
+          require: 'admin'
 
-      - if: (steps.parse_pr_head.outputs.head_user == 'leanprover-community') && (steps.parse_user.outputs.permission == 'admin')
+      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.comment.user.login == 'leanprover-community-mathlib4-bot') || (github.event.comment.user.login == 'leanprover-community-bot-assistant')
         uses: octokit/request-action@v2.x
         id: add_label
         name: Add label
@@ -62,7 +27,7 @@ jobs:
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
 
-      - if: (steps.parse_pr_head.outputs.head_user == 'leanprover-community') && (steps.parse_user.outputs.permission == 'admin')
+      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.comment.user.login == 'leanprover-community-mathlib4-bot') || (github.event.comment.user.login == 'leanprover-community-bot-assistant')
         id: remove_labels
         name: Remove "awaiting-author"
         # we use curl rather than octokit/request-action so that the job won't fail
@@ -74,50 +39,15 @@ jobs:
 
   add_delegated_label:
     name: Add delegated label
-    if: (toJSON(github.event.issue.pull_request) != 'null') && (startsWith(github.event.comment.body, 'bors d') || contains(toJSON(github.event.comment.body), '\r\nbors d'))
+    if: github.event.issue.pull_request && (startsWith(github.event.comment.body, 'bors d') || contains(toJSON(github.event.comment.body), '\nbors d'))
     runs-on: ubuntu-latest
     steps:
-      - uses: octokit/request-action@v2.x
-        name: Get PR head
-        id: get_pr_head
-        with:
-          route: GET /repos/:repository/pulls/:pull_number
-          repository: ${{ github.repository }}
-          pull_number: ${{ github.event.issue.number }}
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-
-      # Parse steps.get_pr_head.outputs.data, since it is a string
-      - id: parse_pr_head
-        name: Parse PR head
-        uses: gr2m/get-json-paths-action@v1.x
-        with:
-          json: ${{ steps.get_pr_head.outputs.data }}
-          head_user: 'head.user.login'
-
-      # we skip the rest if this PR is from a fork,
-      # since the GITHUB_TOKEN doesn't have write perms
-      - if: steps.parse_pr_head.outputs.head_user == 'leanprover-community'
-        uses: octokit/request-action@v2.x
-        name: Get comment author
-        id: get_user
-        with:
-          route: GET /repos/:repository/collaborators/:username/permission
-          repository: ${{ github.repository }}
-          username: ${{ github.event.comment.user.login }}
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-
-      # Parse steps.get_user.outputs.data, since it is a string
-      - if: steps.parse_pr_head.outputs.head_user == 'leanprover-community'
-        id: parse_user
-        name: Parse comment author permission
-        uses: gr2m/get-json-paths-action@v1.x
+      - id: user_permission
+        uses: actions-cool/check-user-permission@v2
         with:
-          json: ${{ steps.get_user.outputs.data }}
-          permission: 'permission'
+          require: 'admin'
 
-      - if: (steps.parse_pr_head.outputs.head_user == 'leanprover-community') && (steps.parse_user.outputs.permission == 'admin')
+      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.comment.user.login == 'leanprover-community-mathlib4-bot') || (github.event.comment.user.login == 'leanprover-community-bot-assistant')
         uses: octokit/request-action@v2.x
         id: add_label
         name: Add label

.github/workflows/add_label_from_diff.yaml

@@ -0,0 +1,42 @@
+name: Autolabel PRs
+
+on:
+  pull_request:
+    types: [opened]
+  push:
+    paths:
+      - scripts/autolabel.lean
+      - .github/workflows/add_label_from_diff.yaml
+
+jobs:
+  add_topic_label:
+    name: Add topic label
+    runs-on: ubuntu-latest
+    # Don't run on forks, where we wouldn't have permissions to add the label anyway.
+    if: github.repository == 'leanprover-community/mathlib4'
+    permissions:
+      issues: write
+      checks: write
+      pull-requests: write
+      contents: read
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+      - name: install elan
+        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}"
+      - name: lake exe autolabel
+        run: |
+          # the checkout dance, to avoid a detached head
+          git checkout master
+          git checkout -
+          lake exe autolabel "$NUMBER"
+        env:
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          GH_REPO: ${{ github.repository }}
+          NUMBER: ${{ github.event.number }}