chore: migrate nightly-testing workflows to GitHub App

.github/workflows/bump_toolchain_nightly-testing.yml

@@ -12,11 +12,19 @@ jobs:
     if: github.repository == 'leanprover/cslib'
     runs-on: ubuntu-latest
     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 }}
+    # The create-github-app-token README states that this token is masked and will not be logged accidentally.
+
     - name: Checkout code
       uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
       with:
         ref: nightly-testing # checkout nightly-testing branch
-        token: ${{ secrets.NIGHTLY_TESTING }}
+        token: ${{ steps.app-token.outputs.token }}
 
     - name: Get latest release tag from leanprover/lean4-nightly
       id: get-latest-release
@@ -70,10 +78,8 @@ jobs:
     - name: Commit and push changes
       if: steps.check-nightly-testing.outputs.tag_exists == 'true'
       run: |
-        # For now we reuse a bot managed by Mathlib,
-        # but it is fine to update this if Cslib wants to create its own bot accounts.
-        git config user.name "leanprover-community-mathlib4-bot"
-        git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
+        git config user.name "mathlib-nightly-testing[bot]"
+        git config user.email "mathlib-nightly-testing[bot]@users.noreply.github.com"
         git add lean-toolchain lakefile.toml lake-manifest.json
         # Don't fail if there's nothing to commit
         git commit -m "chore: bump to ${RELEASE_TAG} with mathlib at ${NIGHTLY_TESTING_TAG}" || true

.github/workflows/merge_main_into_nightly-testing.yml

@@ -13,13 +13,21 @@ jobs:
     if: github.repository == 'leanprover/cslib'
     runs-on: ubuntu-latest
     steps:
-      - name: Checkout nightly-testing 
+      - 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 }}
+      # The create-github-app-token README states that this token is masked and will not be logged accidentally.
+
+      - name: Checkout nightly-testing
         uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
         with:
           repository: leanprover/cslib
           ref: nightly-testing
           path: nightly-testing
-          token: ${{ secrets.NIGHTLY_TESTING }} # This secret needs repo access to leanprover/cslib
+          token: ${{ steps.app-token.outputs.token }}
           fetch-depth: 0
 
       - name: Configure Lean
@@ -33,10 +41,8 @@ jobs:
       - name: Configure Git User
         run: |
           cd nightly-testing
-          # For now we reuse a bot managed by Mathlib,
-          # but it is fine to update this if Cslib wants to create its own bot accounts.
-          git config user.name "leanprover-community-mathlib4-bot"
-          git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
+          git config user.name "mathlib-nightly-testing[bot]"
+          git config user.email "mathlib-nightly-testing[bot]@users.noreply.github.com"
 
       - name: Merge main to nightly-testing favoring nightly-testing changes
         run: |
@@ -58,5 +64,5 @@ jobs:
           # If there's nothing to do (because there are no new commits from main),
           # that's okay, hence the '|| true'.
           git commit -m "Merge main into nightly-testing" || true
-          # Push 
+          # Push
           git push origin nightly-testing

.github/workflows/report_failures_nightly-testing.yml

@@ -35,12 +35,20 @@ jobs:
     runs-on: ubuntu-latest
 
     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 }}
+    # The create-github-app-token README states that this token is masked and will not be logged accidentally.
+
     - name: Checkout code
       uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
       with:
         ref: nightly-testing # checkout nightly-testing branch
         fetch-depth: 0 # checkout all branches so that we can push from `nightly-testing` to `nightly-testing-YYYY-MM-DD`
-        token: ${{ secrets.NIGHTLY_TESTING }}
+        token: ${{ steps.app-token.outputs.token }}
     - name: Update the nightly-testing-YYYY-MM-DD branch
       run: |
         toolchain="$(<lean-toolchain)"
@@ -286,7 +294,7 @@ jobs:
       with:
         ref: nightly-testing # checkout nightly-testing branch (shouldn't matter which)
         fetch-depth: 0 # checkout all branches
-        token: ${{ secrets.NIGHTLY_TESTING }}
+        token: ${{ steps.app-token.outputs.token }}
 
     - name: Attempt automatic PR creation
       id: auto_pr
@@ -296,7 +304,7 @@ jobs:
         BUMP_VERSION: ${{ steps.bump_version.outputs.result }}
         BUMP_BRANCH: ${{ steps.latest_bump_branch.outputs.result }}
         SHA: ${{ env.SHA }}
-        GH_TOKEN: ${{ secrets.NIGHTLY_TESTING }}
+        GH_TOKEN: ${{ steps.app-token.outputs.token }}
         ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
       run: |
         echo "Current version: ${NIGHTLY}"