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: 0c154d6 — chore: bump toolchain to v4.30.0-rc1 (#37564) (2026-04-04 (Garmelon)).
Last-known-good mathlib commit: 8850ed9 — feat: union/intersection lemmas for DirSupInacc/DirSupClosed (#37639) (2026-04-04 (Violeta Hernández Palacios))
Verified when LeanMachineLearning/LML was at: e4af5f2 — Add AlgorithmDensity (#111) (2026-05-26 (Rémy Degenne)).
You can reproduce this break by:
- updating the
mathlib rev field in your lakefile to 0c154d67103f74be3a0f2c509f72ccbf5be9f2a7
- running
lake update mathlib
- running
lake build
downstream-reports reported at 2026-06-09T07:13:24Z · Workflow run · Job log · Failure log
This issue was last updated on 2026-06-10 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:
0c154d6— chore: bump toolchain to v4.30.0-rc1 (#37564) (2026-04-04 (Garmelon)).Last-known-good mathlib commit:
8850ed9— feat: union/intersection lemmas forDirSupInacc/DirSupClosed(#37639) (2026-04-04 (Violeta Hernández Palacios))Verified when
LeanMachineLearning/LMLwas at:e4af5f2— Add AlgorithmDensity (#111) (2026-05-26 (Rémy Degenne)).You can reproduce this break by:
mathlibrevfield in yourlakefileto0c154d67103f74be3a0f2c509f72ccbf5be9f2a7lake update mathliblake builddownstream-reports reported at 2026-06-09T07:13:24Z · Workflow run · Job log · Failure log
This issue was last updated on 2026-06-10 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.