chore: migrate lean-pr-testing workflows to GitHub App

Replaces the `LEAN_PR_TESTING` personal access token with a GitHub App
token generated via `actions/create-github-app-token`.

This requires a GitHub App in the `leanprover` org installed on `lean4`.

Part of the migration from personal bot accounts to GitHub Apps.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>

Author: kim-em

.github/workflows/build_template.yml

@@ -54,6 +54,15 @@ jobs:
         shell: bash # there is no script body, so this is safe to "run" outside landrun.
         run: |
           # We just populate the env vars for this step to make them viewable in the logs
+      - name: Generate lean-pr-testing app token
+        id: lean-pr-testing-token
+        shell: bash
+        uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
+        with:
+          app-id: ${{ secrets.MATHLIB_LEAN_PR_TESTING_APP_ID }}
+          private-key: ${{ secrets.MATHLIB_LEAN_PR_TESTING_PRIVATE_KEY }}
+          owner: leanprover
+          repositories: lean4
       - name: cleanup
         shell: bash    # This *just* deletes old files, so is safe to run outside landrun.
         run: |
@@ -571,11 +580,12 @@ jobs:
             exit 1
           fi
 
+      # The create-github-app-token README states that this token is masked and will not be logged accidentally.
       - name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
         if: always()
         shell: bash
         env:
-          TOKEN: ${{ secrets.LEAN_PR_TESTING }}
+          TOKEN: ${{ steps.lean-pr-testing-token.outputs.token }}
           GITHUB_CONTEXT: ${{ toJson(github) }}
           WORKFLOW_URL: https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}
           BUILD_OUTCOME: ${{ steps.build.outcome }}

.github/workflows/nightly_detect_failure.yml

@@ -80,12 +80,21 @@ jobs:
     - name: Cleanup workspace
       run: |
         sudo rm -rf -- *
+    - name: Generate lean-pr-testing app token
+      id: lean-pr-testing-token
+      uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
+      with:
+        app-id: ${{ secrets.MATHLIB_LEAN_PR_TESTING_APP_ID }}
+        private-key: ${{ secrets.MATHLIB_LEAN_PR_TESTING_PRIVATE_KEY }}
+        owner: leanprover
+        repositories: lean4
     # Checkout the Lean repository on 'nightly-with-mathlib'
+    # The create-github-app-token README states that this token is masked and will not be logged accidentally.
     - name: Checkout Lean repository
       uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
       with:
         repository: leanprover/lean4
-        token: ${{ secrets.LEAN_PR_TESTING }}
+        token: ${{ steps.lean-pr-testing-token.outputs.token }}
         ref: nightly-with-mathlib
     # Merge the relevant nightly.
     - name: Fetch tags from 'lean4-nightly', and merge relevant nightly into 'nightly-with-mathlib'