ci: auto-update mathlib-ci ref (#37493)

bryangingechen · bryangingechen · commit 6ef8cc273178 · 2026-04-02T23:42:31.000Z
This adds steps to `update_dependencies.yml` to keep the default `ref` in the `get-mathlib-ci` action up to date.

prepared with claude code
diff --git a/.github/actions/get-mathlib-ci/README.md b/.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
 
diff --git a/.github/actions/get-mathlib-ci/action.yml b/.github/actions/get-mathlib-ci/action.yml
@@ -9,6 +9,7 @@ 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
+    # This is also updated automatically by .github/workflows/update_dependencies.yml
     default: b6def9edd1c39de8602b8c177c66e9416e5dbc60
   path:
     description: Checkout destination path.
diff --git a/.github/workflows/update_dependencies.yml b/.github/workflows/update_dependencies.yml
@@ -71,6 +71,27 @@ jobs:
           prNumber: ${{ steps.PR.outputs.number }}
           prUrl: ${{ steps.PR.outputs.pr_url }}
 
+      - name: Get latest mathlib-ci SHA
+        if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') }}
+        id: mathlib-ci-sha
+        env:
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+        run: |
+          SHA=$(gh api repos/leanprover-community/mathlib-ci/commits/HEAD --jq '.sha')
+          echo "sha=$SHA" >> "$GITHUB_OUTPUT"
+
+      - name: Update mathlib-ci ref in get-mathlib-ci action
+        if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') }}
+        id: update-mathlib-ci-ref
+        run: |
+          sed -i "s|^\( *default: \)[0-9a-f]\{40\}|\1${{ steps.mathlib-ci-sha.outputs.sha }}|" \
+            .github/actions/get-mathlib-ci/action.yml
+          if git diff --quiet .github/actions/get-mathlib-ci/action.yml; then
+            echo "modified=false" >> "$GITHUB_OUTPUT"
+          else
+            echo "modified=true" >> "$GITHUB_OUTPUT"
+          fi
+
       - name: Update dependencies
         if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') }}
         run: lake update -v
@@ -116,6 +137,10 @@ jobs:
             create_pr=true
             echo "Differences found with lake-manifest.json on $BRANCH_NAME, need to run create-pull-request to update $BRANCH_NAME"
           fi
+          if [ "${{ steps.update-mathlib-ci-ref.outputs.modified }}" == "true" ]; then
+            create_pr=true
+            echo "mathlib-ci ref was updated, need to run create-pull-request"
+          fi
           # Otherwise, there's no reason to run create-pull-request
           echo "create_pr=$create_pr" >> "${GITHUB_OUTPUT}"
 
