Skip to content

Commit 0f81be6

Browse files
committed
chore: migrate nightly-testing workflows to GitHub App (leanprover-community#34751)
This PR migrates the nightly-testing workflows from using a personal access token (`NIGHTLY_TESTING` from `leanprover-community-mathlib4-bot`) to using a GitHub App. Affects: `nightly_merge_master.yml`, `nightly_bump_toolchain.yml`, `discover-lean-pr-testing.yml`, `nightly_detect_failure.yml` **Note:** The app must be installed on both `mathlib4` AND `mathlib4-nightly-testing`, and secrets must be added to both repos. 🤖 Prepared with Claude Code
1 parent 97cc7ce commit 0f81be6

4 files changed

Lines changed: 45 additions & 12 deletions

File tree

.github/workflows/discover-lean-pr-testing.yml

Lines changed: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,17 +13,25 @@ jobs:
1313
if: github.repository == 'leanprover-community/mathlib4-nightly-testing'
1414

1515
steps:
16+
- name: Generate app token
17+
id: app-token
18+
uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
19+
with:
20+
app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }}
21+
private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }}
22+
23+
# The create-github-app-token README states that this token is masked and will not be logged accidentally.
1624
- name: Checkout mathlib4 repository
1725
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
1826
with:
1927
ref: nightly-testing
2028
fetch-depth: 0 # Fetch all branches
21-
token: ${{ secrets.NIGHTLY_TESTING }}
29+
token: ${{ steps.app-token.outputs.token }}
2230

2331
- name: Set up Git
2432
run: |
25-
git config --global user.name "leanprover-community-mathlib4-bot"
26-
git config --global user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
33+
git config --global user.name "mathlib-nightly-testing[bot]"
34+
git config --global user.email "mathlib-nightly-testing[bot]@users.noreply.github.com"
2735
2836
- name: Configure Lean
2937
uses: leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4.0

.github/workflows/nightly_bump_toolchain.yml

Lines changed: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,11 +13,19 @@ jobs:
1313
runs-on: ubuntu-latest
1414
if: github.repository == 'leanprover-community/mathlib4-nightly-testing'
1515
steps:
16+
- name: Generate app token
17+
id: app-token
18+
uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
19+
with:
20+
app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }}
21+
private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }}
22+
23+
# The create-github-app-token README states that this token is masked and will not be logged accidentally.
1624
- name: Checkout code
1725
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
1826
with:
1927
ref: nightly-testing # checkout nightly-testing branch
20-
token: ${{ secrets.NIGHTLY_TESTING }}
28+
token: ${{ steps.app-token.outputs.token }}
2129

2230
- name: Get latest release tag from leanprover/lean4-nightly
2331
id: get-latest-release
@@ -31,8 +39,8 @@ jobs:
3139
3240
- name: Commit and push changes
3341
run: |
34-
git config user.name "leanprover-community-mathlib4-bot"
35-
git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
42+
git config user.name "mathlib-nightly-testing[bot]"
43+
git config user.email "mathlib-nightly-testing[bot]@users.noreply.github.com"
3644
git add lean-toolchain
3745
# Don't fail if there's nothing to commit
3846
git commit -m "chore: bump to ${RELEASE_TAG}" || true

.github/workflows/nightly_detect_failure.yml

Lines changed: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -35,12 +35,20 @@ jobs:
3535
runs-on: ubuntu-latest
3636

3737
steps:
38+
- name: Generate app token
39+
id: app-token
40+
uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
41+
with:
42+
app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }}
43+
private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }}
44+
45+
# The create-github-app-token README states that this token is masked and will not be logged accidentally.
3846
- name: Checkout code
3947
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
4048
with:
4149
ref: nightly-testing # checkout nightly-testing branch
4250
fetch-depth: 0 # checkout all branches so that we can push from `nightly-testing` to `nightly-testing-YYYY-MM-DD`
43-
token: ${{ secrets.NIGHTLY_TESTING }}
51+
token: ${{ steps.app-token.outputs.token }}
4452
- name: Update the nightly-testing-green branch
4553
continue-on-error: true
4654
run: |
@@ -313,7 +321,7 @@ jobs:
313321
with:
314322
ref: nightly-testing # checkout nightly-testing branch (shouldn't matter which)
315323
fetch-depth: 0 # checkout all branches
316-
token: ${{ secrets.NIGHTLY_TESTING }}
324+
token: ${{ steps.app-token.outputs.token }}
317325

318326
- name: Attempt automatic PR creation
319327
id: auto_pr
@@ -323,7 +331,7 @@ jobs:
323331
BUMP_VERSION: ${{ steps.bump_version.outputs.result }}
324332
BUMP_BRANCH: ${{ steps.latest_bump_branch.outputs.result }}
325333
SHA: ${{ env.SHA }}
326-
GH_TOKEN: ${{ secrets.NIGHTLY_TESTING }}
334+
GH_TOKEN: ${{ steps.app-token.outputs.token }}
327335
ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
328336
run: |
329337
echo "Current version: ${NIGHTLY}"

.github/workflows/nightly_merge_master.yml

Lines changed: 12 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -12,13 +12,22 @@ jobs:
1212
runs-on: ubuntu-latest
1313
if: github.repository == 'leanprover-community/mathlib4'
1414
steps:
15+
- name: Generate app token
16+
id: app-token
17+
uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
18+
with:
19+
app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }}
20+
private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }}
21+
repositories: mathlib4,mathlib4-nightly-testing
22+
23+
# The create-github-app-token README states that this token is masked and will not be logged accidentally.
1524
- name: Checkout nightly-testing from fork
1625
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
1726
with:
1827
repository: leanprover-community/mathlib4-nightly-testing
1928
ref: nightly-testing
2029
path: nightly-testing
21-
token: ${{ secrets.NIGHTLY_TESTING }}
30+
token: ${{ steps.app-token.outputs.token }}
2231
fetch-depth: 0
2332

2433
- name: Configure Lean
@@ -32,8 +41,8 @@ jobs:
3241
- name: Configure Git User
3342
run: |
3443
cd nightly-testing
35-
git config user.name "leanprover-community-mathlib4-bot"
36-
git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
44+
git config user.name "mathlib-nightly-testing[bot]"
45+
git config user.email "mathlib-nightly-testing[bot]@users.noreply.github.com"
3746
3847
- name: Merge master to nightly favoring nightly changes
3948
run: |

0 commit comments

Comments
 (0)