fix: use mathlib-lean-pr-testing app for PR comments (#12323)

This PR fixes the PR release workflow which was failing due to the
deprecated `MATHLIB4_COMMENT_BOT` PAT being invalid.

**Error:** `jq: error (at <stdin>:4): Cannot index string with string
"name"` when fetching labels - the API returned an error response
instead of labels array because the PAT credentials were bad.

**Changes:**
- Generate a token from the `mathlib-lean-pr-testing` GitHub App (ID:
2785182) for posting comments to Lean PRs about mathlib compatibility
- Use `GITHUB_TOKEN` for read-only label fetching (no special identity
needed)
- Update the bot username check from `leanprover-community-bot` to
`mathlib-lean-pr-testing[bot]`

**Secrets added:** `MATHLIB_LEAN_PR_TESTING_APP_ID` and
`MATHLIB_LEAN_PR_TESTING_PRIVATE_KEY` have been added to the repository.

Fixes the CI failure at
https://github.com/leanprover/lean4/actions/runs/21705647318/job/62595966115

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>

.github/workflows/pr-release.yml

@@ -170,6 +170,18 @@ jobs:
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         uses: dcarbone/install-jq-action@v3.2.0
 
+      # Generate a token for posting comments to Lean PRs about mathlib compatibility.
+      # This app is in the leanprover org and installed on leanprover/lean4.
+      - name: Generate GitHub App token for Lean PR comments
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
+        id: mathlib-comment-token
+        uses: actions/create-github-app-token@3ff1caaa28b64c9cc276ce0a02e2ff584f3900c5 # v2.0.2
+        with:
+          app-id: ${{ secrets.MATHLIB_LEAN_PR_TESTING_APP_ID }}
+          private-key: ${{ secrets.MATHLIB_LEAN_PR_TESTING_PRIVATE_KEY }}
+          owner: leanprover
+          repositories: lean4
+
       # Check that the most recently nightly coincides with 'git merge-base HEAD master'
       - name: Check merge-base and nightly-testing-YYYY-MM-DD for Mathlib/Batteries
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
@@ -204,8 +216,9 @@ jobs:
 
           if [[ -n "$MESSAGE" ]]; then
             # Check if force-mathlib-ci label is present
+            # Use GITHUB_TOKEN for read-only label fetch (MATHLIB4_COMMENT_BOT is only for posting comments)
             LABELS="$(curl --retry 3 --location --silent \
-                          -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
+                          -H "Authorization: token ${{ secrets.GITHUB_TOKEN }}" \
                           -H "Accept: application/vnd.github.v3+json" \
                           "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/labels" \
                           | jq -r '.[].name')"
@@ -226,10 +239,10 @@ jobs:
 
             # Use GitHub API to check if a comment already exists
             existing_comment="$(curl --retry 3 --location --silent \
-                                    -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
+                                    -H "Authorization: token ${{ steps.mathlib-comment-token.outputs.token }}" \
                                     -H "Accept: application/vnd.github.v3+json" \
                                     "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments" \
-                                    | jq 'first(.[] | select(.body | test("^- . Mathlib") or startswith("Mathlib CI status")) | select(.user.login == "leanprover-community-bot"))')"
+                                    | jq 'first(.[] | select(.body | test("^- . Mathlib") or startswith("Mathlib CI status")) | select(.user.login == "mathlib-lean-pr-testing[bot]"))')"
             existing_comment_id="$(echo "$existing_comment" | jq -r .id)"
             existing_comment_body="$(echo "$existing_comment" | jq -r .body)"
 
@@ -239,14 +252,14 @@ jobs:
               echo "Posting message to the comments: $MESSAGE"
 
               # Append new result to the existing comment or post a new comment
-              # It's essential we use the MATHLIB4_COMMENT_BOT token here, so that Mathlib CI can subsequently edit the comment.
+              # Use the mathlib-lean-pr-testing app token so Mathlib CI can subsequently edit the comment.
               if [ -z "$existing_comment_id" ]; then
                 INTRO="Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)):"
                 # Post new comment with a bullet point
                 echo "Posting as new comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
                 curl -L -s \
                   -X POST \
-                  -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
+                  -H "Authorization: token ${{ steps.mathlib-comment-token.outputs.token }}" \
                   -H "Accept: application/vnd.github.v3+json" \
                   -d "$(jq --null-input --arg intro "$INTRO" --arg val "$MESSAGE" '{"body":($intro + "\n" + $val)}')" \
                   "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
@@ -255,7 +268,7 @@ jobs:
                 echo "Appending to existing comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
                 curl -L -s \
                   -X PATCH \
-                  -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
+                  -H "Authorization: token ${{ steps.mathlib-comment-token.outputs.token }}" \
                   -H "Accept: application/vnd.github.v3+json" \
                   -d "$(jq --null-input --arg existing "$existing_comment_body" --arg message "$MESSAGE" '{"body":($existing + "\n" + $message)}')" \
                   "https://api.github.com/repos/leanprover/lean4/issues/comments/$existing_comment_id"