1010 runs-on : ubuntu-latest
1111 steps :
1212 - name : Check awaiting-mathlib label
13+ id : check-awaiting-mathlib-label
1314 if : github.event_name == 'pull_request'
1415 uses : actions/github-script@v7
1516 with :
@@ -22,18 +23,16 @@ jobs:
2223 if (hasAwaiting && hasBreaks) {
2324 core.setFailed('PR has both "awaiting-mathlib" and "breaks-mathlib" labels.');
2425 } else if (hasAwaiting && !hasBreaks && !hasBuilds) {
25- // Create a neutral check run (yellow circle)
26- const octokit = github.getOctokit(process.env.GITHUB_TOKEN);
27- await octokit.rest.checks.create({
28- owner: context.repo.owner,
29- repo: context.repo.repo,
30- name: "awaiting-mathlib label check",
31- head_sha: context.payload.pull_request.head.sha,
32- status: "completed",
33- conclusion: "neutral",
34- output: {
35- title: "Awaiting mathlib",
36- summary: 'PR is marked "awaiting-mathlib" but neither "breaks-mathlib" nor "builds-mathlib" labels are present.'
37- }
38- });
26+ core.info('PR is marked "awaiting-mathlib" but neither "breaks-mathlib" nor "builds-mathlib" labels are present.');
27+ core.setOutput('awaiting', 'true');
3928 }
29+
30+ - name : Wait for mathlib compatibility
31+ if : github.event_name == 'pull_request' && steps.check-awaiting-mathlib-label.outputs.awaiting == 'true'
32+ run : |
33+ echo "::notice title=Awaiting mathlib::PR is marked 'awaiting-mathlib' but neither 'breaks-mathlib' nor 'builds-mathlib' labels are present."
34+ echo "This check will remain in progress until the PR is updated with appropriate mathlib compatibility labels."
35+ # Keep the job running indefinitely to show "in progress" status
36+ while true; do
37+ sleep 3600 # Sleep for 1 hour at a time
38+ done
0 commit comments