From cbf6fe5d1be2186da51492658cf1018f0762cc59 Mon Sep 17 00:00:00 2001
From: Garmelon <joscha@plugh.de>
Date: Mon, 8 Dec 2025 15:04:21 +0100
Subject: [PATCH] chore: add mathlib4-nightly-available label (#11526)

This PR automatically adds
https://github.com/leanprover/lean4/labels/mathlib4-nightly-available to
a PR if a corresponding branch exists in
https://github.com/leanprover-community/mathlib4-nightly-testing. This
way, the `!bench mathlib` command can delay the benchmark job until
everything is ready.
---
 .github/workflows/pr-release.yml | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml
index 117bf5cd3d..ab3454c50e 100644
--- a/.github/workflows/pr-release.yml
+++ b/.github/workflows/pr-release.yml
@@ -127,7 +127,7 @@ jobs:
               description: "${{ github.repository_owner }}/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}",
             });
 
-      - name: Add label
+      - name: Add toolchain-available label
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         uses: actions/github-script@v8
         with:
@@ -515,6 +515,18 @@ jobs:
         run: |
           git push origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
 
+      - name: Add mathlib4-nightly-available label
+        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
+        uses: actions/github-script@v8
+        with:
+          script: |
+            await github.rest.issues.addLabels({
+              issue_number: ${{ steps.workflow-info.outputs.pullRequestNumber }},
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              labels: ['mathlib4-nightly-available']
+            })
+
       # We next automatically create a reference manual branch using this toolchain.
       # Reference manual CI will be responsible for reporting back success or failure
       # to the PR comments asynchronously (and thus transitively SubVerso/Verso).