chore: Bump mathlib dependency to 1d2ba2d

.github/workflows/lake-update.yml

@@ -11,7 +11,39 @@ permissions:
 
 jobs:
   bump:
-    uses: leanprover-community/downstream-reports/.github/workflows/bump-dependency-to-latest.yml@main
+    runs-on: ubuntu-latest
     permissions:
       contents: write
       pull-requests: write
+    steps:
+      - name: Generate app token
+        id: app-token
+        uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
+        with:
+          app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }}
+          private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }}
+
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+
+      - name: Bump to latest
+        id: bump
+        uses: leanprover-community/downstream-reports/.github/actions/bump-to-latest@main
+
+      - name: Open or update PR
+        id: open-pr
+        if: steps.bump.outputs.updated == 'true'
+        uses: leanprover-community/downstream-reports/.github/actions/open-bump-pr@main
+        with:
+          title: "chore: ${{ steps.bump.outputs.pr-title }}"
+          message:        ${{ steps.bump.outputs.bump-description }}
+          commit-message: ${{ steps.bump.outputs.commit-message }}
+          token:          ${{ steps.app-token.outputs.token }}
+          git-user-name:  mathlib-nightly-testing[bot]
+          git-user-email: mathlib-nightly-testing[bot]@users.noreply.github.com
+
+      - name: Enable auto-merge
+        if: steps.open-pr.outputs.pr-number != ''
+        env:
+          GH_TOKEN: ${{ steps.app-token.outputs.token }}
+        run: |
+          gh pr merge --auto --merge "${{ steps.open-pr.outputs.pr-number }}"

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5450b53e5ddc75d46418fabb605edbf36bd0beb6",
+   "rev": "1d2ba2d2aedb9065a4699cff0bfe8f0c3d3fb8d9",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "1d2ba2d2aedb9065a4699cff0bfe8f0c3d3fb8d9",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",

lakefile.toml

@@ -18,6 +18,7 @@ weak.linter.unicodeLinter = false
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
+rev = "1d2ba2d2aedb9065a4699cff0bfe8f0c3d3fb8d9"
 
 [[lean_lib]]
 name = "Cslib"