Skip to content

ci(nightly-testing): replace github-script JS with bash #940

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
jessealama wants to merge 5 commits into
base: main
Choose a base branch
from
Draft

ci(nightly-testing): replace github-script JS with bash #940

Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
f3463b9
ci(nightly-testing): guard the bump-branch steps when the nightly bum…
jessealama Sep 16, 2026
efa2442
ci(nightly-testing): add a catch-all Zulip warning and report failure…
jessealama Sep 23, 2026
5ba90ce
ci(nightly-testing): replace the github-script steps with git commands
jessealama Sep 23, 2026
bf2fba2
ci(nightly-testing): report a distinct reason for each bump-step failure
jessealama Sep 23, 2026
91e5d50
ci(nightly-testing): let git for-each-ref pick the latest bump branch
jessealama Sep 23, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
196 changes: 86 additions & 110 deletions .github/workflows/report_failures_nightly-testing.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -125,126 +125,77 @@ jobs:

- name: Check for matching bump/nightly-YYYY-MM-DD branch
id: check_branch
uses: actions/github-script@60a0d83039c74a4aee543508d2ffcb1c3799cdea # v7.0.1
with:
script: |
const branchName = `bump/nightly-${process.env.NIGHTLY}`;
console.log(`Looking for branch: ${branchName}`);

// Use paginate to get all branches
const branches = await github.paginate(github.rest.repos.listBranches, {
owner: 'leanprover',
repo: 'cslib'
});

const exists = branches.some(branch => branch.name === branchName);
if (exists) {
console.log(`Branch ${branchName} exists.`);
return true;
} else {
console.log(`Branch ${branchName} does not exist.`);
return false;
}
result-encoding: string

- name: Exit if matching branch exists
if: steps.check_branch.outputs.result == 'true'
run: |
echo "Matching bump/nightly-YYYY-MM-DD branch found, no further action needed."
exit 0
branch="bump/nightly-${NIGHTLY}"
if git show-ref --verify --quiet "refs/remotes/origin/${branch}"; then
echo "Branch ${branch} exists."
echo "result=true" >> "${GITHUB_OUTPUT}"
else
echo "Branch ${branch} does not exist."
echo "result=false" >> "${GITHUB_OUTPUT}"
fi

# If the matching bump/nightly-YYYY-MM-DD branch already exists there is nothing left
# to do, so every step from here on is guarded on the check above. (A step that runs
# `exit 0` would only end that step, not the job.)

- name: Fetch latest bump branch name
id: latest_bump_branch
uses: actions/github-script@60a0d83039c74a4aee543508d2ffcb1c3799cdea # v7.0.1
with:
result-encoding: string
script: |
const branches = await github.paginate(github.rest.repos.listBranches, {
owner: 'leanprover',
repo: 'cslib'
});
const bumpBranches = branches
.map(branch => branch.name)
.filter(name => name.match(/^bump\/v4\.\d+\.0$/))
.sort((a, b) => b.localeCompare(a, undefined, {numeric: true, sensitivity: 'base'}));
if (!bumpBranches.length) {
throw new Exception("Did not find any bump/v4.x.0 branch")
}
const latestBranch = bumpBranches[0];
return latestBranch;
if: steps.check_branch.outputs.result == 'false'
run: |
if ! latest="$(git for-each-ref --sort=-version:refname --count=1 --format='%(refname:lstrip=3)' 'refs/remotes/origin/bump/v4.*.0')"; then
echo "reason=Listing the bump/v4.x.0 branches failed" >> "${GITHUB_OUTPUT}"
exit 1
fi
if [[ -z "${latest}" ]]; then
echo "reason=Did not find any bump/v4.x.0 branch" >> "${GITHUB_OUTPUT}"
exit 1
fi
echo "Latest bump branch: ${latest}"
echo "result=${latest}" >> "${GITHUB_OUTPUT}"

- name: Fetch lean-toolchain from latest bump branch
id: bump_version
uses: actions/github-script@60a0d83039c74a4aee543508d2ffcb1c3799cdea # v7.0.1
with:
script: |
const branchName = '${{ steps.latest_bump_branch.outputs.result }}';
let content = '';
let sha = '';

// Get branch SHA first for durable URL
try {
const branchResponse = await github.rest.repos.getBranch({
owner: 'leanprover',
repo: 'cslib',
branch: branchName
});
sha = branchResponse.data.commit.sha;
core.setOutput('branch_sha', sha);
} catch (error) {
core.setFailed(`Failed to get branch SHA for ${branchName}: ${error.message}`);
core.setOutput('branch_name', branchName);
return null;
}

