mathlib incompatibility detected
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: fd066e6 — chore: make trivial definitions unfold (#525) (2026-04-30 (Eric Wieser)).
You can reproduce this break by:
- updating the
mathlib rev field in your lakefile to 6cf3ab1c11e19e328c2e535bdd32d66dc7842fb5
- running
lake update mathlib
- running
lake build
downstream-reports reported at 2026-05-02T16:29:15Z · Workflow run · Job log
This issue was last updated on 2026-05-02 by this workflow run. It is maintained automatically by downstream-reports/track-incompatibility. When the incompatibility is resolved, the issue is closed automatically with a comment.
mathlib incompatibility detected
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
mathlibwithout breaking.First incompatible mathlib commit:
6cf3ab1— chore: make argument inzero_le/one_leimplicit (#38148) (2026-04-29 (Violeta Hernández Palacios)).Last-known-good mathlib commit:
6727686— ci(olean_report): uselake envinstead oflake execto invoke cache binary (#38712) (2026-04-29 (Bryan Gin-ge Chen))Verified when
leanprover/cslibwas at:fd066e6— chore: make trivial definitions unfold (#525) (2026-04-30 (Eric Wieser)).You can reproduce this break by:
mathlibrevfield in yourlakefileto6cf3ab1c11e19e328c2e535bdd32d66dc7842fb5lake update mathliblake builddownstream-reports reported at 2026-05-02T16:29:15Z · Workflow run · Job log
This issue was last updated on 2026-05-02 by this workflow run. It is maintained automatically by downstream-reports/track-incompatibility. When the incompatibility is resolved, the issue is closed automatically with a comment.