From be097c5e38cc1e8263402d6057833c2ede289899 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Fri, 13 Feb 2026 16:48:05 +1100
Subject: [PATCH] fix: nightly revision date logic and mathlib trigger auth
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR fixes two issues with the nightly release workflow:

1. The `workflow_dispatch` path used `date -u +%F` (current UTC date) to compute the
   base nightly name, but a manual re-release should revise the *most recent* nightly,
   not today's date. Now finds the latest `nightly-*` tag and creates a revision of that.

2. The mathlib4 nightly-testing trigger was broken:
   - Workflow renamed: `nightly_bump_toolchain.yml` → `nightly_bump_and_merge.yml`
   - `MATHLIB4_BOT` PAT expired after mathlib migrated to GitHub Apps
   - Replace with `actions/create-github-app-token` using the `mathlib-nightly-testing`
     app (requires `MATHLIB_NIGHTLY_TESTING_APP_ID` and
     `MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY` secrets to be configured)

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---
 .github/workflows/ci.yml | 36 ++++++++++++++++++++++--------------
 1 file changed, 22 insertions(+), 14 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 618fd2179491..4d065eb34c8d 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -60,22 +60,20 @@ jobs:
           if [[ -n '${{ secrets.PUSH_NIGHTLY_TOKEN }}' ]]; then
             git remote add nightly https://foo:'${{ secrets.PUSH_NIGHTLY_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-nightly.git
             git fetch nightly --tags
-            BASE_NIGHTLY="nightly-$(date -u +%F)"
             if [[ '${{ github.event_name }}' == 'workflow_dispatch' ]]; then
-              # Manual re-release: find next available revision if base nightly exists
-              if git rev-parse "refs/tags/$BASE_NIGHTLY" >/dev/null 2>&1; then
-                REV=1
-                while git rev-parse "refs/tags/${BASE_NIGHTLY}-rev${REV}" >/dev/null 2>&1; do
-                  REV=$((REV + 1))
-                done
-                LEAN_VERSION_STRING="${BASE_NIGHTLY}-rev${REV}"
-              else
-                LEAN_VERSION_STRING="$BASE_NIGHTLY"
-              fi
+              # Manual re-release: create a revision of the most recent nightly
+              BASE_NIGHTLY=$(git tag -l 'nightly-*' | sort -rV | head -1)
+              # Strip any existing -revK suffix to get the base date tag
+              BASE_NIGHTLY="${BASE_NIGHTLY%%-rev*}"
+              REV=1
+              while git rev-parse "refs/tags/${BASE_NIGHTLY}-rev${REV}" >/dev/null 2>&1; do
+                REV=$((REV + 1))
+              done
+              LEAN_VERSION_STRING="${BASE_NIGHTLY}-rev${REV}"
               echo "nightly=$LEAN_VERSION_STRING" >> "$GITHUB_OUTPUT"
             else
               # Scheduled: do nothing if commit already has a different tag
-              LEAN_VERSION_STRING="$BASE_NIGHTLY"
+              LEAN_VERSION_STRING="nightly-$(date -u +%F)"
               if [[ "$(git name-rev --name-only --tags --no-undefined HEAD 2> /dev/null || echo "$LEAN_VERSION_STRING")" == "$LEAN_VERSION_STRING" ]]; then
                 echo "nightly=$LEAN_VERSION_STRING" >> "$GITHUB_OUTPUT"
               fi
@@ -513,8 +511,18 @@ jobs:
           gh workflow -R leanprover/release-index run update-index.yml
         env:
           GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }}
+      - name: Generate mathlib nightly-testing app token
+        id: mathlib-app-token
+        uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
+        continue-on-error: true
+        with:
+          app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }}
+          private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }}
+          owner: leanprover-community
+          repositories: mathlib4-nightly-testing
       - name: Update toolchain on mathlib4's nightly-testing branch
+        if: steps.mathlib-app-token.outcome == 'success'
         run: |
-          gh workflow -R leanprover-community/mathlib4-nightly-testing run nightly_bump_toolchain.yml
+          gh workflow -R leanprover-community/mathlib4-nightly-testing run nightly_bump_and_merge.yml
         env:
-          GITHUB_TOKEN: ${{ secrets.MATHLIB4_BOT }}
+          GITHUB_TOKEN: ${{ steps.mathlib-app-token.outputs.token }}