Merge remote-tracking branch 'upstream/master' into infinite-prod-with-zero

Author: b-mehta

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

@@ -0,0 +1,74 @@
+# 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.
+
+## 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,51 @@
+# 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
+    default: 261ca4c0c6bd3267e4846ef9fdd676afab9fef4e
+  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

@@ -23,16 +23,15 @@ jobs:
         fetch-depth: 0
         path: pr-branch
 
-    - name: Checkout mathlib-ci
+    - name: Checkout local actions
       uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
       with:
-        repository: leanprover-community/mathlib-ci
-        ref: 4af75ac0b0d1aaf38d4546a779bc5c68b4d75069
+        ref: ${{ github.workflow_sha }}
         fetch-depth: 1
-        path: ci-tools
-
-    - name: Set up CI scripts paths
-      uses: ./ci-tools/.github/actions/setup-ci-scripts
+        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: |

.github/workflows/actionlint.yml

@@ -3,7 +3,6 @@ on:
   pull_request:
     paths:
       - '.github/**'
-  merge_group:
 
 jobs:
   actionlint:
@@ -13,7 +12,7 @@ jobs:
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
       - name: suggester / actionlint
-        uses: reviewdog/action-actionlint@e58ee9d111489c31395fbe4857b0be6e7635dbda # v1.70.0
+        uses: reviewdog/action-actionlint@0d952c597ef8459f634d7145b0b044a9699e5e43 # v1.71.0
         with:
           tool_name: actionlint
           fail_level: any

.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'
 

.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'
 

.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'
 

.github/workflows/build_template.yml

@@ -23,7 +23,7 @@ on:
       mathlib_ci_ref:
         type: string
         required: false
-        default: 4af75ac0b0d1aaf38d4546a779bc5c68b4d75069
+        default: ''
 
 env:
   # Disable Lake's automatic fetching of cloud builds.
@@ -95,16 +95,27 @@ jobs:
           ref: ${{ inputs.tools_branch_ref != '' && inputs.tools_branch_ref || (github.repository == 'leanprover-community/mathlib4-nightly-testing' && 'nightly-testing-green' || 'master') }}
           path: tools-branch
 
-      - name: Checkout mathlib-ci
+      - name: Checkout local actions
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
         with:
-          repository: leanprover-community/mathlib-ci
-          ref: ${{ inputs.mathlib_ci_ref }}
+          ref: ${{ github.workflow_sha }}
           fetch-depth: 1
-          path: ci-tools
-
-      - name: Set up CI scripts paths
-        uses: ./ci-tools/.github/actions/setup-ci-scripts
+          sparse-checkout: .github/actions
+          path: workflow-actions
+
+      # We need to 'duplicate' this step below because GitHub Actions does not let a `uses:` step
+      # conditionally omit a single `with:` key, and passing `ref: ''` would override
+      # the composite action's default to the empty string instead of falling back to it
+      # Note only one of the two below will actually run in any given run
+      - name: Get mathlib-ci
+        if: ${{ inputs.mathlib_ci_ref == '' }}
+        uses: ./workflow-actions/.github/actions/get-mathlib-ci
+
+      - name: Get mathlib-ci
+        if: ${{ inputs.mathlib_ci_ref != '' }}
+        uses: ./workflow-actions/.github/actions/get-mathlib-ci
+        with:
+          ref: ${{ inputs.mathlib_ci_ref }}
 
       # Checkout the PR branch into a subdirectory
       - name: Checkout PR branch
@@ -193,32 +204,6 @@ jobs:
           ls .lake/build/bin/check-yaml
           ls .lake/packages/importGraph/.lake/build/bin/graph
 
-      - name: cleanup .cache/mathlib
-        # This needs write access to .cache/mathlib, so can't be run inside landrun.
-        # However it is only using the `tools` version of `cache`, so is safe to run outside landrun.
-        shell: bash
-        run: |
-          # Define the cache directory path
-          CACHE_DIR="$HOME/.cache/mathlib"
-
-          # Check if directory exists
-          if [ ! -d "$CACHE_DIR" ]; then
-            echo "::warning::Cache directory does not exist: $CACHE_DIR"
-            exit 0
-          fi
-
-          # Calculate directory size in bytes
-          DIR_SIZE=$(du -sb "$CACHE_DIR" | cut -f1)
-          printf 'Cache size (in bytes): %s\n' "$DIR_SIZE"
-
-          # Check if size exceeds 10GB
-          if [ "$DIR_SIZE" -gt "10737418240" ]; then
-            echo "Cache size exceeds threshold, running lake exe cache clean"
-            # We use the tools-branch version of `cache`.
-            cd tools-branch
-            lake exe cache clean
-          fi
-
       - name: download dependencies
         # We need network access to download dependencies
         # We run this inside landrun, but restrict disk access.
