Skip to content

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

Draft
jessealama wants to merge 5 commits into
leanprover:mainfrom
jessealama:ci/nightly-bump-bash
Draft

jessealama wants to merge 5 commits into
leanprover:mainfrom
jessealama:ci/nightly-bump-bash

Conversation

@jessealama

@jessealama jessealama commented Sep 23, 2026 •

Copy link
Copy Markdown
Contributor

A few github-script steps query the GitHub API to list branches and read a file, wrapped in a retry loop to guard against potential network flakiness. These queries aren't necessary because the job fully checks out the repository. The bump branches and their lean-toolchain are already present.

This PR replaces inline JS with short bash steps built on git show-ref, git for-each-ref, git rev-parse and git show. Step IDs, names, and outputs are unchanged.

A side benefit is that actionlint now makes the bash steps visible to shellcheck. The inline JavaScript wasn't linted, which is how the new Exception bug fixed in #914 got through.

Stacked on #914.

@jessealama

Copy link
Copy Markdown
Contributor Author

Converting this to draft because this kind of report is probably going to be obsolete soon.

@jessealama
jessealama marked this pull request as draft September 29, 2026 14:46
…p branch exists

The "Exit if matching branch exists" step ran `exit 0`, which only ends that
step, so the two following github-script steps ran unguarded. If no
bump/v4.x.0 branch existed, the first of them threw and the `if: failure()`
Zulip warning posted a misleading message about a toolchain pattern mismatch.

Drop the no-op step and guard both fetch steps on the branch check, matching
every later step. Post a dedicated Zulip warning when no bump/v4.x.0 branch is
found, and only post the pattern-mismatch warning when the toolchain fetch step
itself failed. Also replace `new Exception`, which is a ReferenceError in
JavaScript, with `new Error`.
… reasons

Narrowing the toolchain warning to `steps.bump_version.outcome == 'failure'`
left every other step in the job (app token, checkout, tag update, Zulip status
post, branch check, PR creation setup) with no notification at all. Add a final
catch-all step that posts a generic warning with a link to the run whenever the
job fails or is cancelled and neither of the two dedicated warnings fired.

Both `latest_bump_branch` and `bump_version` can fail for several reasons, but
their warnings named a single cause. Record a `reason` output at each failure
point in the scripts and include it in the warning, and reword the step names
and messages so they no longer claim more than the script actually determined.
The three steps that look for the bump branches and read the bump branch
toolchain used the GitHub API from inline JavaScript. The job already
checks out the repository with full depth, so the same information is
available from the local remote-tracking refs. Replace the JavaScript
with short bash steps that use git show-ref, git for-each-ref and git
show. The step ids and output names are unchanged, so the steps that
consume them are untouched.

The retry loop is dropped since nothing hits the network anymore, and
these steps no longer need the API token. The inline JavaScript was also
the only inline code in the workflow that no linter covered, since
actionlint already runs shellcheck over run steps.
Split the pipeline and grouped echoes in the two bash steps into
separate commands, so that a failed branch listing, a missing bump
branch, an unreadable or empty lean-toolchain, and a toolchain that
doesn't match the nightly pattern each record their own reason for the
Zulip warnings, as the github-script versions did.
git for-each-ref can filter, version-sort and limit the bump branches
itself, which replaces the grep/sort/tail chain with a single command.
Also drop the fail() helper and the separate empty-file check: an empty
lean-toolchain now fails the pattern check, and the warning still shows
its content as "(empty)".
@jessealama
jessealama force-pushed the ci/nightly-bump-bash branch from bac6c9b to 91e5d50 Compare October 5, 2026 03:02
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant