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