chore: migrate triage workflows to GitHub App (leanprover-community#34752)

kim-em · kim-em · commit 0bbce5a6376e · 2026-02-04T00:38:52.000Z
This PR migrates `maintainer_bors.yml`, `maintainer_bors_wf_run.yml`, `maintainer_merge.yml`, and `maintainer_merge_wf_run.yml` from using a personal access token (`TRIAGE_TOKEN`) to using a GitHub App.

🤖 Prepared with Claude Code
diff --git a/.github/workflows/maintainer_bors.yml b/.github/workflows/maintainer_bors.yml
@@ -23,10 +23,19 @@ jobs:
       COMMENT_REVIEW: ${{ github.event.review.body }}
       PR_NUMBER: ${{ github.event.issue.number }}${{ github.event.pull_request.number }}
       HAS_DELEGATED_LABEL: ${{ contains(github.event.issue.labels.*.name, 'delegated') }}
+      HAS_TRIAGE_SECRET: ${{ secrets.MATHLIB_TRIAGE_APP_ID != '' }}
     name: Add ready-to-merge or delegated label
     runs-on: ubuntu-latest
     if: github.repository == 'leanprover-community/mathlib4'
     steps:
+      - name: Generate app token
+        if: ${{ env.HAS_TRIAGE_SECRET == 'true' }}
+        id: app-token
+        uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
+        with:
+          app-id: ${{ secrets.MATHLIB_TRIAGE_APP_ID }}
+          private-key: ${{ secrets.MATHLIB_TRIAGE_PRIVATE_KEY }}
+
       - name: Find bors merge/delegate
         id: merge_or_delegate
         run: |
@@ -58,7 +67,8 @@ jobs:
           printf $'removeLabels=%s\n' "${remove_labels}" >> "${GITHUB_OUTPUT}"
           if [ "${AUTHOR}" == 'leanprover-community-mathlib4-bot' ] ||
              [ "${AUTHOR}" == 'leanprover-community-bot-assistant' ] ||
-             [ "${AUTHOR}" == 'mathlib-bors[bot]' ]
+             [ "${AUTHOR}" == 'mathlib-bors[bot]' ] ||
+             [ "${AUTHOR}" == 'mathlib-triage[bot]' ]
           then
             printf $'bot=true\n'
             printf $'bot=true\n' >> "${GITHUB_OUTPUT}"
@@ -70,7 +80,7 @@ jobs:
           fi
 
           # write an artifact with all data needed below if we don't have access to necessary secrets
-          if [[ -z '${{ secrets.TRIAGE_TOKEN }}' ]]
+          if [[ -z '${{ secrets.MATHLIB_TRIAGE_APP_ID }}' ]]
           then
             printf 'No access to secrets, writing to file.\n'
             jq -n \
@@ -131,7 +141,8 @@ jobs:
           issue_number: ${{ github.event.issue.number }}${{ github.event.pull_request.number }}
           labels: '["${{ steps.merge_or_delegate.outputs.mOrD }}"]'
         env:
-          GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }}
+          # The create-github-app-token README states that this token is masked and will not be logged accidentally.
+          GITHUB_TOKEN: ${{ steps.app-token.outputs.token }}
 
       - if: ${{ ! steps.merge_or_delegate.outputs.secrets == '' &&
           (! steps.merge_or_delegate.outputs.mOrD == '' &&
@@ -145,7 +156,7 @@ jobs:
           for label in awaiting-author maintainer-merge; do
             curl --request DELETE \
               --url "https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}${{ github.event.pull_request.number }}/labels/${label}" \
-              --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
+              --header 'authorization: Bearer ${{ steps.app-token.outputs.token }}'
           done
 
       - name: On bors r/d-, remove ready-to-merge or delegated label
@@ -158,7 +169,7 @@ jobs:
           for label in ready-to-merge delegated; do
             curl --request DELETE \
               --url "https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}${{ github.event.pull_request.number }}/labels/${label}" \
-              --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
+              --header 'authorization: Bearer ${{ steps.app-token.outputs.token }}'
           done
 
       - name: Set up Python
diff --git a/.github/workflows/maintainer_bors_wf_run.yml b/.github/workflows/maintainer_bors_wf_run.yml
@@ -13,6 +13,13 @@ jobs:
     runs-on: ubuntu-latest
     if: ${{ github.repository == 'leanprover-community/mathlib4' && github.event.workflow_run.conclusion == 'success' }}
     steps:
+      - name: Generate app token
+        id: app-token
+        uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
+        with:
+          app-id: ${{ secrets.MATHLIB_TRIAGE_APP_ID }}
+          private-key: ${{ secrets.MATHLIB_TRIAGE_PRIVATE_KEY }}
+
       - name: Download artifact
         id: download-artifact
         uses: dawidd6/action-download-artifact@5c98f0b039f36ef966fdb7dfa9779262785ecb05 # v14
@@ -80,7 +87,8 @@ jobs:
           issue_number: ${{ steps.extract-data.outputs.pr_number }}
           labels: '["${{ steps.extract-data.outputs.mOrD }}"]'
         env:
-          GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }}
+          # The create-github-app-token README states that this token is masked and will not be logged accidentally.
+          GITHUB_TOKEN: ${{ steps.app-token.outputs.token }}
 
       - if: ${{ ! steps.extract-data.outputs.mOrD == '' &&
           ( steps.user_permission.outputs.require-result == 'true' ||
@@ -93,7 +101,7 @@ jobs:
           for label in awaiting-author maintainer-merge; do
             curl --request DELETE \
               --url "https://api.github.com/repos/${{ github.repository }}/issues/${{ steps.extract-data.outputs.pr_number }}/labels/${label}" \
-              --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
+              --header 'authorization: Bearer ${{ steps.app-token.outputs.token }}'
           done
 
       - name: On bors r/d-, remove ready-to-merge or delegated label
@@ -104,7 +112,7 @@ jobs:
           for label in ready-to-merge delegated; do
             curl --request DELETE \
               --url "https://api.github.com/repos/${{ github.repository }}/issues/${{ steps.extract-data.outputs.pr_number }}/labels/${label}" \
-              --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
+              --header 'authorization: Bearer ${{ steps.app-token.outputs.token }}'
           done
 
       - name: Set up Python
diff --git a/.github/workflows/maintainer_merge.yml b/.github/workflows/maintainer_merge.yml
@@ -27,6 +27,7 @@ jobs:
       PR_TITLE_PR: ${{ github.event.pull_request.title }}
       PR_URL: ${{ github.event.issue.html_url }}${{ github.event.pull_request.html_url }}
       EVENT_NAME: ${{ github.event_name }}
+      HAS_TRIAGE_SECRET: ${{ secrets.MATHLIB_TRIAGE_APP_ID != '' }}
     name: Ping maintainers on Zulip
     runs-on: ubuntu-latest
     if: >- # crude check to skip running this on most reviews / comments
@@ -36,6 +37,14 @@ jobs:
         contains(format('{0}{1}', github.event.comment.body, github.event.review.body), 'maintainer delegate')
       )
     steps:
+      - name: Generate app token
+        if: ${{ env.HAS_TRIAGE_SECRET == 'true' }}
+        id: app-token
+        uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
+        with:
+          app-id: ${{ secrets.MATHLIB_TRIAGE_APP_ID }}
+          private-key: ${{ secrets.MATHLIB_TRIAGE_PRIVATE_KEY }}
+
       - name: Find maintainer merge/delegate
         id: merge_or_delegate
         run: |
@@ -58,7 +67,7 @@ jobs:
           printf $'mOrD=%s\n' "${m_or_d}" > "${GITHUB_OUTPUT}"
 
           # write an artifact with all data needed below if we don't have access to necessary secrets
-          if [[ -z '${{ secrets.MATHLIB_REVIEWERS_TEAM_KEY }}' ]]
+          if [[ -z '${{ secrets.MATHLIB_TRIAGE_APP_ID }}' ]]
           then
             printf 'No access to secrets, writing to file.\n'
             jq -n \
@@ -167,7 +176,8 @@ jobs:
         uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8.0.0
         with:
           # labels added by GITHUB_TOKEN won't trigger the Zulip emoji workflow
-          github-token: ${{secrets.TRIAGE_TOKEN}}
+          # The create-github-app-token README states that this token is masked and will not be logged accidentally.
+          github-token: ${{ steps.app-token.outputs.token }}
           script: |
             const { owner, repo, number: issue_number } = context.issue;
             await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['maintainer-merge'] });
diff --git a/.github/workflows/maintainer_merge_wf_run.yml b/.github/workflows/maintainer_merge_wf_run.yml
@@ -13,6 +13,13 @@ jobs:
     runs-on: ubuntu-latest
     if: ${{ github.repository == 'leanprover-community/mathlib4' && github.event.workflow_run.conclusion == 'success' }}
     steps:
+      - name: Generate app token
+        id: app-token
+        uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
+        with:
+          app-id: ${{ secrets.MATHLIB_TRIAGE_APP_ID }}
+          private-key: ${{ secrets.MATHLIB_TRIAGE_PRIVATE_KEY }}
+
       - name: Download artifact
         id: download-artifact
         uses: dawidd6/action-download-artifact@5c98f0b039f36ef966fdb7dfa9779262785ecb05 # v14
@@ -140,7 +147,8 @@ jobs:
         uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8.0.0
         with:
           # labels added by GITHUB_TOKEN won't trigger the Zulip emoji workflow
-          github-token: ${{secrets.TRIAGE_TOKEN}}
+          # The create-github-app-token README states that this token is masked and will not be logged accidentally.
+          github-token: ${{ steps.app-token.outputs.token }}
           script: |
             const { owner, repo } = context.repo;
             const issue_number = ${{ steps.extract-data.outputs.pr_number }};
