From c1866a7b7e66fa23bbfa2098f9c75c0fc25a1ab3 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Mon, 26 May 2025 12:13:00 +1000
Subject: [PATCH] chore: fix awaiting-mathlib.yml (#8480)

This PR hopefully fixes a problem from #8471, which even the most
cursory testing (by me!) should have detected.
---
 .github/workflows/awaiting-mathlib.yml | 27 +++++++++++++-------------
 1 file changed, 13 insertions(+), 14 deletions(-)

diff --git a/.github/workflows/awaiting-mathlib.yml b/.github/workflows/awaiting-mathlib.yml
index bcbe44dfcd..27a0a8e295 100644
--- a/.github/workflows/awaiting-mathlib.yml
+++ b/.github/workflows/awaiting-mathlib.yml
@@ -10,6 +10,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check awaiting-mathlib label
+        id: check-awaiting-mathlib-label
         if: github.event_name == 'pull_request'
         uses: actions/github-script@v7
         with:
@@ -22,18 +23,16 @@ jobs:
             if (hasAwaiting && hasBreaks) {
               core.setFailed('PR has both "awaiting-mathlib" and "breaks-mathlib" labels.');
             } else if (hasAwaiting && !hasBreaks && !hasBuilds) {
-              // Create a neutral check run (yellow circle)
-              const octokit = github.getOctokit(process.env.GITHUB_TOKEN);
-              await octokit.rest.checks.create({
-                owner: context.repo.owner,
-                repo: context.repo.repo,
-                name: "awaiting-mathlib label check",
-                head_sha: context.payload.pull_request.head.sha,
-                status: "completed",
-                conclusion: "neutral",
-                output: {
-                  title: "Awaiting mathlib",
-                  summary: 'PR is marked "awaiting-mathlib" but neither "breaks-mathlib" nor "builds-mathlib" labels are present.'
-                }
-              });
+              core.info('PR is marked "awaiting-mathlib" but neither "breaks-mathlib" nor "builds-mathlib" labels are present.');
+              core.setOutput('awaiting', 'true');
             }
+      
+      - name: Wait for mathlib compatibility
+        if: github.event_name == 'pull_request' && steps.check-awaiting-mathlib-label.outputs.awaiting == 'true'
+        run: |
+          echo "::notice title=Awaiting mathlib::PR is marked 'awaiting-mathlib' but neither 'breaks-mathlib' nor 'builds-mathlib' labels are present."
+          echo "This check will remain in progress until the PR is updated with appropriate mathlib compatibility labels."
+          # Keep the job running indefinitely to show "in progress" status
+          while true; do
+            sleep 3600  # Sleep for 1 hour at a time
+          done