Merge branch 'master' into fae_uniformConvex_filter

Author: faenuccio

.github/actions/get-mathlib-ci/README.md

@@ -9,7 +9,8 @@ Any workflow that needs `mathlib-ci` should use this action instead of writing i
 own `actions/checkout` block for `leanprover-community/mathlib-ci`.
 
 The default `ref` in [`action.yml`](./action.yml) is the single canonical pinned
-`mathlib-ci` commit for this repository.
+`mathlib-ci` commit for this repository. This is auto-updated regularly by the
+[`update_dependencies.yml` workflow](../../workflows/update_dependencies.yml).
 
 ## Why
 

.github/actions/get-mathlib-ci/action.yml

@@ -9,7 +9,8 @@ inputs:
     required: false
     # Default pinned commit used by workflows unless they explicitly override.
     # Update this ref as needed to pick up changes to mathlib-ci scripts
-    default: 261ca4c0c6bd3267e4846ef9fdd676afab9fef4e
+    # This is also updated automatically by .github/workflows/update_dependencies.yml
+    default: 99a8d566da03485d4e08fa0a85e38200f2d4e964
   path:
     description: Checkout destination path.
     required: false

.github/workflows/PR_summary.yml

@@ -228,7 +228,7 @@ jobs:
         then
           # Format each changed workflow path as a Markdown bullet: "- `path`"
           workflowFilesChangedMarkdown="$(sed "s|^|- \`|; s|\$|\`|" <<< "${workflowFilesChanged}")"
-          workflowDocsReminder="$(printf "### Workflow documentation reminder\nThis PR modifies files under \`.github/workflows/\`.\nPlease update \`docs/workflows.md\` if the workflow inventory, triggers, or behavior changed.\n\nModified workflow files:\n%s\n" "${workflowFilesChangedMarkdown}")"
+          workflowDocsReminder="$(printf "### ⚠️ Workflow documentation reminder\nThis PR modifies files under \`.github/workflows/\`.\nPlease update \`docs/workflows.md\` if the workflow inventory, triggers, or behavior changed.\n\nModified workflow files:\n%s\n" "${workflowFilesChangedMarkdown}")"
         else
           workflowDocsReminder=""
         fi
@@ -239,7 +239,7 @@ jobs:
         then
           # Format each added scripts path as a Markdown bullet: "- `path`"
           scriptsFilesAddedMarkdown="$(sed "s|^|- \`|; s|\$|\`|" <<< "${scriptsFilesAdded}")"
-          scriptsLocationReminder="$(printf "### Scripts folder reminder\nThis PR adds files under \`scripts/\`.\nPlease consider whether each added script belongs in this repository or in \`leanprover-community/mathlib-ci\`.\n\nAdded scripts files:\n%s\n" "${scriptsFilesAddedMarkdown}")"
+          scriptsLocationReminder="$(printf "### ⚠️ Scripts folder reminder\nThis PR adds files under \`scripts/\`.\nPlease consider whether each added script belongs in this repository or in [\`leanprover-community/mathlib-ci\`](https://github.com/leanprover-community/mathlib-ci).\n\nA script belongs in **\`mathlib-ci\`** if it is a CI automation script that interacts with GitHub (e.g. managing labels, posting comments, triggering bots), runs from a trusted external checkout in CI, or requires access to secrets.\n\nA script belongs in **this repository** (\`scripts/\`) if it is a developer or maintainer tool to be run locally, a code maintenance or analysis utility, a style linting tool, or a data file used by the library's own linters.\n\nSee the [\`mathlib-ci\` README](https://github.com/leanprover-community/mathlib-ci) for more details.\n\nAdded scripts files:\n%s\n" "${scriptsFilesAddedMarkdown}")"
         else
           scriptsLocationReminder=""
         fi

.github/workflows/actionlint.yml

@@ -12,7 +12,7 @@ jobs:
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
       - name: suggester / actionlint
-        uses: reviewdog/action-actionlint@0d952c597ef8459f634d7145b0b044a9699e5e43 # v1.71.0
+        uses: reviewdog/action-actionlint@6fb7acc99f4a1008869fa8a0f09cfca740837d9d # v1.72.0
         with:
           tool_name: actionlint
           fail_level: any

.github/workflows/add_label_from_diff.yaml

@@ -27,7 +27,7 @@ jobs:
         ref: master
         path: tools
     - name: Configure Lean
-      uses: leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4.0
+      uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0
       with:
         auto-config: false
         use-github-cache: false

.github/workflows/bors.yml

@@ -27,6 +27,9 @@ jobs:
     with:
       concurrency_group: ${{ github.workflow }}-${{ github.ref }}-${{ github.run_id }}
       pr_branch_ref: ${{ github.sha }}
+      # Use the MASTER cache key only when merging into mathlib4 (staging branch);
+      # 'bors try' runs (trying branch) and nightly-testing use NON_MASTER
+      cache_application_id: ${{ github.ref_name == 'staging' && github.repository == 'leanprover-community/mathlib4' && vars.CACHE_MASTER_WRITER_AZURE_APP_ID || vars.CACHE_NON_MASTER_WRITER_AZURE_APP_ID }}
       # bors runs should build the tools from their commit-under-test: after all, we are trying to
       # test 'what would happen if this was merged', so we need to use the 'would-be-post-merge' tools
       tools_branch_ref: ${{ github.sha }}

.github/workflows/build.yml

@@ -35,5 +35,7 @@ jobs:
     with:
       concurrency_group: ${{ github.workflow }}-${{ github.ref }}-${{ (github.event_name == 'push' && github.ref == 'refs/heads/master' && github.run_id) || '' }}
       pr_branch_ref: ${{ github.sha }}
+      # Use the MASTER cache key only on mathlib4/master; nightly-testing and other branches use NON_MASTER
+      cache_application_id: ${{ github.repository == 'leanprover-community/mathlib4' && github.ref == 'refs/heads/master' && vars.CACHE_MASTER_WRITER_AZURE_APP_ID || vars.CACHE_NON_MASTER_WRITER_AZURE_APP_ID }}
       runs_on: pr
     secrets: inherit

.github/workflows/build_fork.yml

@@ -36,5 +36,6 @@ jobs:
     with:
       concurrency_group: ${{ github.workflow }}-${{ github.event.pull_request.number }}
       pr_branch_ref: ${{ github.event.pull_request.head.sha }}
+      cache_application_id: ${{ vars.CACHE_NON_MASTER_WRITER_AZURE_APP_ID }}
       runs_on: pr
     secrets: inherit