From e877a2b67d22be40b4ca6bcbbcaeb236f2370eab Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 3 Feb 2026 05:28:56 +0000 Subject: [PATCH] chore: migrate nightly-testing workflows to GitHub App MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Migrate from NIGHTLY_TESTING token (from leanprover-community-mathlib4-bot) to mathlib-nightly-testing GitHub App. This is part of the migration away from bot accounts following GitHub ToS notice. 🤖 Prepared with Claude Code --- .../bump_toolchain_nightly-testing.yml | 16 ++++++++++----- .../merge_main_into_nightly-testing.yml | 20 ++++++++++++------- .../report_failures_nightly-testing.yml | 14 ++++++++++--- 3 files changed, 35 insertions(+), 15 deletions(-) diff --git a/.github/workflows/bump_toolchain_nightly-testing.yml b/.github/workflows/bump_toolchain_nightly-testing.yml index cd5022183..cb0925a58 100644 --- a/.github/workflows/bump_toolchain_nightly-testing.yml +++ b/.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 diff --git a/.github/workflows/merge_main_into_nightly-testing.yml b/.github/workflows/merge_main_into_nightly-testing.yml index 38860a8cd..3d73be5c5 100644 --- a/.github/workflows/merge_main_into_nightly-testing.yml +++ b/.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 diff --git a/.github/workflows/report_failures_nightly-testing.yml b/.github/workflows/report_failures_nightly-testing.yml index 2ad0a8b41..bdbd87881 100644 --- a/.github/workflows/report_failures_nightly-testing.yml +++ b/.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="$(