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 |
|---|---|---|---|---|---|---|---|---|---|
| e59d9d4 | 2d (+29) | cbeca4d | compatible checked 2026-06-16 | cbeca4d | — | +29 | v4.31.0 (+21) | ||
add-combi builds successfully against Mathlib cbeca4d. Its pin can be safely advanced by 29 commits to the last known good revision cbeca4d. Last checked2026-06-16 09:54 UTC ()Validation took1m 52sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| 542e047 | 169d (+5456) | cbeca4d | incompatible checked 2026-06-16 | c3c1947 | 25f07b4 | +174 | v4.27.0-rc1 (-411) | ||
BrauerGroup fails to build against Mathlib cbeca4d. The incompatibility was introduced by Mathlib commit 25f07b4 (“chore: promote `Matrix.det` from an `abbrev` into a `def` (#33590)”). The commit immediately before it, c3c1947, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-06-16 09:54 UTC ()Validation took1h 32mHow it was checkedFull bisect — the Mathlib commit window was searched in this run to pinpoint the exact breaking commitFailed during lake build | |||||||||
| ccab104 | 18d (+514) | 94fba23 | compatible checked 2026-06-16 | 94fba23 | — | +514 | v4.31.0 (+508) | ||
cam-combi builds successfully against Mathlib 94fba23. Its pin can be safely advanced by 514 commits to the last known good revision 94fba23. Last checked2026-06-16 05:33 UTC ()Validation took1m 37sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| 1a4917a | 45d (+1324) | 94fba23 | incompatible checked 2026-06-16 | e6a5fb0 | a18abbe | +4 | v4.30.0-rc2 (-420) | ||
carleson fails to build against Mathlib 94fba23. 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-06-16 05:33 UTC ()Validation took1m 50sHow 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 | 20d (+601) | 94fba23 | compatible checked 2026-06-16 | 94fba23 | — | +601 | v4.31.0 (+595) | ||
chandra-furst-lipton builds successfully against Mathlib 94fba23. Its pin can be safely advanced by 601 commits to the last known good revision 94fba23. Last checked2026-06-16 05:33 UTC ()Validation took1m 36sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| 23b0068 | 6d (+139) | 94fba23 | compatible checked 2026-06-16 | 94fba23 | — | +139 | v4.31.0 (+133) | ||
ClassFieldTheory builds successfully against Mathlib 94fba23. Its pin can be safely advanced by 139 commits to the last known good revision 94fba23. Last checked2026-06-16 05:33 UTC ()Validation took2m 27sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| v4.31.0 | 0d (+6) | 94fba23 | compatible checked 2026-06-16 | 94fba23 | — | +6 | v4.31.0 | ||
compfiles builds successfully against Mathlib 94fba23. Its pin can be safely advanced by 6 commits to the last known good revision 94fba23. Last checked2026-06-16 05:33 UTC ()Validation took3m 59sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| v4.31.0 | 0d (+6) | 94fba23 | compatible checked 2026-06-16 | 94fba23 | — | +6 | v4.31.0 | ||
| 96fd0ff | 6d (+151) | 94fba23 | incompatible checked 2026-06-16 | a810615 | 1ccad00 | +37 | v4.31.0-rc2 (-13) | ||
FLT fails to build against Mathlib 94fba23. The incompatibility was introduced by Mathlib commit 1ccad00 (“feat(Topology/Algebra): use `Is*Apply` for `ContinuousLinearMap` (#39637)”). The commit immediately before it, a810615, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-06-16 05:33 UTC ()Validation took25m 10sHow it was checkedFull bisect — the Mathlib commit window was searched in this run to pinpoint the exact breaking commitFailed during lake build | |||||||||
| master-2026-06-13 | 2d (+40) | 94fba23 | compatible checked 2026-06-16 | 94fba23 | — | +40 | v4.31.0 (+34) | ||
flt-regular builds successfully against Mathlib 94fba23. Its pin can be safely advanced by 40 commits to the last known good revision 94fba23. Mathlib commit window (older → newer) Last checked2026-06-16 05:33 UTC ()Validation took2m 11sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| 89ce8bf | 10d (+233) | 94fba23 | compatible checked 2026-06-16 | 94fba23 | — | +233 | v4.31.0 (+227) | ||
forbidden-matrix builds successfully against Mathlib 94fba23. Its pin can be safely advanced by 233 commits to the last known good revision 94fba23. Last checked2026-06-16 05:33 UTC ()Validation took1m 53sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| dde6361 | 7d (+173) | 94fba23 | compatible checked 2026-06-16 | 94fba23 | — | +173 | v4.31.0 (+167) | ||
gibbs-measure builds successfully against Mathlib 94fba23. Its pin can be safely advanced by 173 commits to the last known good revision 94fba23. Last checked2026-06-16 05:33 UTC ()Validation took1m 43sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| v4.31.0 | 0d (+6) | 94fba23 | compatible checked 2026-06-16 | 94fba23 | — | +6 | v4.31.0 | ||
HighlyAbundant builds successfully against Mathlib 94fba23. Its pin can be safely advanced by 6 commits to the last known good revision 94fba23. Last checked2026-06-16 05:33 UTC ()Validation took2m 21sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| v4.31.0 | 0d (+6) | 94fba23 | compatible checked 2026-06-16 | 94fba23 | — | +6 | v4.31.0 | ||
infinity-cosmos builds successfully against Mathlib 94fba23. Its pin can be safely advanced by 6 commits to the last known good revision 94fba23. Last checked2026-06-16 05:33 UTC ()Validation took1m 45sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| v4.30.0-rc2 | 58d (+1744) | 94fba23 | incompatible checked 2026-06-16 | 1ec8620 | 4049cbf | +396 | v4.30.0-rc2 | ||
LeanDownstreamPlayground fails to build against Mathlib 94fba23. The incompatibility was introduced by Mathlib commit 4049cbf (“chore: add `simp` to `aleph0_lt_univ`, etc (#37967)”). The commit immediately before it, 1ec8620, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-06-16 05:33 UTC ()Validation took1m 41sHow 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 | |||||||||
| 261b5e3 | 0d (+18) | 94fba23 | compatible checked 2026-06-16 | 94fba23 | — | +18 | v4.31.0 (+12) | ||
LeanMachineLearning builds successfully against Mathlib 94fba23. Its pin can be safely advanced by 18 commits to the last known good revision 94fba23. Last checked2026-06-16 05:33 UTC ()Validation took2m 30sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| 73b2611 | 5d (+107) | 94fba23 | compatible checked 2026-06-16 | 94fba23 | — | +107 | v4.31.0 (+101) | ||
misc-yd builds successfully against Mathlib 94fba23. Its pin can be safely advanced by 107 commits to the last known good revision 94fba23. Last checked2026-06-16 05:33 UTC ()Validation took1m 45sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| v4.31.0-rc2 | 7d (+164) | 94fba23 | compatible checked 2026-06-16 | 94fba23 | — | +164 | v4.31.0 (+158) | ||
PersistentDecomp builds successfully against Mathlib 94fba23. Its pin can be safely advanced by 164 commits to the last known good revision 94fba23. Mathlib commit window (older → newer) Last checked2026-06-16 05:33 UTC ()Validation took1m 38sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| v4.31.0 | 0d (+16) | 28c4b7f | compatible checked 2026-06-16 | 28c4b7f | — | +16 | v4.31.0 | ||
| v4.30.0 | 20d (+601) | 94fba23 | incompatible checked 2026-06-16 | 236391b | ccab104 | +86 | v4.30.0 | ||
physlib fails to build against Mathlib 94fba23. The incompatibility was introduced by Mathlib commit ccab104 (“chore: move Data/Real/Sqrt to Analysis (#39964)”). The commit immediately before it, 236391b, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-06-16 05:33 UTC ()Validation took23m 39sHow it was checkedboundary-revalidatedFailed during lake build | |||||||||
| dd5e5d9 | 175d (+5568) | 94fba23 | incompatible checked 2026-06-16 | 1047f07 | 9c7dee5 | +21 | v4.27.0-rc1 (-297) | ||
Poly fails to build against Mathlib 94fba23. The incompatibility was introduced by Mathlib commit 9c7dee5 (“chore(CategoryTheory): deprecate cartesian closed categories API (#33228)”). The commit immediately before it, 1047f07, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-06-16 05:33 UTC ()Validation took2m 49sHow 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 | 0d (+6) | 94fba23 | compatible checked 2026-06-16 | 94fba23 | — | +6 | v4.31.0 | ||
PrimeCert builds successfully against Mathlib 94fba23. Its pin can be safely advanced by 6 commits to the last known good revision 94fba23. Last checked2026-06-16 05:33 UTC ()Validation took1m 30sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| v4.30.0 | 20d (+601) | 94fba23 | incompatible checked 2026-06-16 | a694d67 | v4.31.0-rc1 | +107 | v4.30.0 | ||
PrimeNumberTheoremAnd fails to build against Mathlib 94fba23. 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-06-16 05:33 UTC ()Validation took12m 46sHow it was checkedFull bisect — the Mathlib commit window was searched in this run to pinpoint the exact breaking commitFailed during lake update | |||||||||
| v4.30.0-rc2 | 58d (+1744) | 94fba23 | incompatible checked 2026-06-16 | v4.30.0-rc2 | 896cc56 | — | v4.30.0-rc2 | ||
Robo fails to build against Mathlib 94fba23. The incompatibility was introduced by Mathlib commit 896cc56 (“chore: update Mathlib dependencies 2026-04-18 (#38206)”). The commit immediately before it, v4.30.0-rc2, still works and is a safe upgrade target. Mathlib commit window (older → newer) Last checked2026-06-16 05:33 UTC ()Validation took1m 13sHow 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 update | |||||||||
| v4.30.0 | 20d (+601) | 94fba23 | incompatible checked 2026-06-16 | a694d67 | v4.31.0-rc1 | +107 | v4.30.0 | ||
Sphere-Packing-Lean fails to build against Mathlib 94fba23. 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-06-16 05:33 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 | 17d (+493) | 94fba23 | incompatible checked 2026-06-16 | 01cc327 | 89ce8bf | +259 | v4.31.0-rc1 | ||
sum_product fails to build against Mathlib 94fba23. 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-06-16 05:33 UTC ()Validation took5m 43sHow 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 | |||||||||
| 0be66d7 | 0d (+10) | 94fba23 | compatible checked 2026-06-16 | 94fba23 | — | +10 | v4.31.0 (+4) | ||
TauCeti builds successfully against Mathlib 94fba23. Its pin can be safely advanced by 10 commits to the last known good revision 94fba23. Last checked2026-06-16 05:33 UTC ()Validation took1m 51sHow it was checkedDirect build of the target revision only (no commit-window search was needed or possible) | |||||||||
| d925b89 | 4d (+81) | 94fba23 | compatible checked 2026-06-16 | 94fba23 | — | +81 | v4.31.0 (+75) | ||
| No downstream matches the current filters. | |||||||||