From bdbb6597657869edcb458337cd8ee6b25566df09 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Sun, 25 May 2025 22:38:56 +1000
Subject: [PATCH] chore: while awaiting-mathlib, show yellow status not red
 (#8471)

This PR changes the CI check when the `awaiting-mathlib` label is
present. If `breaks-mathlib` is present, it shows a red cross, but if
neither `breaks-mathlib` nor `builds-mathlib` is present it shows a
yellow circle.
---
 .github/workflows/awaiting-mathlib.yml | 25 ++++++++++++++++++++++---
 1 file changed, 22 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/awaiting-mathlib.yml b/.github/workflows/awaiting-mathlib.yml
index 01dbfea01c..bcbe44dfcd 100644
--- a/.github/workflows/awaiting-mathlib.yml
+++ b/.github/workflows/awaiting-mathlib.yml
@@ -14,7 +14,26 @@ jobs:
         uses: actions/github-script@v7
         with:
           script: |
-            const { labels } = context.payload.pull_request;
-            if (labels.some(label => label.name == "awaiting-mathlib") && !labels.some(label => label.name == "builds-mathlib")) {
-              core.setFailed('PR is marked "awaiting-mathlib" but "builds-mathlib" label has not been applied yet by the bot');
+            const { labels, number: prNumber } = context.payload.pull_request;
+            const hasAwaiting = labels.some(label => label.name == "awaiting-mathlib");
+            const hasBreaks = labels.some(label => label.name == "breaks-mathlib");
+            const hasBuilds = labels.some(label => label.name == "builds-mathlib");
+
+            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.'
+                }
+              });
             }