Commit 2023-11-27 11:28 c1f4e113

View on Github →

chore: update the nightly-with-mathlib branch at leanprover/lean4 (#8628) This should result in the nightly-with-mathlib branch at leanprover/lean4 always being:

  • the latest commit which was released as a nightly nightly-YYYY-MM-DD
  • on which Mathlib CI has completed, using the nightly-testing branch
  • and hence Mathlib has a nightly-testing-YYYY-MM-DD branch using that nightly. If this works as planned, nightly-with-mathlib will become the new recommended base branch for Lean PRs that require Mathlib testing. (It will still work if you base off nightly, you might just get a message about Mathlib not being ready. And if you base off master you might get a message about needing to rebase to get Mathlib testing.)

Estimated changes