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

chore: while awaiting-mathlib, show yellow status not red (#8471)

Browse source 
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.
This commit is contained in:
Kim Morrison 2025-05-25 22:38:56 +10:00 • committed by GitHub
parent 2a1354b3cc
commit bdbb659765
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 22 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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.'
}
});
}