Merge branch 'leanprover-community:master' into freeprob

Author: CoolRmal

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

@@ -0,0 +1,75 @@
+# get-mathlib-ci
+
+This action is the source of truth for how workflows in this repository check out
+`leanprover-community/mathlib-ci`.
+
+## Policy
+
+Any workflow that needs `mathlib-ci` should use this action instead of writing its
+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. This is auto-updated regularly by the
+[`update_dependencies.yml` workflow](../../workflows/update_dependencies.yml).
+
+## Why
+
+- Keep the pinned `mathlib-ci` ref in one place.
+- Avoid drift and copy/paste mistakes across many workflows.
+- Make ref bumps a one-file update.
+
+## Usage
+
+In workflows, check out this repository's actions from the running workflow commit,
+then use the local action:
+
+```yaml
+- name: Checkout local actions
+  uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+  with:
+    ref: ${{ github.workflow_sha }}
+    fetch-depth: 1
+    sparse-checkout: .github/actions
+    path: workflow-actions
+
+- name: Get mathlib-ci
+  uses: ./workflow-actions/.github/actions/get-mathlib-ci
+```
+
+Override the ref only when needed:
+
+```yaml
+- name: Get mathlib-ci
+  uses: ./workflow-actions/.github/actions/get-mathlib-ci
+  with:
+    ref: master
+```
+
+## Outputs
+
+This action also exposes values that later workflow steps can reuse:
+
+- `ref`: the effective `mathlib-ci` ref that was checked out. If the workflow did
+  not pass `with.ref`, this is the action's default pinned commit.
+- `path`: the checkout path used for `mathlib-ci`.
+- `scripts_dir`: the absolute path to the checked out `scripts` directory.
+
+The action also exports these environment variables for subsequent steps:
+
+- `CI_CHECKOUT_PATH`: the absolute path to the checked out `mathlib-ci` repository.
+- `CI_SCRIPTS_DIR`: the absolute path to the checked out `mathlib-ci/scripts` directory.
+
+If a workflow needs to refer to the exact resolved `mathlib-ci` ref later, use the
+action output instead of duplicating the pinned SHA in the workflow:
+
+```yaml
+- name: Get mathlib-ci
+  id: get_mathlib_ci
+  uses: ./workflow-actions/.github/actions/get-mathlib-ci
+
+- name: Use resolved ref
+  run: |
+    echo "Resolved ref: ${{ steps.get_mathlib_ci.outputs.ref }}"
+    echo "Scripts dir: ${{ steps.get_mathlib_ci.outputs.scripts_dir }}"
+    echo "Raw URL: https://raw.githubusercontent.com/leanprover-community/mathlib-ci/${{ steps.get_mathlib_ci.outputs.ref }}/scripts/nightly/create-adaptation-pr.sh"
+```

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

@@ -0,0 +1,52 @@
+# Source of truth for `mathlib-ci` checkout settings in this repository.
+# Workflows should use this action instead of duplicating the checkout block
+# and hardcoded ref in multiple places.
+name: Get mathlib-ci
+description: Checkout leanprover-community/mathlib-ci at a shared ref.
+inputs:
+  ref:
+    description: Git ref (branch, tag, or SHA) for mathlib-ci.
+    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
+    # This is also updated automatically by .github/workflows/update_dependencies.yml
+    default: e7a159e9a129f92fd07e6852a742485798678473
+  path:
+    description: Checkout destination path.
+    required: false
+    default: ci-tools
+  fetch-depth:
+    description: Number of commits to fetch.
+    required: false
+    default: '1'
+outputs:
+  ref:
+    description: Effective ref used for the checkout.
+    value: ${{ inputs.ref }}
+  path:
+    description: Checkout path used.
+    value: ${{ inputs.path }}
+  scripts_dir:
+    description: Absolute path to the scripts directory.
+    value: ${{ steps.paths.outputs.scripts_dir }}
+runs:
+  using: composite
+  steps:
+    - name: Get mathlib-ci
+      uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      with:
+        repository: leanprover-community/mathlib-ci
+        ref: ${{ inputs.ref }}
+        fetch-depth: ${{ inputs.fetch-depth }}
+        path: ${{ inputs.path }}
+
+    - name: Setup CI Scripts Paths
+      id: paths
+      shell: bash
+      run: |
+        checkout_path="${GITHUB_WORKSPACE}/${{ inputs.path }}"
+        scripts_dir="${checkout_path}/scripts"
+        echo "checkout_path=${checkout_path}" >> "$GITHUB_OUTPUT"
+        echo "scripts_dir=${scripts_dir}" >> "$GITHUB_OUTPUT"
+        echo "CI_CHECKOUT_PATH=${checkout_path}" >> "$GITHUB_ENV"
+        echo "CI_SCRIPTS_DIR=${scripts_dir}" >> "$GITHUB_ENV"

