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: e06eff5 — chore(Data): move some files to Basic (#43176) (2026-08-31 (Yaël Dillies)).
Last-known-good mathlib commit: 3c8e222 — doc(Algebra/Ring/Defs): remove duplicate text in doc-string (#43177) (2026-08-30 (Marsh Ray))
Verified when leanprover/cslib was at: 492d030 — feat(ModalLogic/LambdaCalculus): modal grind set and proof of type safety for simply typed lambda calculus (#840) (2026-08-30 (Fabrizio Montesi)).
You can reproduce this break by:
- updating
mathlib to e06eff5f95374108acfaf19f1ff7473aa7771df2
- running
lake update mathlib
- running
lake build
downstream-reports reported at 2026-08-31T18:18:13Z · Workflow run · Job log · Failure log
This issue was last updated on 2026-08-31 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:
e06eff5— chore(Data): move some files to Basic (#43176) (2026-08-31 (Yaël Dillies)).Last-known-good mathlib commit:
3c8e222— doc(Algebra/Ring/Defs): remove duplicate text in doc-string (#43177) (2026-08-30 (Marsh Ray))Verified when
leanprover/cslibwas at:492d030— feat(ModalLogic/LambdaCalculus): modal grind set and proof of type safety for simply typed lambda calculus (#840) (2026-08-30 (Fabrizio Montesi)).You can reproduce this break by:
mathlibtoe06eff5f95374108acfaf19f1ff7473aa7771df2lake update mathliblake builddownstream-reports reported at 2026-08-31T18:18:13Z · Workflow run · Job log · Failure log
This issue was last updated on 2026-08-31 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.