Skip to content

test(build_report): unit tests for zulip_build_report.py - #73

Draft
jessealama wants to merge 2 commits into
leanprover-community:masterfrom
jessealama:weekly-lint-report-tests
Draft

jessealama wants to merge 2 commits into
leanprover-community:masterfrom
jessealama:weekly-lint-report-tests

Conversation

@jessealama

Copy link
Copy Markdown

These are the tests that were split off from #70, at reviewer request. Stacked on #70, so the diff includes that commit until it merges.

I'm open to feedback on whether unit-testing CI scripts this way is worth it here, or whether the usual small-script-plus-fix-in-production approach is preferred.

@jessealama
jessealama force-pushed the weekly-lint-report-tests branch from 7c12d28 to e8cf37e Compare September 28, 2026 03:04
Add scripts/reporting/zulip_build_report.py, a successor to
zulip_build_report.sh with the same environment-variable contract and
stdout/stderr shape. The shell script is left untouched for the
nightly-testing workflows that still call it.

The script is a thin entry point; the implementation is the
scripts/reporting/build_report/ package, one module per responsibility
(Lake log parsing, report context, Zulip rendering, job-summary
rendering, CLI), following the layout of scripts/zulip/reconcile_emojis.py.

Compared to the shell script it:

- parses whole messages, including continuation lines, Lake's failure
  epilogue, and stderr panic blocks, as Lake actually prints them;
- attributes each message to a linter via the `set_option linter.X
  false` (or `0`) note that logLint appends, keeping the rest visible
  under "(not attributed to a linter)";
- posts a compact Zulip message: the shell script's headline, severity
  bullets, and error/panic tables, plus a per-linter count table instead
  of per-message warning/info tables, with the spoiler tables capped so
  the message stays under Zulip's limit even for a badly broken build;
- writes the full per-occurrence detail to GITHUB_STEP_SUMMARY, one
  section per linter, each row linking to the source at the built commit
  when the file exists in the package directory, budgeted against
  GitHub's 1 MiB cap including what the step already wrote.

The code targets Python 3.8, since the self-hosted runners' Python is not
pinned. Tests follow in a separate PR to keep this one small to review.
Tests in tests/build_report/ use trimmed real logs from a Mathlib and a
CSLib weekly run plus a synthetic failed build; test_build_report.yml
runs them on Python 3.8 (the floor, since the self-hosted runners'
Python is not pinned) and latest.

Split out of the PR that adds the script, at reviewer request, to keep
that one small to review.
@jessealama
jessealama force-pushed the weekly-lint-report-tests branch from e8cf37e to 5d96753 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