Merge branch 'master' into tangentspace-elaborators

Author: grunweg

.github/workflows/PR_summary.yml

@@ -27,7 +27,7 @@ jobs:
       uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
       with:
         repository: leanprover-community/mathlib-ci
-        ref: 7355aeb4f32cb2a181d02abd7a9d6ab4fe033286
+        ref: 4af75ac0b0d1aaf38d4546a779bc5c68b4d75069
         fetch-depth: 1
         path: ci-tools
 

.github/workflows/build_template.yml

@@ -23,7 +23,7 @@ on:
       mathlib_ci_ref:
         type: string
         required: false
-        default: 7355aeb4f32cb2a181d02abd7a9d6ab4fe033286
+        default: 4af75ac0b0d1aaf38d4546a779bc5c68b4d75069
 
 env:
   # Disable Lake's automatic fetching of cloud builds.

.github/workflows/commit_verification.yml

@@ -44,7 +44,7 @@ jobs:
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
         with:
           repository: leanprover-community/mathlib-ci
-          ref: 7355aeb4f32cb2a181d02abd7a9d6ab4fe033286
+          ref: 4af75ac0b0d1aaf38d4546a779bc5c68b4d75069
           fetch-depth: 1
           path: ci-tools
 

.github/workflows/label_new_contributor.yml

@@ -104,7 +104,7 @@ jobs:
           header: 'New Contributor Welcome'
           message: |
             ## Welcome new contributor!
-            Thank you for contributing to Mathlib! If you haven't done so already, please review our [contribution guidelines](https://leanprover-community.github.io/contribute/index.html), as well as the [style guide](https://leanprover-community.github.io/contribute/style.html) and [naming conventions](https://leanprover-community.github.io/contribute/naming.html).
+            Thank you for contributing to Mathlib! If you haven't done so already, please review our [contribution guidelines](https://leanprover-community.github.io/contribute/index.html), as well as the [style guide](https://leanprover-community.github.io/contribute/style.html) and [naming conventions](https://leanprover-community.github.io/contribute/naming.html). In particular, we kindly remind contributors that we have [guidelines](https://leanprover-community.github.io/contribute/index.html#use-of-ai) regarding the use of AI when making pull requests.
 
             We use a [review queue](https://leanprover-community.github.io/queueboard/review_dashboard.html) to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the `awaiting-author` tag, or another reason described in the [Lifecycle of a PR](https://leanprover-community.github.io/contribute/index.html#lifecycle-of-a-pr). The review dashboard has [a dedicated webpage](https://leanprover-community.github.io/queueboard/on_the_queue.html?search=${{ github.event.pull_request.number }}) which shows whether your PR is on the review queue, and (if not), why.
 

.github/workflows/latest_import.yml

@@ -32,7 +32,7 @@ jobs:
       uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
       with:
         repository: leanprover-community/mathlib-ci
-        ref: 7355aeb4f32cb2a181d02abd7a9d6ab4fe033286
+        ref: 4af75ac0b0d1aaf38d4546a779bc5c68b4d75069
         fetch-depth: 1
         path: ci-tools
 

.github/workflows/long_file_report.yml

@@ -18,7 +18,7 @@ jobs:
       uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
       with:
         repository: leanprover-community/mathlib-ci
-        ref: 7355aeb4f32cb2a181d02abd7a9d6ab4fe033286
+        ref: 4af75ac0b0d1aaf38d4546a779bc5c68b4d75069
         fetch-depth: 1
         path: ci-tools
 

.github/workflows/maintainer_bors.yml

@@ -180,7 +180,7 @@ jobs:
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
         with:
           repository: leanprover-community/mathlib-ci
-          ref: 7355aeb4f32cb2a181d02abd7a9d6ab4fe033286
+          ref: 4af75ac0b0d1aaf38d4546a779bc5c68b4d75069
           fetch-depth: 1
           path: ci-tools
 

.github/workflows/maintainer_bors_wf_run.yml

@@ -122,7 +122,7 @@ jobs:
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
         with:
           repository: leanprover-community/mathlib-ci
-          ref: 7355aeb4f32cb2a181d02abd7a9d6ab4fe033286
+          ref: 4af75ac0b0d1aaf38d4546a779bc5c68b4d75069
           fetch-depth: 1
           path: ci-tools
 

.github/workflows/maintainer_merge.yml

@@ -31,9 +31,9 @@ jobs:
     name: Ping maintainers on Zulip
     runs-on: ubuntu-latest
     if: >- # crude check to skip running this on most reviews / comments
-      github.repository == 'leanprover-community/mathlib4' && 
+      github.repository == 'leanprover-community/mathlib4' &&
       (
-        contains(format('{0}{1}', github.event.comment.body, github.event.review.body), 'maintainer merge') || 
+        contains(format('{0}{1}', github.event.comment.body, github.event.review.body), 'maintainer merge') ||
         contains(format('{0}{1}', github.event.comment.body, github.event.review.body), 'maintainer delegate')
       )
     steps:
@@ -124,7 +124,7 @@ jobs:
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
         with:
           repository: leanprover-community/mathlib-ci
-          ref: 7355aeb4f32cb2a181d02abd7a9d6ab4fe033286
+          ref: 4af75ac0b0d1aaf38d4546a779bc5c68b4d75069
           fetch-depth: 1
           path: ci-tools
 

.github/workflows/maintainer_merge_wf_run.yml

@@ -90,7 +90,7 @@ jobs:
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
         with:
           repository: leanprover-community/mathlib-ci
-          ref: 7355aeb4f32cb2a181d02abd7a9d6ab4fe033286
+          ref: 4af75ac0b0d1aaf38d4546a779bc5c68b4d75069
           fetch-depth: 1
           path: ci-tools