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 |
|---|---|---|---|---|---|---|---|---|---|
| dc2a600 | 1d (+29) | af6dcfb | compatible checked 2026-11-12 | af6dcfb | — | +29 | v4.36.0-rc2 (-376) | ||
add-combi builds successfully against Mathlib af6dcfb. Its pin can be safely advanced by 29 commits to the last known good revision af6dcfb. Last checked2026-11-12 17:16 UTC ()Validation took2m 23sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| c31114f | 6d (+131) | v4.36.0-rc2 | compatible checked 2026-11-12 | v4.36.0-rc2 | — | +131 | v4.36.0-rc2 (+131) | ||
apap builds successfully against Mathlib v4.36.0-rc2. Its pin can be safely advanced by 131 commits to the last known good revision v4.36.0-rc2. Mathlib commit window (older → newer) Last checked2026-11-12 17:16 UTC ()Validation took19sHow it was checkedSkipped — this exact project revision was already validated as compatible with this Mathlib revision in a previous run | |||||||||
| 089be9f | 3d (+99) | af6dcfb | compatible checked 2026-11-12 | af6dcfb | — | +99 | v4.36.0-rc2 (-306) | ||
BrauerGroup builds successfully against Mathlib af6dcfb. Its pin can be safely advanced by 99 commits to the last known good revision af6dcfb. Last checked2026-11-12 17:16 UTC ()Validation took4m 31sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| dc2a600 | 1d (+29) | af6dcfb | compatible checked 2026-11-12 | af6dcfb | — | +29 | v4.36.0-rc2 (-376) | ||
cam-combi builds successfully against Mathlib af6dcfb. Its pin can be safely advanced by 29 commits to the last known good revision af6dcfb. Last checked2026-11-12 17:16 UTC ()Validation took2m 23sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| d888143 | 5d (+115) | v4.36.0-rc2 | compatible checked 2026-11-12 | v4.36.0-rc2 | — | +115 | v4.36.0-rc2 (+115) | ||
carleson builds successfully against Mathlib v4.36.0-rc2. Its pin can be safely advanced by 115 commits to the last known good revision v4.36.0-rc2. Mathlib commit window (older → newer) Last checked2026-11-12 17:16 UTC ()Validation took24sHow it was checkedSkipped — this exact project revision was already validated as compatible with this Mathlib revision in a previous run | |||||||||
| v4.36.0-rc2 | 15d (+405) | af6dcfb | compatible checked 2026-11-12 | af6dcfb | — | +405 | v4.36.0-rc2 | ||
chandra-furst-lipton builds successfully against Mathlib af6dcfb. Its pin can be safely advanced by 405 commits to the last known good revision af6dcfb. Mathlib commit window (older → newer) Last checked2026-11-12 17:16 UTC ()Validation took1m 34sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| e20b4f3 | 15d (+392) | af6dcfb | incompatible checked 2026-11-12 | f2bcc25 | 97bcf24 | +53 | v4.36.0-rc2 (-13) | ||
ClassFieldTheory fails to build against Mathlib af6dcfb. The incompatibility was introduced by Mathlib commit 97bcf24 (“feat: use `IsApply` for `Module.End` (#45347)”). The commit immediately before it, f2bcc25, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-11-12 17:16 UTC ()Validation took2m 00sHow 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.35.0 | 3d (+89) | v4.36.0-rc1 | incompatible checked 2026-11-12 | 10f994e | ba9c63d | +2 | v4.35.0 | ||
compfiles fails to build against Mathlib v4.36.0-rc1. The incompatibility was introduced by Mathlib commit ba9c63d (“refactor(Data): make `Set` a one-field structure (#41506)”). The commit immediately before it, 10f994e, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-11-12 17:16 UTC ()Validation took4m 25sHow 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 | |||||||||
| 887bb84 | 5d (+132) | af6dcfb | compatible checked 2026-11-12 | af6dcfb | — | +132 | v4.36.0-rc2 (-273) | ||
cslib builds successfully against Mathlib af6dcfb. Its pin can be safely advanced by 132 commits to the last known good revision af6dcfb. Last checked2026-11-12 17:16 UTC ()Validation took3m 39sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| v4.35.0-rc1 | 0d (+21) | v4.35.0-rc2 | compatible checked 2026-11-12 | v4.35.0-rc2 | — | +21 | v4.35.0-rc2 (+21) | ||
DirichletProblem builds successfully against Mathlib v4.35.0-rc2. Its pin can be safely advanced by 21 commits to the last known good revision v4.35.0-rc2. Mathlib commit window (older → newer) Last checked2026-11-12 17:16 UTC ()Validation took24sHow it was checkedSkipped — this exact project revision was already validated as compatible with this Mathlib revision in a previous run | |||||||||
| v4.36.0-rc2 | 15d (+405) | af6dcfb | compatible checked 2026-11-12 | af6dcfb | — | +405 | v4.36.0-rc2 | ||
DynamicalSystems builds successfully against Mathlib af6dcfb. Its pin can be safely advanced by 405 commits to the last known good revision af6dcfb. Mathlib commit window (older → newer) Last checked2026-11-12 17:16 UTC ()Validation took2m 58sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
detached | 106d (+2914) | af6dcfb | incompatible checked 2026-11-12 | — | 39c86ed | — | — | ||
ErdosUnitDistance fails to build against Mathlib af6dcfb. The earliest known incompatible Mathlib commit is 39c86ed (“feat(NumberTheory/NumberField/AdeleRing): define the idele class group (#40735)”). Last checked2026-11-12 17:16 UTC ()Validation took3m 57sHow 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.35.0 | 3d (+89) | v4.36.0-rc1 | incompatible checked 2026-11-12 | 10f994e | ba9c63d | +2 | v4.35.0 | ||
FLT fails to build against Mathlib v4.36.0-rc1. The incompatibility was introduced by Mathlib commit ba9c63d (“refactor(Data): make `Set` a one-field structure (#41506)”). The commit immediately before it, 10f994e, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-11-12 17:16 UTC ()Validation took18m 43sHow it was checkedFull bisect — the Mathlib commit window was searched in this run to pinpoint the exact breaking commitFailed during lake build | |||||||||
| 4dcd48f | 4d (+126) | af6dcfb | incompatible checked 2026-11-12 | 089be9f | 1c2b155 | +27 | v4.36.0-rc2 (-279) | ||
flt-regular fails to build against Mathlib af6dcfb. The incompatibility was introduced by Mathlib commit 1c2b155 (“chore(NumberTheory): move declarations from namespace `RingOfIntegers` to `NumberField.RingOfIntegers` (#45809)”). The commit immediately before it, 089be9f, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-11-12 17:16 UTC ()Validation took2m 01sHow 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 | |||||||||
| 6955275 | 15d (+394) | af6dcfb | compatible checked 2026-11-12 | af6dcfb | — | +394 | v4.36.0-rc2 (-11) | ||
forbidden-matrix builds successfully against Mathlib af6dcfb. Its pin can be safely advanced by 394 commits to the last known good revision af6dcfb. Last checked2026-11-12 17:16 UTC ()Validation took2m 33sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| v4.36.0-rc2 | 15d (+405) | af6dcfb | compatible checked 2026-11-12 | af6dcfb | — | +405 | v4.36.0-rc2 | ||
gibbs-measure builds successfully against Mathlib af6dcfb. Its pin can be safely advanced by 405 commits to the last known good revision af6dcfb. Mathlib commit window (older → newer) Last checked2026-11-12 17:16 UTC ()Validation took1m 46sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| 6b7abb3 | 8d (+225) | v4.35.0-rc4 | error checked 2026-11-12 | — | c35749f | — | — | ||
The latest validation run for hex-dev hit an unexpected error before producing a result. This usually points to an infrastructure problem (runner, network, cache) rather than a Mathlib incompatibility. Last checked2026-11-12 17:16 UTC ()Validation took15m 32sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible)Failed during lake updatelake update failed; dependency resolution is a network operation, so no tested commit is implicated | |||||||||
| v4.33.0 | 11d (+1) | v4.33.1 | compatible checked 2026-11-12 | 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-11-12 17:16 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-11-12 | 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-11-12 17:16 UTC ()Validation took24sHow it was checkedSkipped — this exact project revision was already validated as compatible with this Mathlib revision in a previous run | |||||||||
| 6135ffb | 6d (+176) | af6dcfb | incompatible checked 2026-11-12 | 94f4300 | master-2026-11-06 | +23 | v4.36.0-rc2 (-229) | ||
LeanMachineLearning fails to build against Mathlib af6dcfb. The incompatibility was introduced by Mathlib commit master-2026-11-06 (“refactor: change the definition of `EventuallyEqSet` (#45712)”). The commit immediately before it, 94f4300, still works and is a safe upgrade target. Mathlib commit window (older → newer) 6135ffbpinned 23 commits 94f4300last known good master-2026-11-06first known bad 152 commits af6dcfbtarget Last checked2026-11-12 17:16 UTC ()Validation took3m 23sHow 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 | |||||||||
| 2d833a6 | 0d (+16) | af6dcfb | compatible checked 2026-11-12 | af6dcfb | — | +16 | v4.36.0-rc2 (-389) | ||
mean-fourier builds successfully against Mathlib af6dcfb. Its pin can be safely advanced by 16 commits to the last known good revision af6dcfb. Last checked2026-11-12 17:16 UTC ()Validation took2m 18sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| 6955275 | 15d (+394) | af6dcfb | compatible checked 2026-11-12 | af6dcfb | — | +394 | v4.36.0-rc2 (-11) | ||
misc-yd builds successfully against Mathlib af6dcfb. Its pin can be safely advanced by 394 commits to the last known good revision af6dcfb. Last checked2026-11-12 17:16 UTC ()Validation took2m 17sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| v4.36.0-rc2 | 15d (+405) | af6dcfb | compatible checked 2026-11-12 | af6dcfb | — | +405 | v4.36.0-rc2 | ||
PersistentDecomp builds successfully against Mathlib af6dcfb. Its pin can be safely advanced by 405 commits to the last known good revision af6dcfb. Mathlib commit window (older → newer) Last checked2026-11-12 17:16 UTC ()Validation took1m 40sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| 8fe7ce4 | 14d (+328) | af6dcfb | compatible checked 2026-11-12 | af6dcfb | — | +328 | v4.36.0-rc2 (-77) | ||
| v4.35.0 | 3d (+89) | v4.36.0-rc1 | compatible checked 2026-11-12 | v4.36.0-rc1 | — | +89 | v4.36.0-rc1 (+89) | ||
physlib builds successfully against Mathlib v4.36.0-rc1. Its pin can be safely advanced by 89 commits to the last known good revision v4.36.0-rc1. Mathlib commit window (older → newer) Last checked2026-11-12 17:16 UTC ()Validation took5m 23sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| b8dad03 | 5d (+198) | v4.28.0 | compatible checked 2026-11-12 | 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-11-12 17:16 UTC ()Validation took19sHow it was checkedSkipped — this exact project revision was already validated as compatible with this Mathlib revision in a previous run | |||||||||
| v4.36.0-rc2 | 15d (+405) | af6dcfb | incompatible checked 2026-11-12 | 64e4c10 | e2bb1c9 | +48 | v4.36.0-rc2 | ||
PrimeCert fails to build against Mathlib af6dcfb. The incompatibility was introduced by Mathlib commit e2bb1c9 (“chore(Algebra/Order): split out the order on `Associates` (#45247)”). The commit immediately before it, 64e4c10, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-11-12 17:16 UTC ()Validation took1m 52sHow 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 test | |||||||||
| v4.35.0 | 3d (+89) | v4.36.0-rc1 | incompatible checked 2026-11-12 | 10f994e | ba9c63d | +2 | v4.35.0 | ||
PrimeNumberTheoremAnd fails to build against Mathlib v4.36.0-rc1. The incompatibility was introduced by Mathlib commit ba9c63d (“refactor(Data): make `Set` a one-field structure (#41506)”). The commit immediately before it, 10f994e, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-11-12 17:16 UTC ()Validation took15m 33sHow it was checkedboundary-revalidatedFailed during lake build | |||||||||
| v4.35.0 | 3d (+89) | v4.36.0-rc1 | error checked 2026-11-12 | v4.32.0-rc1 | — | 0 | v4.32.0-rc1 (-2750) | ||
The latest validation run for Robo hit an unexpected error before producing a result. This usually points to an infrastructure problem (runner, network, cache) rather than a Mathlib incompatibility. Last checked2026-11-12 17:16 UTC ()Validation took1m 23sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible)Failed during lake updatelake update failed; dependency resolution is a network operation, so no tested commit is implicated | |||||||||
| v4.35.0 | 3d (+89) | v4.36.0-rc1 | incompatible checked 2026-11-12 | 10f994e | ba9c63d | +2 | v4.35.0 | ||
Sphere-Packing-Lean fails to build against Mathlib v4.36.0-rc1. The incompatibility was introduced by Mathlib commit ba9c63d (“refactor(Data): make `Set` a one-field structure (#41506)”). The commit immediately before it, 10f994e, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-11-12 17:16 UTC ()Validation took2m 27sHow 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 | |||||||||
| 6135ffb | 6d (+176) | af6dcfb | incompatible checked 2026-11-12 | 94f4300 | master-2026-11-06 | +23 | v4.36.0-rc2 (-229) | ||
Statlib fails to build against Mathlib af6dcfb. The incompatibility was introduced by Mathlib commit master-2026-11-06 (“refactor: change the definition of `EventuallyEqSet` (#45712)”). The commit immediately before it, 94f4300, still works and is a safe upgrade target. Mathlib commit window (older → newer) 6135ffbpinned 23 commits 94f4300last known good master-2026-11-06first known bad 152 commits af6dcfbtarget Last checked2026-11-12 17:16 UTC ()Validation took2m 03sHow 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-rc1 | 10d (+329) | v4.31.0-rc2 | incompatible checked 2026-11-12 | 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-11-12 17:16 UTC ()Validation took9m 18sHow 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 | |||||||||
| a949576 | 7d (+188) | af6dcfb | compatible checked 2026-11-12 | af6dcfb | — | +188 | v4.36.0-rc2 (-217) | ||
Toric builds successfully against Mathlib af6dcfb. Its pin can be safely advanced by 188 commits to the last known good revision af6dcfb. Last checked2026-11-12 17:16 UTC ()Validation took2m 23sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| No downstream matches the current filters. | |||||||||