Skip to content

ci: split build job so post-build chain overlaps test+lint#40233

Draft
bryangingechen wants to merge 1 commit into
masterfrom
ci-dev/split-build-test-lint
Draft

ci: split build job so post-build chain overlaps test+lint#40233
bryangingechen wants to merge 1 commit into
masterfrom
ci-dev/split-build-test-lint

Conversation

@bryangingechen
Copy link
Copy Markdown
Contributor

@bryangingechen bryangingechen commented Jun 4, 2026 •
edited
Loading

Peel test and lint out of the self-hosted build job into a new self-hosted test_lint job, so the GitHub-hosted post-build chain (upload_cache -> post_steps) no longer waits behind the ~300s test+lint tail of build.

  • New test_lint job (self-hosted, needs: [build, upload_cache]): re-does the setup prefix, fetches this run's oleans with cache get + verifies the Mathlib cache is complete (mirrors post_steps), then runs test, lint, and the nightly-testing comment. Its PR-branch checkout is shallow (fetch-depth: 1): unlike build it does no parent-commit cache warmup, so it only needs HEAD.
  • build job: test/lint removed; noisy moved up to right after the Counterexamples build (it only needs the just-built oleans), so it stays in build and test_lint need not fetch Archive/Counterexamples. test/lint outputs move to test_lint.
  • final: now also needs: test_lint and requires its success.

Prepared with Claude code

See also this (LLM-generated) report for more details on how a split like this could improve build times.

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions Bot commented Jun 4, 2026 •
edited
Loading

PR summary 3b6eb1a35c

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff (regex)

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 3b6eb1a35c
Reference commit a91021ae97

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

⚠️ Workflow documentation reminder

This PR modifies files under .github/workflows/.
Please update docs/workflows.md if the workflow inventory, triggers, or behavior changed.

Modified workflow files:

  • .github/workflows/build_template.yml

@github-actions github-actions Bot added the CI Modifies the continuous integration setup or other automation label Jun 4, 2026
@bryangingechen @claude
CI: split build job so post-build chain overlaps test+lint
3b6eb1a 
Peel `test` and `lint` out of the self-hosted `build` job into a new
self-hosted `test_lint` job, so the GitHub-hosted post-build chain
(`upload_cache` -> `post_steps`) no longer waits behind the ~300s test+lint
tail of `build`.

Why
---
`build_template.yml` is a DAG: build -> upload_cache -> post_steps -> final
(plus lint_style in parallel). `upload_cache`/`post_steps` `needs: [build]`, so
they cannot start until the *entire* build job finishes -- including test+lint,
which they do not depend on (they only need the staged oleans, which `build`
uploads as the `cache-staging` artifact ~300s before it runs `test`). With the
recent ~2 min "dump declarations" step added to `post_steps`, that serial
GitHub-hosted chain is now ~349s sitting back-to-back with the ~308s test+lint
tail, though the two are independent.

Splitting `build` at the staging boundary lets `test_lint` and the post-build
chain run in parallel. On the representative warm fork run this cuts the typical
end-to-end contributor wait from ~790s to ~520-580s. Because the overlapped
chain is on free GitHub-hosted runners, the only self-hosted cost is one
re-paid setup+cache-fetch prefix (the fresh `test_lint` runner), and per-run
PEAK pool concurrency is unchanged (build and test_lint run sequentially on the
pool). See the analysis in the companion mathlib4_ci_parallel_simulation study.

What changed
------------
- New `test_lint` job (self-hosted, `needs: [build, upload_cache]`): re-does the
  setup prefix, fetches this run's oleans with `cache get` + verifies the Mathlib
  cache is complete (mirrors `post_steps`), then runs test, lint, and the
  nightly-testing comment. Its PR-branch checkout is shallow (fetch-depth: 1):
  unlike `build` it does no parent-commit cache warmup, so it only needs HEAD.
- `build` job: `test`/`lint` removed; `noisy` moved up to right after the
  Counterexamples build (it only needs the just-built oleans), so it stays in
  `build` and `test_lint` need not fetch Archive/Counterexamples. `test`/`lint`
  outputs move to `test_lint`.
- `final`: now also `needs: test_lint` and requires its success.

Reporting behavior is preserved
-------------------------------
The split reproduces the monolith's per-step gating via the build job's outputs,
so CI reporting is unchanged:
- `test_lint` runs when `build` SUCCEEDED *or* FAILED (not cancelled), so `lint`
  still reports (best-effort, over whatever oleans the cache has) even on a
  failed build -- as it did under the monolith's `if: always()`.
- `test` runs only on a clean build (build + mk_all + archive + counterexamples
  all success), exactly as before (it had no `if:` and was skipped otherwise).
- The cache-completeness check only hard-fails on a successful build; on a failed
  build it is skipped so it does not block lint reporting.
- `final` still requires `build` success, so a failed build fails CI regardless
  of the best-effort lint -- unchanged.
- Minor: on a test/lint failure `post_steps` now still runs (build succeeded), so
  the decls-diff / import-graph artifacts are produced; `final` is still gated on
  `test_lint` success, so overall CI status is unaffected.

To validate in CI
-----------------
- Cache handoff: `test_lint` depends on `upload_cache` and re-fetches from Azure
  (the proven `post_steps` pattern). A follow-up could have it consume the
  `cache-staging` artifact directly (`cache unstage` + `unpack`) to drop the
  ~61s `upload_cache` wait and capture the rest of the latency win; that path
  needs validation before relying on it.
- The duplicated setup prefix between `build` and `test_lint` is a candidate for
  extraction into a shared composite action in a follow-up.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@bryangingechen bryangingechen force-pushed the ci-dev/split-build-test-lint branch from a8267bb to 3b6eb1a Compare June 4, 2026 16:35
@bryangingechen bryangingechen added the LLM-generated PRs with substantial input from LLMs - review accordingly label Jun 4, 2026
@bryangingechen
Copy link
Copy Markdown
Contributor Author

bryangingechen commented Jun 4, 2026

Three test runs:

  1. Warm run (this branch, no source change) — ✅
    Build 1m58s → Test and lint (5m50s) and Post-Build Step (4m49s) ran in
    parallel    ; Upload to cache skipped (no new oleans). End-to-end ~476s vs
    ~681s for the equivalent monolith (≈30% faster).

  2. Changed Mathlib leaf (forces new oleans) — ✅
    Upload to cache ran (56s), and test_lint fetched the freshly-uploaded
    oleans: its get cache + verify the Mathlib cache is complete + test +
    lint steps all passed. Confirms the upload_cache → test_lint handoff.

  3. Intentionally broken Mathlib leaf (build fails) — ❌ (expected)
    Build fails → test_lint still runs lint (best-effort, reported via the
    problem matcher), while verify/test are skipped and Post-Build Step /
    Post-CI job are skipped — i.e. the monolith's lint-on-failure reporting is
    preserved and a failed build still fails CI.

(Comment prepared with Claude code)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

CI Modifies the continuous integration setup or other automation LLM-generated PRs with substantial input from LLMs - review accordingly

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@bryangingechen