.github/workflows/PR_summary.yml

@@ -22,14 +22,18 @@ jobs:
         ref: ${{ github.event.pull_request.head.sha }}
         fetch-depth: 0
         path: pr-branch
+        # Untrusted (potentially fork) checkout: don't persist the GITHUB_TOKEN into its .git/config.
+        persist-credentials: false
 
-    # Checkout the master branch into a subdirectory
-    - name: Checkout master branch
+    - name: Checkout local actions
       uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
       with:
-        # When testing the scripts, comment out the "ref: master"
-        ref: master
-        path: master-branch
+        ref: ${{ github.workflow_sha }}
+        fetch-depth: 1
+        sparse-checkout: .github/actions
+        path: workflow-actions
+    - name: Get mathlib-ci
+      uses: ./workflow-actions/.github/actions/get-mathlib-ci
 
     - name: Update the merge-conflict label
       run: |
@@ -79,6 +83,10 @@ jobs:
         echo "Saving the changed files to 'changed_files.txt'..."
         git diff --name-only origin/${{ github.base_ref }}... | tee changed_files.txt
 
+        # Get all newly added files.
+        echo "Checking for added files..."
+        git diff --name-only --diff-filter A origin/${{ github.base_ref }}... | tee added_files.txt
+
         # Get all files which were removed or renamed.
         echo "Checking for removed files..."
 
@@ -152,13 +160,13 @@ jobs:
         printf 'currentHash=%s\n' "${currentHash}"
 
         echo "Compute the counts for the HEAD of the PR"
-        python ../master-branch/scripts/count-trans-deps.py "Mathlib/" > head.json
+        python "${CI_SCRIPTS_DIR}/pr_summary/count-trans-deps.py" "Mathlib/" > head.json
 
         # Checkout the merge base
         git checkout "$(git merge-base master ${{ github.event.pull_request.head.sha }})"
 
         echo "Compute the counts for the merge base"
-        python ../master-branch/scripts/count-trans-deps.py "Mathlib/" > base.json
+        python "${CI_SCRIPTS_DIR}/pr_summary/count-trans-deps.py" "Mathlib/" > base.json
 
         # switch back to the current branch: the `declarations_diff` script should be here
         git checkout "${currentHash}" --
@@ -173,12 +181,12 @@ jobs:
         PR="${{ github.event.pull_request.number }}"
         title="### PR summary"
 
-        graphAndHighPercentReports=$(python ../master-branch/scripts/import-graph-report.py base.json head.json changed_files.txt)
+        graphAndHighPercentReports=$(python "${CI_SCRIPTS_DIR}/pr_summary/import-graph-report.py" base.json head.json changed_files.txt)
 
         echo "Produce import count comment"
         importCount=$(
           printf '%s\n' "${graphAndHighPercentReports}" | sed '/^Import changes exceeding/Q'
-          ../master-branch/scripts/import_trans_difference.sh
+          "${CI_SCRIPTS_DIR}/pr_summary/import_trans_difference.sh"
         )
 
         echo "Produce high percentage imports"
@@ -202,7 +210,7 @@ jobs:
         fi
 
         echo "Compute Declarations' diff comment"
-        declDiff=$(../master-branch/scripts/declarations_diff.sh)
+        declDiff=$("${CI_SCRIPTS_DIR}/pr_summary/declarations_diff.sh")
         if [ "$(printf '%s' "${declDiff}" | wc -l)" -gt 15 ]
         then
           declDiff="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "#### Declarations diff" "${declDiff}")"
@@ -214,10 +222,40 @@ jobs:
         printf 'hashURL: %s' "${hashURL}"
 
         echo "Compute technical debt changes"
