From 5536281238dff2fb4e0a54da472d4f0d6496069e Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Wed, 5 Mar 2025 17:36:38 +1100
Subject: [PATCH] feat: force-mathlib-ci label (#7337)

This PR adds support for a `force-mathlib-ci` label, which attempts full
Mathlib CI even if the PR branch is not based off the
`nightly-with-mathlib` branch, or if the relevant
`nightly-testing-YYYY-MM-DD` branch is not present at Batteries or
Mathlib.
---
 .github/workflows/pr-release.yml | 25 ++++++++++++++++++++++---
 1 file changed, 22 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml
index 22f3c64839..b730d6a897 100644
--- a/.github/workflows/pr-release.yml
+++ b/.github/workflows/pr-release.yml
@@ -155,6 +155,20 @@ jobs:
           fi
 
           if [[ -n "$MESSAGE" ]]; then
+            # Check if force-mathlib-ci label is present
+            LABELS="$(curl --retry 3 --location --silent \
+                          -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
+                          -H "Accept: application/vnd.github.v3+json" \
+                          "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/labels" \
+                          | jq -r '.[].name')"
+            
+            if echo "$LABELS" | grep -q "^force-mathlib-ci$"; then
+              echo "force-mathlib-ci label detected, forcing CI despite issues"
+              MESSAGE="Forcing Mathlib CI because the \`force-mathlib-ci\` label is present, despite problem: $MESSAGE"
+              FORCE_CI=true
+            else
+              MESSAGE="$MESSAGE You can force Mathlib CI using the \`force-mathlib-ci\` label."
+            fi
 
             echo "Checking existing messages"
 
@@ -201,7 +215,12 @@ jobs:
             else
               echo "The message already exists in the comment body."
             fi
-            echo "mathlib_ready=false" >> "$GITHUB_OUTPUT"
+
+            if [[ "$FORCE_CI" == "true" ]]; then
+              echo "mathlib_ready=true" >> "$GITHUB_OUTPUT"
+            else
+              echo "mathlib_ready=false" >> "$GITHUB_OUTPUT"
+            fi
           else
             echo "mathlib_ready=true" >> "$GITHUB_OUTPUT"
           fi
@@ -252,7 +271,7 @@ jobs:
           if git ls-remote --heads --tags --exit-code origin "nightly-testing-${MOST_RECENT_NIGHTLY}" >/dev/null; then
             BASE="nightly-testing-${MOST_RECENT_NIGHTLY}"
           else
-            echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Batteries. Falling back to 'nightly-testing'."
+            echo "Couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Batteries. Falling back to 'nightly-testing'."
             BASE=nightly-testing
           fi
 
@@ -316,7 +335,7 @@ jobs:
           if git ls-remote --heads --tags --exit-code origin "nightly-testing-${MOST_RECENT_NIGHTLY}" >/dev/null; then
             BASE="nightly-testing-${MOST_RECENT_NIGHTLY}"
           else
-            echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' branch at Mathlib. Falling back to 'nightly-testing'."
+            echo "Couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' branch at Mathlib. Falling back to 'nightly-testing'."
             BASE=nightly-testing
           fi