Skip to content

ci(nightly-testing): guard the bump-branch steps when the nightly bump branch exists - #914

Draft
jessealama wants to merge 2 commits into
leanprover:mainfrom
jessealama:ci/nightly-bump-guards
Draft

jessealama wants to merge 2 commits into
leanprover:mainfrom
jessealama:ci/nightly-bump-guards

Conversation

@jessealama

@jessealama jessealama commented Sep 16, 2026 •

Copy link
Copy Markdown
Contributor

The "Exit if matching branch exists" step did exit 0, which only ends that step. Since a zero exit is a success, the job simply moved on and the subsequent steps ran. When no bump/v4.x.0 branch existed, the first of them threw, and the if: failure() Zulip warning could post a misleading message about a toolchain pattern mismatch, but the real reason was the non-existence of the proper branch.

This PR drops the no-op step and guards both fetch steps on the branch check, as other later step already are. Post a dedicated warning to Zulip when no bump/v4.x.0 branch is found, and only post the toolchain warning when the toolchain fetch step itself failed.

Also replace new Exception, which is a ReferenceError in JavaScript, with new Error. Exception doesn't exist in JS. So, curiously, running this code caused a different kind of exception to be thrown (a ReferenceError for referring to something that doesn't exist), which ended up killing the step as intended, but for the wrong reason.

@kim-em

kim-em commented Sep 23, 2026

Copy link
Copy Markdown
Collaborator

🤖 Claude says:

Narrowing if: failure() to steps.bump_version.outcome == 'failure' silences the steps that run before it. The old blanket warning sat just above Setup for automatic PR creation, so it only ever covered what preceded it: Generate app token, Checkout code, Update the nightly-testing-YYYY-MM-DD branch, Install Zulip API client, Check last message and post if necessary, and check_branch itself. Those got a misleading toolchain message before; now they get nothing. handle_failure doesn't pick them up either, since it keys off workflow_run.conclusion, which is the triggering CI run rather than this job.

Could you add a catch-all as the last step?

    - name: Send warning message on Zulip on any other failure
      if: >-
        (failure() || cancelled())
        && steps.latest_bump_branch.outcome != 'failure'
        && steps.bump_version.outcome != 'failure'

with a generic "the bump job failed before reaching PR creation" body and a link to the run. Skipped steps are fine here, since a skipped step's outcome is skipped and both comparisons hold.

Two things I noticed while reading, neither blocking:

  • Both warnings are less cause-specific than their wording suggests. latest_bump_branch can fail because listBranches errored rather than because no branch matched, and bump_version can fail fetching the branch, fetching the file, or getting empty content, all of which report "pattern doesn't match". Narrowing the if is already an improvement on what was there; exposing a reason from the scripts would finish the job.
  • Pre-existing and separate: handle_failure links ${{ github.sha }}, which on a workflow_run event is the default-branch commit, not the nightly-testing head that failed. It uses github.event.workflow_run.id correctly for the run link, so github.event.workflow_run.head_sha is presumably what was intended for the commit.

@jessealama

Copy link
Copy Markdown
Contributor Author

@kim-em I've added a catch-all as the last step, with your condition as well as a generic message and link. It'll be worth keeping our eye on the message to make sure it's useful and doesn't become recurring spam.

I also take your second point. Both scripts now record a reason output at each point of failure, and the two warnings report it now instead of asserting a single cause.

Agreed the github.sha link in handle_failure should be github.event.workflow_run.head_sha; I'll do that in a separate PR. Thanks!

@chenson2018

Copy link
Copy Markdown
Collaborator

I'm somewhat inclined to not touch this, as it seems we could just go ahead and remove the "CSLib Status Updates" thread completely in favor of the downstrean-lean4 reporting. Would you have any objections to this? Is there any improvements in one of your open PRs that this would end up missing?

@jessealama

Copy link
Copy Markdown
Contributor Author

I'm happy to drop this! I've also been watching the downstream-lean4 stuff and am happy to see things get consolidated.

ctchou pushed a commit to ctchou/cslib that referenced this pull request Sep 23, 2026
…eanprover#939)

On a `workflow_run` event, `github.sha` is the head of the default
branch, not the commit whose CI run failed. The failure message posted
to Zulip therefore linked the wrong commit. Use
`github.event.workflow_run.head_sha` instead, matching the run link,
which already uses `workflow_run.id`.

Pointed out by @kim-em in leanprover#914.
mathlib-bors Bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Sep 25, 2026
`Exception` is not defined in JavaScript, so this `throw` would raise a
`ReferenceError` with a misleading message instead of the intended one.

This is a latent bug: the path is only reached when no `bump/v4.x.0`
branch exists, and no CI run appears to have actually hit it. Cslib
inherited the same line from this workflow and is fixing it in
leanprover/cslib#914.
mathlib-bors Bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Sep 25, 2026
`Exception` is not defined in JavaScript, so `throw new Exception` causes an unintended `ReferenceError` exception to be thrown.

The error is reached only when the bump branch doesn't exist. I couldn't find any CI run that actually hit this issue. The JS code is problematic nonetheless and should be fixed.

NB: CSLib has the same issue. A fix is in leanprover/cslib#914.
@jessealama
jessealama marked this pull request as draft September 29, 2026 14:47
@jessealama

Copy link
Copy Markdown
Contributor Author

Converting to draft while we get acquainted with the new downsteam CI setup. I'll see whether the idea contained in this PR might apply in that setting.

…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.
@jessealama
jessealama force-pushed the ci/nightly-bump-guards branch from c53bf09 to 265899e 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.

3 participants