// Retry logic for fetching content (in case of network errors)
const maxRetries = 3;
for (let attempt = 1; attempt <= maxRetries; attempt++) {
try {
const response = await github.rest.repos.getContent({
owner: context.repo.owner,
repo: context.repo.repo,
path: 'lean-toolchain',
ref: branchName
});
content = Buffer.from(response.data.content, 'base64').toString().trim();

if (content) {
break; // Success, exit retry loop
} else if (attempt < maxRetries) {
console.log(`Attempt ${attempt}: lean-toolchain content is empty, retrying...`);
await new Promise(resolve => setTimeout(resolve, 2000)); // Wait 2 seconds
}
} catch (error) {
if (attempt === maxRetries) {
core.setFailed(`Failed to fetch lean-toolchain from ${branchName} after ${maxRetries} attempts: ${error.message}`);
core.setOutput('branch_name', branchName);
return null;
}
console.log(`Attempt ${attempt}: Error fetching lean-toolchain from ${branchName}, retrying... ${error.message}`);
await new Promise(resolve => setTimeout(resolve, 2000)); // Wait 2 seconds
}
}
if: steps.check_branch.outputs.result == 'false'
env:
BUMP_BRANCH: ${{ steps.latest_bump_branch.outputs.result }}
run: |
sha="$(git rev-parse "origin/${BUMP_BRANCH}")"
echo "branch_name=${BUMP_BRANCH}" >> "${GITHUB_OUTPUT}"
echo "branch_sha=${sha}" >> "${GITHUB_OUTPUT}"
if ! content="$(git show "${sha}:lean-toolchain")"; then
echo "reason=Could not read lean-toolchain from ${BUMP_BRANCH}" >> "${GITHUB_OUTPUT}"
exit 1
fi
content="${content//[[:space:]]/}"
echo "toolchain_content=${content:-(empty)}" >> "${GITHUB_OUTPUT}"
if [[ ! "${content}" =~ leanprover/lean4:nightly-([0-9]{4}-[0-9]{2}-[0-9]{2}) ]]; then
echo "reason=lean-toolchain does not match the expected pattern 'leanprover/lean4:nightly-YYYY-MM-DD'" >> "${GITHUB_OUTPUT}"
exit 1
fi
echo "result=${BASH_REMATCH[1]}" >> "${GITHUB_OUTPUT}"

if (!content) {
core.setFailed(`lean-toolchain content is empty after ${maxRetries} attempts from branch ${branchName}`);
core.setOutput('toolchain_content', '(empty)');
core.setOutput('branch_name', branchName);
return null;
}
# Each of the two steps above can fail for more than one reason, so the warnings below
# report the reason the script recorded rather than guessing at a single cause.

core.setOutput('toolchain_content', content);
core.setOutput('branch_name', branchName);
- name: Send warning message on Zulip if the latest bump/v4.x.0 branch could not be determined
if: failure() && steps.latest_bump_branch.outcome == 'failure'
uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
with:
api-key: ${{ secrets.ZULIP_API_KEY }}
email: 'github-mathlib4-bot@leanprover.zulipchat.com'
organization-url: 'https://leanprover.zulipchat.com'
to: 'nightly-testing-cslib'
type: 'stream'
topic: 'Cslib status updates'
content: |
⚠️ Warning: Could not determine the latest `bump/v4.x.0` branch, so no `bump/nightly-${{ env.NIGHTLY }}` PR was opened.

const match = content.match(/leanprover\/lean4:nightly-(\d{4}-\d{2}-\d{2})/);
if (!match) {
core.setFailed('Toolchain pattern did not match');
return null;
}
return match[1];
**Reason:** ${{ steps.latest_bump_branch.outputs.reason || 'unknown (see the run log)' }}
**Run:** https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}

- name: Send warning message on Zulip if pattern doesn't match
if: failure()
- name: Send warning message on Zulip if the bump branch toolchain could not be read
if: failure() && steps.bump_version.outcome == 'failure'
uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
with:
api-key: ${{ secrets.ZULIP_API_KEY }}
Expand All @@ -254,11 +205,13 @@ jobs:
type: 'stream'
topic: 'Cslib status updates'
content: |
⚠️ Warning: The lean-toolchain file in bump branch `${{ steps.bump_version.outputs.branch_name }}` does not match the expected pattern 'leanprover/lean4:nightly-YYYY-MM-DD'.
⚠️ Warning: Could not read a nightly toolchain from bump branch `${{ steps.bump_version.outputs.branch_name }}`, so no `bump/nightly-${{ env.NIGHTLY }}` PR was opened.

**Reason:** ${{ steps.bump_version.outputs.reason || 'unknown (see the run log)' }}
**Branch:** `${{ steps.bump_version.outputs.branch_name }}`
**File URL:** https://github.com/${{ github.repository }}/blob/${{ steps.bump_version.outputs.branch_sha }}/lean-toolchain
**Current content:** `${{ steps.bump_version.outputs.toolchain_content }}`
**Run:** https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}

This needs to be fixed for the nightly testing process to work correctly.

Expand Down Expand Up @@ -397,3 +350,26 @@ jobs:
print(result)
else:
print('No action needed.')

# Catch-all for every other failure in this job: the steps before the branch check
# (app token, checkout, tag update, Zulip status post) and the steps after the two
# warnings above. Without this they would fail silently, since the two warnings above
# only fire for their own step. A skipped step's outcome is 'skipped', so the two
# comparisons below hold whenever those steps did not run.
- name: Send warning message on Zulip on any other failure
if: >-
(failure() || cancelled())
&& steps.latest_bump_branch.outcome != 'failure'
&& steps.bump_version.outcome != 'failure'
uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
with:
api-key: ${{ secrets.ZULIP_API_KEY }}
email: 'github-mathlib4-bot@leanprover.zulipchat.com'
organization-url: 'https://leanprover.zulipchat.com'
to: 'nightly-testing-cslib'
type: 'stream'
topic: 'Cslib status updates'
content: |
⚠️ Warning: The job that checks whether a `bump/nightly-YYYY-MM-DD` PR is needed failed or was cancelled at a step that has no dedicated warning, so it may not have reached PR creation.

**Run:** https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}
Loading