-        techDebtVar="$(../master-branch/scripts/technical-debt-metrics.sh pr_summary)"
+        techDebtVar="$("${CI_SCRIPTS_DIR}/reporting/technical-debt-metrics.sh" pr_summary)"
+
+        echo "Compute documentation reminder"
+        workflowFilesChanged="$(grep '^\.github/workflows/' changed_files.txt || true)"
+        if [ -n "${workflowFilesChanged}" ]
+        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}")"
+        else
+          workflowDocsReminder=""
+        fi
+
+        echo "Compute scripts-location reminder"
+        scriptsFilesAdded="$(grep '^scripts/' added_files.txt || true)"
+        if [ -n "${scriptsFilesAdded}" ]
+        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\`](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
 
         # 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}" > please_merge_master.md
+        if [ -n "${workflowDocsReminder}" ]
+        then
+          printf '\n\n---\n\n%s\n' "${workflowDocsReminder}" >> please_merge_master.md
+        fi
+        if [ -n "${scriptsLocationReminder}" ]
+        then
+          printf '\n\n---\n\n%s\n' "${scriptsLocationReminder}" >> please_merge_master.md
+        fi
 
         echo "Include any errors about removed or renamed files without deprecation,"
         echo "as well as errors about extraneous deprecated_module additions."
@@ -233,7 +271,7 @@ jobs:
         fi
 
         cat please_merge_master.md
-        ../master-branch/scripts/update_PR_comment.sh please_merge_master.md "${title}" "${PR}"
+        "${CI_SCRIPTS_DIR}/pr_summary/update_PR_comment.sh" please_merge_master.md "${title}" "${PR}"
 
     - name: Update the file-removed label
       run: |

.github/workflows/actionlint.yml

@@ -3,7 +3,6 @@ on:
   pull_request:
     paths:
       - '.github/**'
-  merge_group:
 
 jobs:
   actionlint:
@@ -13,7 +12,19 @@ jobs:
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
       - name: suggester / actionlint
-        uses: reviewdog/action-actionlint@e58ee9d111489c31395fbe4857b0be6e7635dbda # v1.70.0
+        uses: reviewdog/action-actionlint@6fb7acc99f4a1008869fa8a0f09cfca740837d9d # v1.72.0
         with:
           tool_name: actionlint
-          fail_level: error
+          fail_level: any
+
+  ensure-sha-pinned-actions:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+
+      # Using our fork's PR branch until upstream merges the improved error reporting:
+      # https://github.com/zgosalvez/github-actions-ensure-sha-pinned-actions/pull/288
+      # TODO: Update to upstream release once merged.
+      - name: Ensure all actions are pinned to SHA
+        uses: kim-em/github-actions-ensure-sha-pinned-actions@00f51cdb5bbc21f5bc873ef3a2dceef45df213af # improve-error-reporting

.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
@@ -43,6 +43,8 @@ jobs:
         ref: ${{ github.event.pull_request.head.sha || github.sha }}
         fetch-depth: 0
         path: pr-branch
+        # Untrusted (potentially fork) checkout: don't persist the GITHUB_TOKEN into its .git/config.
+        persist-credentials: false
     - name: Run autolabel
       working-directory: pr-branch
       run: |

.github/workflows/bors.yml

@@ -15,6 +15,7 @@ concurrency:
 # Limit permissions for GITHUB_TOKEN for the entire workflow
 permissions:
   contents: read
+  id-token: write
   pull-requests: write  # Only allow PR comments/labels
   # All other permissions are implicitly 'none'
 
@@ -26,9 +27,12 @@ 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 }}
-      # We don't wan't 'bors try' runs to compete with merge-candidates, so we pool trying with PR runs
+      # We don't want 'bors try' runs to compete with merge-candidates, so we pool trying with PR runs
       runs_on: ${{ github.ref_name == 'trying' && 'pr' || 'bors' }}
     secrets: inherit

.github/workflows/bot_fix_style.yaml

@@ -12,6 +12,14 @@ on:
     # triggers on a review comment
     types: [created, edited]
 
+# `lint-style-action` in `fix` mode pushes a style-fix commit and reacts/comments
+# on the PR. Grant exactly those scopes rather than inheriting the default token
+# permissions; all other scopes are implicitly 'none'.
+permissions:
+  contents: write       # push the style-fix commit to the PR branch
+  pull-requests: write  # add the bot's reaction/comment
+  issues: write         # PR comment reactions go through the issues API
+
 jobs:
   fix_style:
     # we set some variables. The ones of the form `${{ X }}${{ Y }}` are typically not

.github/workflows/build.yml

@@ -12,7 +12,6 @@ on:
       - 'trying'
       # ignore branches meant for experiments
       - 'ci-dev/**'
-  merge_group:
 
 concurrency:
   # label each workflow run; only the latest with each label will run
@@ -24,6 +23,7 @@ concurrency:
 # Limit permissions for GITHUB_TOKEN for the entire workflow
 permissions:
   contents: read
+  id-token: write
   pull-requests: write  # Only allow PR comments/labels
   # All other permissions are implicitly 'none'
 
@@ -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

@@ -24,6 +24,7 @@ concurrency:
 # Limit permissions for GITHUB_TOKEN for the entire workflow
 permissions:
   contents: read
+  id-token: write
   pull-requests: write  # Only allow PR comments/labels
   # All other permissions are implicitly 'none'
 
@@ -35,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