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 |
|---|---|---|---|---|---|---|---|---|---|
| be865aa | 3d (+157) | 52b284f | compatible checked 2026-09-04 | 52b284f | — | +157 | v4.34.0-rc2 (-265) | ||
add-combi builds successfully against Mathlib 52b284f. Its pin can be safely advanced by 157 commits to the last known good revision 52b284f. Last checked2026-09-04 18:41 UTC ()Validation took2m 30sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| v4.34.0-rc2 | 13d (+422) | 52b284f | compatible checked 2026-09-04 | 52b284f | — | +422 | v4.34.0-rc2 | ||
apap builds successfully against Mathlib 52b284f. Its pin can be safely advanced by 422 commits to the last known good revision 52b284f. Mathlib commit window (older → newer) Last checked2026-09-04 18:41 UTC ()Validation took6m 07sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| be629e7 | 1d (+63) | 52b284f | compatible checked 2026-09-04 | 52b284f | — | +63 | v4.34.0-rc2 (-359) | ||
BrauerGroup builds successfully against Mathlib 52b284f. Its pin can be safely advanced by 63 commits to the last known good revision 52b284f. Last checked2026-09-04 18:41 UTC ()Validation took5m 39sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| v4.34.0-rc2 | 13d (+422) | 52b284f | compatible checked 2026-09-04 | 52b284f | — | +422 | v4.34.0-rc2 | ||
cam-combi builds successfully against Mathlib 52b284f. Its pin can be safely advanced by 422 commits to the last known good revision 52b284f. Mathlib commit window (older → newer) Last checked2026-09-04 18:41 UTC ()Validation took2m 16sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| b63493a | 12d (+397) | 52b284f | incompatible checked 2026-09-04 | f1c1e67 | ce084cc | +39 | v4.34.0-rc2 (-25) | ||
carleson fails to build against Mathlib 52b284f. The incompatibility was introduced by Mathlib commit ce084cc (“feat(Topology/MetricSpace): add distance congruence lemmas (#42893)”). The commit immediately before it, f1c1e67, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-09-04 18:41 UTC ()Validation took3m 09sHow 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 | |||||||||
| 23a3216 | 13d (+414) | 52b284f | compatible checked 2026-09-04 | 52b284f | — | +414 | v4.34.0-rc2 (-8) | ||
chandra-furst-lipton builds successfully against Mathlib 52b284f. Its pin can be safely advanced by 414 commits to the last known good revision 52b284f. Last checked2026-09-04 18:41 UTC ()Validation took2m 33sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| 26245e6 | 9d (+135) | v4.33.0-rc2 | compatible checked 2026-09-04 | v4.33.0-rc2 | — | +135 | v4.33.0-rc2 (+135) | ||
ClassFieldTheory builds successfully against Mathlib v4.33.0-rc2. Its pin can be safely advanced by 135 commits to the last known good revision v4.33.0-rc2. Mathlib commit window (older → newer) Last checked2026-09-04 18:41 UTC ()Validation took20sHow it was checkedSkipped — this exact project revision was already validated as compatible with this Mathlib revision in a previous run | |||||||||
| master-2026-08-14 | 7d (+175) | v4.34.0-rc2 | incompatible checked 2026-09-04 | c6d40f2 | 9b36600 | +18 | v4.34.0-rc1 (-146) | ||
compfiles fails to build against Mathlib v4.34.0-rc2. The incompatibility was introduced by Mathlib commit 9b36600 (“chore: lake shake --add-public --keep-implied --keep-prefix --fix (#40343)”). The commit immediately before it, c6d40f2, still works and is a safe upgrade target. Mathlib commit window (older → newer) master-2026-08-14pinned 18 commits c6d40f2last known good 9b36600first known bad 156 commits v4.34.0-rc2target Last checked2026-09-04 18:41 UTC ()Validation took9m 54sHow 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 | |||||||||
| e06eff5 | 4d (+195) | 52b284f | incompatible checked 2026-09-04 | 30a58f7 | 950d270 | +179 | v4.34.0-rc2 (-227) | ||
cslib fails to build against Mathlib 52b284f. The incompatibility was introduced by Mathlib commit 950d270 (“feat(TacticAnalysis): suggest `rwa` for `rw` followed by `assumption` (#42732)”). The commit immediately before it, 30a58f7, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-09-04 18:41 UTC ()Validation took27m 29sHow it was checkedFull bisect — the Mathlib commit window was searched in this run to pinpoint the exact breaking commitFailed during lake build | |||||||||
| d9f6d18 | 8d (+267) | 52b284f | compatible checked 2026-09-04 | 52b284f | — | +267 | v4.34.0-rc2 (-155) | ||
DirichletProblem builds successfully against Mathlib 52b284f. Its pin can be safely advanced by 267 commits to the last known good revision 52b284f. Last checked2026-09-04 18:41 UTC ()Validation took2m 59sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| v4.34.0-rc2 | 13d (+422) | 52b284f | compatible checked 2026-09-04 | 52b284f | — | +422 | v4.34.0-rc2 | ||
DynamicalSystems builds successfully against Mathlib 52b284f. Its pin can be safely advanced by 422 commits to the last known good revision 52b284f. Mathlib commit window (older → newer) Last checked2026-09-04 18:41 UTC ()Validation took3m 07sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
detached | 37d (+1248) | 52b284f | incompatible checked 2026-09-04 | — | 39c86ed | — | — | ||
ErdosUnitDistance fails to build against Mathlib 52b284f. The earliest known incompatible Mathlib commit is 39c86ed (“feat(NumberTheory/NumberField/AdeleRing): define the idele class group (#40735)”). Last checked2026-09-04 18:41 UTC ()Validation took3m 54sHow 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⚠ The pinned revision is not an ancestor of the target, so no commit window could be searched — only the target itself was validated. | |||||||||
| c4a007f | 1d (+53) | 52b284f | incompatible checked 2026-09-04 | 5390e8a | c692832 | +11 | v4.34.0-rc2 (-369) | ||
FLT fails to build against Mathlib 52b284f. The incompatibility was introduced by Mathlib commit c692832 (“chore(GroupTheory): make arguments implicit in two iff lemmas (#43382)”). The commit immediately before it, 5390e8a, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-09-04 18:41 UTC ()Validation took1h 03mHow it was checkedFull bisect — the Mathlib commit window was searched in this run to pinpoint the exact breaking commitFailed during lake build | |||||||||
| 1ed178f | 3d (+156) | 52b284f | compatible checked 2026-09-04 | 52b284f | — | +156 | v4.34.0-rc2 (-266) | ||
flt-regular builds successfully against Mathlib 52b284f. Its pin can be safely advanced by 156 commits to the last known good revision 52b284f. Last checked2026-09-04 18:41 UTC ()Validation took2m 59sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| v4.34.0-rc2 | 13d (+422) | 52b284f | compatible checked 2026-09-04 | 52b284f | — | +422 | v4.34.0-rc2 | ||
forbidden-matrix builds successfully against Mathlib 52b284f. Its pin can be safely advanced by 422 commits to the last known good revision 52b284f. Mathlib commit window (older → newer) Last checked2026-09-04 18:41 UTC ()Validation took2m 42sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| fa6385b | 4d (+171) | 52b284f | compatible checked 2026-09-04 | 52b284f | — | +171 | v4.34.0-rc2 (-251) | ||
gibbs-measure builds successfully against Mathlib 52b284f. Its pin can be safely advanced by 171 commits to the last known good revision 52b284f. Last checked2026-09-04 18:41 UTC ()Validation took2m 25sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| v4.34.0-rc2 | 13d (+422) | 52b284f | incompatible checked 2026-09-04 | b87b4e8 | master-2026-08-30 | +212 | v4.34.0-rc2 | ||
hex-dev fails to build against Mathlib 52b284f. The incompatibility was introduced by Mathlib commit master-2026-08-30 (“feat(RingTheory/PowerSeries/Log): log and exp as inverses (#37848)”). The commit immediately before it, b87b4e8, still works and is a safe upgrade target. Mathlib commit window (older → newer) v4.34.0-rc2pinned 212 commits b87b4e8last known good master-2026-08-30first known bad 209 commits 52b284ftarget Last checked2026-09-04 18:41 UTC ()Validation took18m 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.33.0 | 11d (+1) | v4.33.1 | compatible checked 2026-09-04 | v4.33.1 | — | +1 | v4.33.1 (+1) | ||
HighlyAbundant builds successfully against Mathlib v4.33.1. Its pin can be safely advanced by 1 commit to the last known good revision v4.33.1. Last checked2026-09-04 18:41 UTC ()Validation took18sHow it was checkedSkipped — this exact project revision was already validated as compatible with this Mathlib revision in a previous run | |||||||||
| 1fe0a51 | 2d (+33) | v4.34.0-rc2 | compatible checked 2026-09-04 | v4.34.0-rc2 | — | +33 | v4.34.0-rc2 (+33) | ||
infinity-cosmos builds successfully against Mathlib v4.34.0-rc2. Its pin can be safely advanced by 33 commits to the last known good revision v4.34.0-rc2. Mathlib commit window (older → newer) Last checked2026-09-04 18:41 UTC ()Validation took20sHow it was checkedSkipped — this exact project revision was already validated as compatible with this Mathlib revision in a previous run | |||||||||
| cf65d43 | 11d (+386) | 52b284f | incompatible checked 2026-09-04 | aac7f62 | 8819c75 | +52 | v4.34.0-rc2 (-36) | ||
LeanMachineLearning fails to build against Mathlib 52b284f. The incompatibility was introduced by Mathlib commit 8819c75 (“feat: `withDensity` of compositions of kernels and measures (#41192)”). The commit immediately before it, aac7f62, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-09-04 18:41 UTC ()Validation took1h 25mHow it was checkedFull bisect — the Mathlib commit window was searched in this run to pinpoint the exact breaking commitFailed during lake build | |||||||||
| 05322f9 | 6d (+218) | 52b284f | compatible checked 2026-09-04 | 52b284f | — | +218 | v4.34.0-rc2 (-204) | ||
mean-fourier builds successfully against Mathlib 52b284f. Its pin can be safely advanced by 218 commits to the last known good revision 52b284f. Last checked2026-09-04 18:41 UTC ()Validation took2m 42sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| v4.34.0-rc2 | 13d (+422) | 52b284f | compatible checked 2026-09-04 | 52b284f | — | +422 | v4.34.0-rc2 | ||
misc-yd builds successfully against Mathlib 52b284f. Its pin can be safely advanced by 422 commits to the last known good revision 52b284f. Mathlib commit window (older → newer) Last checked2026-09-04 18:41 UTC ()Validation took2m 26sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| v4.34.0-rc2 | 13d (+422) | 52b284f | compatible checked 2026-09-04 | 52b284f | — | +422 | v4.34.0-rc2 | ||
PersistentDecomp builds successfully against Mathlib 52b284f. Its pin can be safely advanced by 422 commits to the last known good revision 52b284f. Mathlib commit window (older → newer) Last checked2026-09-04 18:41 UTC ()Validation took2m 15sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| fa6385b | 4d (+171) | 52b284f | compatible checked 2026-09-04 | 52b284f | — | +171 | v4.34.0-rc2 (-251) | ||
| v4.33.0 | 11d (+1) | v4.33.1 | incompatible checked 2026-09-04 | — | v4.33.1 | — | — | ||
physlib fails to build against Mathlib v4.33.1. The earliest known incompatible Mathlib commit is v4.33.1 (“chore: bump toolchain to v4.33.1”). Mathlib commit window (older → newer) Last checked2026-09-04 18:41 UTC ()Validation took20m 15sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible)Failed during lake build | |||||||||
| b8dad03 | 5d (+198) | v4.28.0 | compatible checked 2026-09-04 | 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-09-04 18:41 UTC ()Validation took28sHow it was checkedSkipped — this exact project revision was already validated as compatible with this Mathlib revision in a previous run | |||||||||
| v4.33.0 | 11d (+1) | v4.33.1 | compatible checked 2026-09-04 | v4.33.1 | — | +1 | v4.33.1 (+1) | ||
PrimeCert builds successfully against Mathlib v4.33.1. Its pin can be safely advanced by 1 commit to the last known good revision v4.33.1. Last checked2026-09-04 18:41 UTC ()Validation took30sHow it was checkedSkipped — this exact project revision was already validated as compatible with this Mathlib revision in a previous run | |||||||||
detached | 37d (+1248) | 52b284f | incompatible checked 2026-09-04 | — | 1f8806b | — | — | ||
PrimeNumberTheoremAnd fails to build against Mathlib 52b284f. The earliest known incompatible Mathlib commit is 1f8806b (“fix: adaptations for batteries #1927 (#42229)”). Last checked2026-09-04 18:41 UTC ()Validation took5m 47sHow 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⚠ The pinned revision is not an ancestor of the target, so no commit window could be searched — only the target itself was validated. | |||||||||
| v4.31.0 | 3d (+113) | v4.32.0-rc1 | compatible checked 2026-09-04 | 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-09-04 18:41 UTC ()Validation took25sHow it was checkedSkipped — this exact project revision was already validated as compatible with this Mathlib revision in a previous run | |||||||||
| v4.32.0 | 9d (+1) | v4.32.1 | compatible checked 2026-09-04 | v4.32.1 | — | +1 | v4.32.1 (+1) | ||
Sphere-Packing-Lean builds successfully against Mathlib v4.32.1. Its pin can be safely advanced by 1 commit to the last known good revision v4.32.1. Last checked2026-09-04 18:41 UTC ()Validation took21sHow it was checkedSkipped — this exact project revision was already validated as compatible with this Mathlib revision in a previous run | |||||||||
| 3ef2c2e | 0d (+1) | v4.33.0 | incompatible checked 2026-09-04 | 3ef2c2e | v4.33.0 | — | v4.33.0-rc2 (-93) | ||
Statlib fails to build against Mathlib v4.33.0. The incompatibility was introduced by Mathlib commit v4.33.0 (“chore: bump toolchain to v4.33.0 (#42604)”). The commit immediately before it, 3ef2c2e, still works and is a safe upgrade target. Last checked2026-09-04 18:41 UTC ()Validation took3m 19sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible)Failed during lake lint | |||||||||
| v4.31.0-rc1 | 10d (+329) | v4.31.0-rc2 | incompatible checked 2026-09-04 | 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-09-04 18:41 UTC ()Validation took5m 47sHow 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 | |||||||||
| 03616a1 | 1d (+56) | 52b284f | incompatible checked 2026-09-04 | 03616a1 | 5fcc665 | — | v4.34.0-rc2 (-366) | ||
TauCeti fails to build against Mathlib 52b284f. The incompatibility was introduced by Mathlib commit 5fcc665 (“chore: make Rat.castHom implicit_reducible (#43242)”). The commit immediately before it, 03616a1, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-09-04 18:41 UTC ()Validation took1h 41mHow it was checkedboundary-revalidatedFailed during lake build | |||||||||
| v4.34.0-rc2 | 13d (+422) | 52b284f | compatible checked 2026-09-04 | 52b284f | — | +422 | v4.34.0-rc2 | ||
Toric builds successfully against Mathlib 52b284f. Its pin can be safely advanced by 422 commits to the last known good revision 52b284f. Mathlib commit window (older → newer) Last checked2026-09-04 18:41 UTC ()Validation took2m 42sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| No downstream matches the current filters. | |||||||||