Skip to content

Commit 24cb101

Browse files
authored
ci(weekly-lints): pass the build status to the Zulip report (#881)
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 build` and pass it through, as in [the corresponding Mathlib PR](leanprover-community/mathlib4#43551).
1 parent d4ca8e7 commit 24cb101

1 file changed

Lines changed: 7 additions & 1 deletion

File tree

.github/workflows/weekly-lints.yml

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,14 +51,20 @@ jobs:
5151
working-directory: ${{ github.workspace }}/${{ env.CSLIB }}
5252
continue-on-error: true
5353
run: |
54+
# The default step shell is `bash -e` without `pipefail`, so the status of
55+
# `lake build | tee` would be tee's. Make the pipeline report lake's instead.
56+
set -o pipefail
5457
lean_outfile=$(mktemp)
55-
(lake build || true) 2>&1 | tee "${lean_outfile}"
58+
build_status=0
59+
lake build 2>&1 | tee "${lean_outfile}" || build_status=$?
60+
if [ "${build_status}" -eq 0 ]; then build_success=true; else build_success=false; fi
5661
5762
# Process output for posting to Zulip
5863
SHA=${{ github.sha }} \
5964
REPO=${{ github.repository }} \
6065
RUN_ID=${{ github.run_id }} \
6166
INFO=true \
67+
SUCCESS="${build_success}" \
6268
"${CI_SCRIPTS_DIR}/reporting/zulip_build_report.sh" "${lean_outfile}" > "${GITHUB_OUTPUT}"
6369
6470
- name: Post output to Zulip

0 commit comments

Comments
 (0)