max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix awaiting-mathlib.yml (#8480)

Browse source 
This PR hopefully fixes a problem from #8471, which even the most
cursory testing (by me!) should have detected.
This commit is contained in:
Kim Morrison 2025-05-26 12:13:00 +10:00 • committed by GitHub
parent 03e905d994
commit c1866a7b7e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 13 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
.github/workflows/awaiting-mathlib.yml vendored
View file

@ -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