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: 8319c83 — refactor(MeasureTheory): define eLpNorm f to be infinite when not AEStronglyMeasurable (#42406) (2026-09-11 (Felix Pernegger)).
Last-known-good mathlib commit: 5089c57 — chore: simplify proofs with grind (#41903) (2026-09-11 (Felix Pernegger))
Verified when LeanMachineLearning/LML was at: dde3322 — bump referee (2026-09-16 (Remy Degenne)).
You can reproduce this break by:
- updating
mathlib to 8319c83af32e262ad477c8a896a0859cdd061b16
- running
lake update mathlib
- running
lake build
downstream-reports reported at 2026-09-22T00:28:18Z · Workflow run · Job log · Failure log
This issue was last updated on 2026-09-22 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:
8319c83— refactor(MeasureTheory): defineeLpNorm fto be infinite when notAEStronglyMeasurable(#42406) (2026-09-11 (Felix Pernegger)).Last-known-good mathlib commit:
5089c57— chore: simplify proofs withgrind(#41903) (2026-09-11 (Felix Pernegger))Verified when
LeanMachineLearning/LMLwas at:dde3322— bump referee (2026-09-16 (Remy Degenne)).You can reproduce this break by:
mathlibto8319c83af32e262ad477c8a896a0859cdd061b16lake update mathliblake builddownstream-reports reported at 2026-09-22T00:28:18Z · Workflow run · Job log · Failure log
This issue was last updated on 2026-09-22 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.