tomevault-io Nightly Testing
Lean 4 publishes nightly toolchain builds from master. Batteries and Mathlib each have a nightly-testing branch that tracks these nightlies and runs CI against them. When CI passes, a nightly-testing-YYYY-MM-DD tag is created. When it fails, fixes are needed before the new toolchain can be adopted.
The mathlib4-nightly-testing Fork
Mathlib's nightly testing lives in a separate fork: leanprover-community/mathlib4-nightly-testing, not on the main leanprover-community/mathlib4 repo. This keeps experimental toolchain branches out of the main repository. When Lean PRs affect Mathlib, lean-pr-testing-NNNN branches are created here automatically.
Key Branches
nightly-testing— tracks the latest Lean nightly. CI runs here determine whether a nightly is usable.nightly-with-mathlib— points to the latest nightly that passes Mathlib CI. Lean PRs that may affect downstream should base off this branch.bump/v4.X.Y— accumulates reviewed adaptations for an upcoming Lean release. Adaptation PRs mergenightly-testingchanges into this branch, andmasteris regularly merged in during release cycles.lean-pr-testing-NNNN— created automatically to test specific Lean PRs against Mathlib.
Zulip
https://leanprover.zulipchat.com/#narrow/channel/nightly-testing has up-to-date status on nightly builds, failures, and adaptation work.
Full Details
The canonical reference for branch and tag conventions across lean4, Batteries, and Mathlib is: https://leanprover-community.github.io/contribute/tags_and_branches.html. If you are asked to work on nightly-testing, or lean-pr-testing-NNNN branches, you should read that page.
Source: leanprover/skills — distributed by TomeVault.