Nightly testing
Understanding the Lean/Mathlib nightly testing infrastructure. Use when working on toolchain bumps, adaptation PRs, or investigating nightly CI failures.From its SKILL.md
npx -y skills add leanprover/skills --skill nightly-testingAssembled from the repository path, not quoted from the project. Check it against their README if it does not work.
SKILL.md
1.9 KB, as published. Nobody here has run it
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.