@@ -489,7 +474,7 @@ jobs:
 
       - name: upload cache staging artifact
         if: ${{ always() && steps.cache_staging_check.outputs.has_files == 'true' }}
-        uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6.0.0
+        uses: actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7.0.0
         with:
           name: cache-staging
           path: cache-staging/
@@ -583,20 +568,6 @@ jobs:
             exit $status
           done
 
-      # We need to separate this step from the previous script because it needs to run outside of landrun
-      - name: kill stray runLinter processes
-        if: ${{ steps.lint.outcome == 'failure' }}
-        continue-on-error: true
-        shell: bash
-        run: |
-          echo "Checking for runLinter processes..."
-          if pgrep -af runLinter; then
-            echo "Killing runLinter processes..."
-            pkill -f runLinter || true
-          else
-            echo "No stray runLinter processes found."
-          fi
-
       - name: end gh-problem-match-wrap for shake and lint steps
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
         with:
@@ -685,7 +656,7 @@ jobs:
           echo "CACHE_BIN=$CACHE_BIN" >> "$GITHUB_ENV"
 
       - name: Download cache staging artifact
-        uses: actions/download-artifact@37930b1c2abaa49bbe596cd826c3c89aef350131 # v7.0.0
+        uses: actions/download-artifact@70fc10c6e5e1ce46ad2ea6f2b72d43f7d47b13c3 # v8.0.0
         with:
           name: cache-staging
           path: cache-staging
@@ -756,7 +727,7 @@ jobs:
           lake exe graph
 
       - name: upload the import graph
-        uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6.0.0
+        uses: actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7.0.0
         with:
           name: import-graph
           path: import_graph.dot
@@ -801,10 +772,13 @@ jobs:
     steps:
       - name: Generate auto merge app token
         id: auto-merge-app-token
-        uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
+        uses: leanprover-community/mathlib-ci/.github/actions/azure-create-github-app-token@3bb576208589a435eeaeac9b144a1b7c3e948760
         with:
           app-id: ${{ secrets.MATHLIB_AUTO_MERGE_APP_ID }}
-          private-key: ${{ secrets.MATHLIB_AUTO_MERGE_PRIVATE_KEY }}
+          key-vault-name: ${{ vars.MATHLIB_AZ_KEY_VAULT_NAME }}
+          key-name: mathlib-auto-merge-app-pk
+          azure-client-id: ${{ vars.GH_APP_AZURE_CLIENT_ID_CI_AUTO_MERGE }}
+          azure-tenant-id: ${{ secrets.LPC_AZ_TENANT_ID }}
 
       - id: PR_from_push
         uses: 8BitJonny/gh-get-current-pr@4056877062a1f3b624d5d4c2bedefa9cf51435c9 # 4.0.0
@@ -916,7 +890,7 @@ jobs:
         name: If `auto-merge-after-CI` is present, add a `bors merge` comment.
         uses: GrantBirki/comment@608e41b19bc973020ec0e189ebfdae935d7fe0cc # v2.1.1
         with:
-          # The create-github-app-token README states that this token is masked and will not be logged accidentally.
+          # This token is masked by the token minting action and will not be logged accidentally.
           token: ${{ steps.auto-merge-app-token.outputs.token }}
           issue-number: ${{ steps.PR.outputs.number }}
           body: |

.github/workflows/ci_dev.yml

@@ -27,6 +27,7 @@ on:
 # Limit permissions for GITHUB_TOKEN for the entire workflow
 permissions:
   contents: read
+  id-token: write
   # By default let's remove this permission (which is present in the other build pipelines)
   # from the CI experimentation runs to avoid unwitting side effects
   # pull-requests: write

.github/workflows/commit_verification.yml

@@ -40,16 +40,15 @@ jobs:
           ref: ${{ github.event.pull_request.head.sha }}
           # Fetch full history to access all PR commits
           fetch-depth: 0
-      - name: Checkout mathlib-ci
+      - name: Checkout local actions
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
         with:
-          repository: leanprover-community/mathlib-ci
-          ref: 4af75ac0b0d1aaf38d4546a779bc5c68b4d75069
+          ref: ${{ github.workflow_sha }}
           fetch-depth: 1
-          path: ci-tools
-
-      - name: Set up CI scripts paths
-        uses: ./ci-tools/.github/actions/setup-ci-scripts
+          sparse-checkout: .github/actions
+          path: workflow-actions
+      - name: Get mathlib-ci
+        uses: ./workflow-actions/.github/actions/get-mathlib-ci
       - name: Check for special commits
         id: check
         run: |