This dashboard answers these questions about projects that depend on mathlib4:
- How far behind is the dependency revision? A scheduled workflow builds each registered downstream against the most recent mathlib commit (the target). The age column shows how many commits your pinned revision lags behind it.
- Which commit introduced the incompatibility? When the downstream is incompatible with the target, we run hopscotch to scan the mathlib history between the pinned revision and the target, to identify the first known bad commit — the earliest Mathlib revision incompatible with the downstream — and the last known good commit just before it.
- How much can I safely advance the dependency? The last known good commit is a safe upgrade target. The bump column shows the distance between it and the currently pinned revision.
Glossary
| Downstream | Pinned to | Age | Target | Compatibility | Last known good | First known bad | Bump | Last good release | Links |
|---|---|---|---|---|---|---|---|---|---|
| v4.31.0 | 3d (+113) | v4.32.0-rc1 | compatible checked 2026-07-11 | v4.32.0-rc1 | — | +113 | v4.32.0-rc1 (+113) | ||
add-combi builds successfully against Mathlib v4.32.0-rc1. Its pin can be safely advanced by 113 commits to the last known good revision v4.32.0-rc1. Mathlib commit window (older → newer) Last checked2026-07-11 16:39 UTC ()Validation took16sHow it was checkedSkipped — this exact project revision was already validated as compatible with this Mathlib revision in a previous run | |||||||||
| 4aaa962 | 8d (+152) | 4efb186 | compatible checked 2026-07-11 | 4efb186 | — | +152 | v4.32.0-rc1 (-421) | ||
| 6130385 | 7d (+136) | 4efb186 | incompatible checked 2026-07-11 | 8f56b70 | e3b7382 | +111 | v4.32.0-rc1 (-437) | ||
BrauerGroup fails to build against Mathlib 4efb186. The incompatibility was introduced by Mathlib commit e3b7382 (“fix(RingTheory/TwoSidedIdeal/Basic): remove instance with bad outParam (#40718)”). The commit immediately before it, 8f56b70, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-07-11 16:39 UTC ()Validation took6m 51sHow it was checkedDirect build of the target revision; it matches a previously identified incompatibility, so the known good/bad boundary from the earlier bisect is shownFailed during lake build | |||||||||
| v4.31.0 | 3d (+113) | v4.32.0-rc1 | compatible checked 2026-07-11 | v4.32.0-rc1 | — | +113 | v4.32.0-rc1 (+113) | ||
cam-combi builds successfully against Mathlib v4.32.0-rc1. Its pin can be safely advanced by 113 commits to the last known good revision v4.32.0-rc1. Mathlib commit window (older → newer) Last checked2026-07-11 16:39 UTC ()Validation took17sHow it was checkedSkipped — this exact project revision was already validated as compatible with this Mathlib revision in a previous run | |||||||||
| 1a4917a | 25d (+723) | v4.30.0 | incompatible checked 2026-07-11 | e6a5fb0 | a18abbe | +4 | v4.30.0-rc2 (-420) | ||
carleson fails to build against Mathlib v4.30.0. The incompatibility was introduced by Mathlib commit a18abbe (“feat: lemmas about liminf multiplied by a constant (#37311)”). The commit immediately before it, e6a5fb0, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-07-11 16:39 UTC ()Validation took2m 34sHow it was checkedDirect build of the target revision; it matches a previously identified incompatibility, so the known good/bad boundary from the earlier bisect is shownFailed during lake build | |||||||||
| v4.31.0 | 3d (+113) | v4.32.0-rc1 | compatible checked 2026-07-11 | v4.32.0-rc1 | — | +113 | v4.32.0-rc1 (+113) | ||
chandra-furst-lipton builds successfully against Mathlib v4.32.0-rc1. Its pin can be safely advanced by 113 commits to the last known good revision v4.32.0-rc1. Mathlib commit window (older → newer) Last checked2026-07-11 16:39 UTC ()Validation took17sHow it was checkedSkipped — this exact project revision was already validated as compatible with this Mathlib revision in a previous run | |||||||||
| 23b0068 | 5d (+133) | v4.31.0 | compatible checked 2026-07-11 | v4.31.0 | — | +133 | v4.31.0 (+133) | ||
ClassFieldTheory builds successfully against Mathlib v4.31.0. Its pin can be safely advanced by 133 commits to the last known good revision v4.31.0. Last checked2026-07-11 16:39 UTC ()Validation took17sHow it was checkedSkipped — this exact project revision was already validated as compatible with this Mathlib revision in a previous run | |||||||||
| master-2026-07-11 | 0d (+2) | 4efb186 | compatible checked 2026-07-11 | 4efb186 | — | +2 | v4.32.0-rc1 (-571) | ||
compfiles builds successfully against Mathlib 4efb186. Its pin can be safely advanced by 2 commits to the last known good revision 4efb186. Mathlib commit window (older → newer) Last checked2026-07-11 16:39 UTC ()Validation took4m 41sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| d52d26f | 10d (+238) | 4efb186 | compatible checked 2026-07-11 | 4efb186 | — | +238 | v4.32.0-rc1 (-335) | ||
cslib builds successfully against Mathlib 4efb186. Its pin can be safely advanced by 238 commits to the last known good revision 4efb186. Last checked2026-07-11 16:39 UTC ()Validation took2m 48sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| master-2026-06-22 | 19d (+492) | 4efb186 | compatible checked 2026-07-11 | 4efb186 | — | +492 | v4.32.0-rc1 (-81) | ||
DynamicalSystems builds successfully against Mathlib 4efb186. Its pin can be safely advanced by 492 commits to the last known good revision 4efb186. Mathlib commit window (older → newer) Last checked2026-07-11 16:39 UTC ()Validation took2m 16sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| 0be66d7 | 0d (+4) | v4.31.0 | compatible checked 2026-07-11 | v4.31.0 | — | +4 | v4.31.0 (+4) | ||
ErdosUnitDistance builds successfully against Mathlib v4.31.0. Its pin can be safely advanced by 4 commits to the last known good revision v4.31.0. Last checked2026-07-11 16:39 UTC ()Validation took16sHow it was checkedSkipped — this exact project revision was already validated as compatible with this Mathlib revision in a previous run | |||||||||
| master-2026-07-10 | 1d (+19) | 4efb186 | compatible checked 2026-07-11 | 4efb186 | — | +19 | v4.32.0-rc1 (-554) | ||
FLT builds successfully against Mathlib 4efb186. Its pin can be safely advanced by 19 commits to the last known good revision 4efb186. Mathlib commit window (older → newer) Last checked2026-07-11 16:39 UTC ()Validation took4m 53sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| acad6f4 | 2d (+35) | 4efb186 | compatible checked 2026-07-11 | 4efb186 | — | +35 | v4.32.0-rc1 (-538) | ||
flt-regular builds successfully against Mathlib 4efb186. Its pin can be safely advanced by 35 commits to the last known good revision 4efb186. Last checked2026-07-11 16:39 UTC ()Validation took1m 59sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| v4.31.0 | 3d (+113) | v4.32.0-rc1 | compatible checked 2026-07-11 | v4.32.0-rc1 | — | +113 | v4.32.0-rc1 (+113) | ||
forbidden-matrix builds successfully against Mathlib v4.32.0-rc1. Its pin can be safely advanced by 113 commits to the last known good revision v4.32.0-rc1. Mathlib commit window (older → newer) Last checked2026-07-11 16:39 UTC ()Validation took17sHow it was checkedSkipped — this exact project revision was already validated as compatible with this Mathlib revision in a previous run | |||||||||
| v4.31.0 | 3d (+113) | v4.32.0-rc1 | compatible checked 2026-07-11 | v4.32.0-rc1 | — | +113 | v4.32.0-rc1 (+113) | ||
gibbs-measure builds successfully against Mathlib v4.32.0-rc1. Its pin can be safely advanced by 113 commits to the last known good revision v4.32.0-rc1. Mathlib commit window (older → newer) Last checked2026-07-11 16:39 UTC ()Validation took18sHow it was checkedSkipped — this exact project revision was already validated as compatible with this Mathlib revision in a previous run | |||||||||
| v4.32.0-rc1-patch1 | 12d (+317) | 4efb186 | incompatible checked 2026-07-11 | 8df0e1b | 2f35248 | +272 | v4.32.0-rc1 (-256) | ||
hex-dev fails to build against Mathlib 4efb186. The incompatibility was introduced by Mathlib commit 2f35248 (“refactor(Algebra): weaken NormalizationMonoid (#34179)”). The commit immediately before it, 8df0e1b, still works and is a safe upgrade target. Mathlib commit window (older → newer) v4.32.0-rc1-patch1pinned 272 commits 8df0e1blast known good 2f35248first known bad 44 commits 4efb186target Last checked2026-07-11 16:39 UTC ()Validation took30m 17sHow it was checkedFull bisect — the Mathlib commit window was searched in this run to pinpoint the exact breaking commitFailed during lake build | |||||||||
| 89a18ed | 1d (+26) | 4efb186 | compatible checked 2026-07-11 | 4efb186 | — | +26 | v4.32.0-rc1 (-547) | ||
HighlyAbundant builds successfully against Mathlib 4efb186. Its pin can be safely advanced by 26 commits to the last known good revision 4efb186. Last checked2026-07-11 16:39 UTC ()Validation took2m 25sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| 89a18ed | 1d (+26) | 4efb186 | incompatible checked 2026-07-11 | 89a18ed | 8f56b70 | — | v4.32.0-rc1 (-547) | ||
infinity-cosmos fails to build against Mathlib 4efb186. The incompatibility was introduced by Mathlib commit 8f56b70 (“feat(AlgebraicTopology/SimplicialSet): define isomorphisms in simplicial sets, and the coherent isomorphism simplicial set (#35287)”). The commit immediately before it, 89a18ed, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-07-11 16:39 UTC ()Validation took1m 48sHow it was checkedDirect build of the target revision; it matches a previously identified incompatibility, so the known good/bad boundary from the earlier bisect is shownFailed during lake build | |||||||||
| v4.30.0-rc1 | 13d (+420) | v4.30.0-rc2 | incompatible checked 2026-07-11 | cb39573 | ff51775 | +412 | v4.30.0-rc1 | ||
LeanDownstreamPlayground fails to build against Mathlib v4.30.0-rc2. The incompatibility was introduced by Mathlib commit ff51775 (“chore(AlgebraicTopology): rename `SingularHomology.HomotopyInvarianceTopCat` (#37658)”). The commit immediately before it, cb39573, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-07-11 16:39 UTC ()Validation took1m 37sHow it was checkedDirect build of the target revision; it matches a previously identified incompatibility, so the known good/bad boundary from the earlier bisect is shownFailed during lake build | |||||||||
| e039464 | 0d (+8) | 4efb186 | compatible checked 2026-07-11 | 4efb186 | — | +8 | v4.32.0-rc1 (-565) | ||
LeanMachineLearning builds successfully against Mathlib 4efb186. Its pin can be safely advanced by 8 commits to the last known good revision 4efb186. Last checked2026-07-11 16:39 UTC ()Validation took2m 28sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| v4.31.0 | 3d (+113) | v4.32.0-rc1 | compatible checked 2026-07-11 | v4.32.0-rc1 | — | +113 | v4.32.0-rc1 (+113) | ||
misc-yd builds successfully against Mathlib v4.32.0-rc1. Its pin can be safely advanced by 113 commits to the last known good revision v4.32.0-rc1. Mathlib commit window (older → newer) Last checked2026-07-11 16:39 UTC ()Validation took16sHow it was checkedSkipped — this exact project revision was already validated as compatible with this Mathlib revision in a previous run | |||||||||
| v4.31.0 | 3d (+113) | v4.32.0-rc1 | compatible checked 2026-07-11 | v4.32.0-rc1 | — | +113 | v4.32.0-rc1 (+113) | ||
PersistentDecomp builds successfully against Mathlib v4.32.0-rc1. Its pin can be safely advanced by 113 commits to the last known good revision v4.32.0-rc1. Mathlib commit window (older → newer) Last checked2026-07-11 16:39 UTC ()Validation took17sHow it was checkedSkipped — this exact project revision was already validated as compatible with this Mathlib revision in a previous run | |||||||||
| af2f0a4 | 9d (+194) | 4efb186 | compatible checked 2026-07-11 | 4efb186 | — | +194 | v4.32.0-rc1 (-379) | ||
| v4.31.0 | 3d (+113) | v4.32.0-rc1 | incompatible checked 2026-07-11 | 50b70b9 | 94fba23 | +5 | v4.31.0 | ||
physlib fails to build against Mathlib v4.32.0-rc1. The incompatibility was introduced by Mathlib commit 94fba23 (“feat(MeasureTheory): use `Is*Apply` for `VectorMeasure` (#40450)”). The commit immediately before it, 50b70b9, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-07-11 16:39 UTC ()Validation took22m 11sHow it was checkedboundary-revalidatedFailed during lake build | |||||||||
| b8dad03 | 5d (+198) | v4.28.0 | compatible checked 2026-07-11 | v4.28.0 | — | +198 | v4.28.0 (+198) | ||
Poly builds successfully against Mathlib v4.28.0. Its pin can be safely advanced by 198 commits to the last known good revision v4.28.0. Last checked2026-07-11 16:39 UTC ()Validation took17sHow it was checkedSkipped — this exact project revision was already validated as compatible with this Mathlib revision in a previous run | |||||||||
| 8df0e1b | 2d (+45) | 4efb186 | compatible checked 2026-07-11 | 4efb186 | — | +45 | v4.32.0-rc1 (-528) | ||
PrimeCert builds successfully against Mathlib 4efb186. Its pin can be safely advanced by 45 commits to the last known good revision 4efb186. Last checked2026-07-11 16:39 UTC ()Validation took1m 45sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| db12779 | 2d (+82) | v4.32.0-rc1 | incompatible checked 2026-07-11 | 5ac7475 | 9d11f4f | +40 | v4.31.0 (-31) | ||
PrimeNumberTheoremAnd fails to build against Mathlib v4.32.0-rc1. The incompatibility was introduced by Mathlib commit 9d11f4f (“feat(Tactic/Positivity): make positivity work for types that are not partial orders (#35394)”). The commit immediately before it, 5ac7475, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-07-11 16:39 UTC ()Validation took5m 37sHow it was checkedDirect build of the target revision; it matches a previously identified incompatibility, so the known good/bad boundary from the earlier bisect is shownFailed during lake build | |||||||||
| v4.31.0 | 3d (+113) | v4.32.0-rc1 | compatible checked 2026-07-11 | v4.32.0-rc1 | — | +113 | v4.32.0-rc1 (+113) | ||
Robo builds successfully against Mathlib v4.32.0-rc1. Its pin can be safely advanced by 113 commits to the last known good revision v4.32.0-rc1. Mathlib commit window (older → newer) Last checked2026-07-11 16:39 UTC ()Validation took18sHow it was checkedSkipped — this exact project revision was already validated as compatible with this Mathlib revision in a previous run | |||||||||
| v4.30.0 | 2d (+108) | v4.31.0-rc1 | incompatible checked 2026-07-11 | a694d67 | v4.31.0-rc1 | +107 | v4.30.0 | ||
Sphere-Packing-Lean fails to build against Mathlib v4.31.0-rc1. The incompatibility was introduced by Mathlib commit v4.31.0-rc1 (“chore: bump toolchain to v4.31.0-rc1 (#39980)”). The commit immediately before it, a694d67, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-07-11 16:39 UTC ()Validation took4m 09sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible)Failed during lake build | |||||||||
| e039464 | 0d (+8) | 4efb186 | compatible checked 2026-07-11 | 4efb186 | — | +8 | v4.32.0-rc1 (-565) | ||
Statlib builds successfully against Mathlib 4efb186. Its pin can be safely advanced by 8 commits to the last known good revision 4efb186. Last checked2026-07-11 16:39 UTC ()Validation took1m 38sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| v4.31.0-rc1 | 10d (+329) | v4.31.0-rc2 | incompatible checked 2026-07-11 | 01cc327 | 89ce8bf | +259 | v4.31.0-rc1 | ||
sum_product fails to build against Mathlib v4.31.0-rc2. The incompatibility was introduced by Mathlib commit 89ce8bf (“feat(Tactic): `convert` discharges side goals reducibly (#39928)”). The commit immediately before it, 01cc327, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-07-11 16:39 UTC ()Validation took5m 53sHow it was checkedDirect build of the target revision; it matches a previously identified incompatibility, so the known good/bad boundary from the earlier bisect is shownFailed during lake build | |||||||||
| faaff5e | 7d (+133) | 4efb186 | incompatible checked 2026-07-11 | ce0dcaa | f4e566c | +21 | v4.32.0-rc1 (-440) | ||
TauCeti fails to build against Mathlib 4efb186. The incompatibility was introduced by Mathlib commit f4e566c (“feat(Algebra/MonoidAlgebra): more general `algHom_ext` (#41412)”). The commit immediately before it, ce0dcaa, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-07-11 16:39 UTC ()Validation took8m 05sHow it was checkedboundary-revalidatedFailed during lake build | |||||||||
| f4e566c | 4d (+111) | 4efb186 | compatible checked 2026-07-11 | 4efb186 | — | +111 | v4.32.0-rc1 (-462) | ||
Toric builds successfully against Mathlib 4efb186. Its pin can be safely advanced by 111 commits to the last known good revision 4efb186. Last checked2026-07-11 16:39 UTC ()Validation took2m 26sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| No downstream matches the current filters. | |||||||||