The Lean Github ecosystem #

Documentation of the branches, tags, and CI workflows relevant for making pull requests to Lean, Std, and Mathlib.

• Things you need to know is relevant for everyone
• Tags and branches is for "experts only" who are making or fixing breaking changes in Lean, or who want to understand the inner workings of Mathlib CI.

Things you need to know #

• If you are making a pull request to leanprover/lean4 which may involve breaking changes, please rebase your PR onto the nightly-with-mathlib branch. This will enable combined CI with Mathlib.

• If you are making a pull request to leanprover-community/mathlib4, please ask for "write" access to the repository via the zulip chat, and push your branch to that repo. This will enable Mathlib's .olean cache to include your pull request.

Tags and branches #

leanprover/lean4 #

• Development occurs on the master branch.
• Stable releases and release candidates have tags, e.g. v4.2.0 or v4.3.0-rc1.
  • To use one of these releases in a project, your lean-toolchain file should contain e.g. leanprover/lean4:v4.2.0.
• Stable releases arrive at the end of each month, and are identical to the last release candidate.
• The first release candidate of the next version is released immediately after the stable release.
• Each version has a releases/v4.X.0 feature branch, which may contain
  • additional commits for release notes
  • cherry picked commits from master for critical fixes released via release candidates.
• We make a regular nightly release from master, which has a tag e.g. nightly-2023-11-01 on the leanprover/lean4-nightly repository.
  • To use a nightly release in a project, your lean-toolchain file should contain e.g. leanprover/lean4:nightly-2023-11-01.
• There is a nightly branch on leanprover/lean4 which follows the most recent commit which was used to construct a nightly release.
• Every PR automatically receives a toolchain after it builds successfully. The PR will then have label toolchain-available. To use PR #NNNN in a project, your lean-toolchain file should contain leanprover/lean4-pr-releases:pr-release-NNNN.
• For any PR that potentially affects Std or Mathlib, you should base your PR off the HEAD of the nightly-with-mathlib branch. In that case, a lean-pr-testing-NNNN Mathlib branch is created, described in detail below, and results from this branch are reported via comments in the PR discussion.

leanprover/std4 (aka 'Std') #

• Development occurs on main.
• Std uses the latest stable release or release candidate in its lean-toolchain.
  • Because we release v4.X+1.0-rc1 immediately after releasing v4.X.0, Std is only very briefly on stable releases.
• The first commit on main which uses a new toolchain is tagged with the version number of that toolchain (e.g. v4.2.0).
• There is a branch stable which follows the v4.X.0 tags.
• Std has a branch bump/v4.X.0 for the upcoming stable release of Lean,
  • which contains adaptations for breaking changes that have been approved by the maintainers
  • and which will be using a leanprover-lean4:nightly-YYYY-MM-DD toolchain.
• Std has a branch nightly-testing which
  • uses a recently nightly release (this is updated automatically)
  • has all commits from main merged into it automatically
  • may have any changes from bump/v4.X.0 merged into it manually
  • may have any other commits, including unreviewed ones, required to keep the nightly-testing branch working again recent nightly releases.
• Failures in CI on the nightly-testing are reported by a bot to zulip in the private "Mathlib reviewers" stream.
• Success in CI on the nightly-testing branch results in the creation of a tag nightly-testing-YYYY-MM-DD to match that commit, if this tag does not already exist.
  • Thus if nightly-testing-YYYY-MM-DD exists, we know that on it:
    • the lean-toolchain is leanprover/lean4:nightly-YYYY-MM-DD, and
    • CI succeeds.
• When changes are required to Std to adapt to a breaking change in Lean, you will need to make a branch, and later open a PR from that branch. (Note that the steps below happen automatically at Mathlib, but need to be done manually for Std.)
  • If the change was made in leanprover/lean4#NNNN, then the Std adaptation branch should be called lean-pr-testing-NNNN.
  • The Std adaptation branch should be based off the tag nightly-testing-YYYY-MM-DD where YYYY-MM-DD is the date of the nightly release that your Lean PR is based off.
  • If the nightly-testing-YYYY-MM-DD tag does not yet exist, you will need to wait (and possibly move forward to a subsequent nightly). Contact @semorrison for assistance if needed.
  • Ideally you will push the lean-pr-testing-NNNN branch to the main Std repository; we can provide write access if needed.
  • The lean-toolchain on this branch must contain leanprover/lean4-pr-releases:pr-release-NNNN.
  • You may open a PR from the lean-pr-testing-NNNN branch, either before or after making the required adaptations.
  • When opening the PR, remember to set the base branch to nightly-testing.
  • Please label the PR with the v4.X.0 and 'depends on core changes' labels. (Or ask for this to be done if you don't have write access.)
  • Once the Lean PR has been merged and published in a nightly release, the Std adaptation PR
    • should have its lean-toolchain updated to leanprover/lean4:nightly-YYYY-MM-DD
    • its changes may be merged manually into nightly-testing as needed to keep nightly-testing working (do not change the base and merge the PR, we still need it).
  • Once the Std adaptation PR has been approved, a maintainer will merge it into bump/v4.X.0 (not nightly-testing-YYYY-MM-DD).
• It is always allowed to merge bump/v4.X.0 into nightly-testing, but not conversely. (Changes to bump/v4.X.0 have been reviewed, but changes to nightly-testing may not have been.)
• When it is time to update Std to a new Lean release, hopefully all that is required is to make a new PR consisting of squash merging bump/v4.X.0 to main.

leanprover-community/mathlib4 (aka 'Mathlib') #

• Everything said above about Std applies to Mathlib, except:
  • Development occurs on master.
  • All PRs to Mathlib should be made from branches of the Mathlib repository itself.
    • This is required for Mathlib's .olean caching mechanism.
    • Please ask on the zulip chat for "write" permission to Mathlib. Please write a sentence about your background and plans.
• The nightly-testing-* tags and bump/v4* branches are write protected, so may only be modified via PRs, maintainers, or the relevant bots.
• Note that the nightly-testing branch of Mathlib may use the nightly-testing branch of Std as required.
• Similarly a bump/v4.X.0 branch of Mathlib may use the bump/v4.X.0 branch of Std as required.
• Branches lean-pr-testing-NNNN are automatically created for any Lean PR that passes CI, and is based off a nightly release. (Unlike for Std, where they must be created manually.)
• Mathlib adaptation PRs on lean-pr-testing-NNNN branches may need to change the Std dependency to use a lean-pr-testing-NNNN branch of Std, if Std also experiences breakages.

Combined CI between Lean and Mathlib #

• For every PR to Lean, we attempt to run Mathlib CI against the resulting toolchain.
• For this to work, you will need to rebase your PR onto the nightly-with-mathlib branch. The nightly-with-mathlib branch points to the latest nightly lean release which passes mathlib CI, and for which a nightly-testing-YYYY-MM-DD tag exists on Mathlib (and possibly Std).
• The bot will create a lean-pr-testing-NNNN branch at Mathlib from the nightly-testing-YYYY-MM-DD tag, or push an empty commit to it if it already exists.
• Subsequent CI results from that Mathlib branch will be reported back to the Lean PR in the form of comments.
• If your PR does not branch off a nightly release for which Mathlib builds, a bot will comment on your PR. It will try again whenever you push to your PR.
• If nightly-with-mathlib is too old for your purposes, you can base off nightly, and mathlib CI will commence as soon as that nightly release itself passes the Mathlib CI and you push to the PR.
• It may be the case that that nightly release never passes the Mathlib CI. In that case you may have to wait for nightly-with-mathlib to be updated and rebase onto that.