ci(weekly-lints): pass the build status to the Zulip report - #881
Conversation
The report script marks a run as succeeded only when the caller sets SUCCESS=true, and this workflow never did, so every weekly report has been posted as failed, even for a clean build with no linter messages. Capture the exit status of `lake build` (the step already runs with `pipefail`) and pass it through, matching how the nightly workflows in mathlib-ci call the same script.
Unspecified `run:` steps use `bash -e {0}` without `pipefail`, so the status
of `lake build | tee` was tee's and `build_status` stayed 0 even on a failed
build. Turn on `pipefail` at the top of the step.
|
@jessealama I see you pushed a new commit. Let me know if you'd like me to run this job from a branch before merging. |
Yeah, please do! I noticed that there was a mismatch in this action and others, in that we don't specify |
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
@jessealama Sorry for the delay, I'm on spotty hotel wifi at the moment. The run that I started seems to have worked as expected. Is this good to merge?
No problem! I'm also a bit delayed, looking around at CI scripts and seeing what else might be lurking here. Yes, I believe this is good to merge. |
3 participants
The report script marks a run with a green checkmark only when the caller sets
SUCCESS=true. This workflow never did: the switch was added to the script in mathlib-ci in March 2026, and the nightly workflows there were updated to set it, but the weekly workflows in Mathlib and CSLib were not. The result is that every weekly report has been posted with a red X, even when the build was clean and had no linter messages.The solution is to just capture the exit status of
lake buildand pass it through, as in the corresponding Mathlib PR.