From b35357634920f75fc5a9cc53d37be8356aa04724 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sat, 2 May 2026 22:31:37 +1000
Subject: [PATCH] fix: pin nightly_detect_failure checkout to the tested SHA
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR fixes a race condition in the `handle_success` job: the workflow
checked out `ref: nightly-testing` after CI completed, so if a new commit
landed on `nightly-testing` between the start of CI and the firing of the
`workflow_run` event, the `nightly-testing-YYYY-MM-DD` tag (and the
`nightly-testing-green` / `nightly-testing-daily` branch updates) would
point to an untested commit. Downstream consumers — `daily.yml`, nanoda,
leanchecker, executable jobs — then test that untested commit, producing
spurious failures attributed to nanoda/leanchecker rather than to the
broken tag.

Pin the checkout to `${{ github.event.workflow_run.head_sha }}`, the SHA
whose CI just succeeded, so the tag is always anchored to a tested commit.

Also fix the `handle_failure` Zulip message, which used `${{ github.sha }}`
— in a `workflow_run` event this is the SHA of the workflow's branch, not
the SHA of the failing run, so the linked commit was misleading whenever a
new commit had landed during CI.

🤖 Prepared with Claude Code
---
 .github/workflows/nightly_detect_failure.yml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/nightly_detect_failure.yml b/.github/workflows/nightly_detect_failure.yml
index 7422921823ca07..4e483def8c0f9a 100644
--- a/.github/workflows/nightly_detect_failure.yml
+++ b/.github/workflows/nightly_detect_failure.yml
@@ -25,7 +25,7 @@ jobs:
         type: 'stream'
         topic: 'Mathlib status updates'
         content: |
-          ❌ The latest CI for Mathlib's [nightly-testing branch](https://github.com/leanprover-community/mathlib4-nightly-testing/tree/nightly-testing) has [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}) ([${{ github.sha }}](https://github.com/${{ github.repository }}/commit/${{ github.sha }})).
+          ❌ The latest CI for Mathlib's [nightly-testing branch](https://github.com/leanprover-community/mathlib4-nightly-testing/tree/nightly-testing) has [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}) ([${{ github.event.workflow_run.head_sha }}](https://github.com/${{ github.repository }}/commit/${{ github.event.workflow_run.head_sha }})).
           You can `git fetch; git checkout nightly-testing` and push a fix.
 
   handle_success:
@@ -52,7 +52,10 @@ jobs:
     - name: Checkout code
       uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
       with:
-        ref: nightly-testing # checkout nightly-testing branch
+        # Pin to the SHA whose CI just succeeded, not the current tip of `nightly-testing`,
+        # which may have advanced while CI was running. Without this, the tag and
+        # `nightly-testing-{green,daily}` updates below can point to an untested commit.
+        ref: ${{ github.event.workflow_run.head_sha }}
         fetch-depth: 0 # checkout all branches so that we can push from `nightly-testing` to `nightly-testing-YYYY-MM-DD`
         token: ${{ steps.app-token.outputs.token }}
     - name: Update the nightly-testing-green branch