You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
Bumping mathlib to 6cf3ab1 would break the build #546
An incompatibility has been detected between this project and recent changes in mathlib.
In other words, this project can't advance to the tip of mathlib without breaking.
First incompatible mathlib commit:6cf3ab1 — chore: make argument in zero_le/one_le implicit (#38148) (2026-04-29 (Violeta Hernández Palacios)).
Last-known-good mathlib commit:6727686 — ci(olean_report): use lake env instead of lake exec to invoke cache binary (#38712) (2026-04-29 (Bryan Gin-ge Chen))
Verified when leanprover/cslib was at:aa62343 — chore: route Zulip notifications to nightly-testing-cslib (#548) (2026-05-05 (Kim Morrison)).
You can reproduce this break by:
updating the mathlibrev field in your lakefile to 6cf3ab1c11e19e328c2e535bdd32d66dc7842fb5
Activity
chore: bump mathlib to 6cf3ab1, fix breaking changes (leanprover#547)
chore: bump mathlib to 6cf3ab1, fix breaking changes (leanprover#547)