Colim · census of Lean’s official package registry
500of 75866%
packages in Lean’s official registry fail to build on the current stable toolchain.proof ↗
52 of the failing packages are recorded only as infrastructure-ambiguous. Independent measurement is in progress; until it completes this figure is an upper bound.proof ↗
Source: Reservoir build history, 116,874 records. Every figure is a SQL query over our ledger; every row links to a public build log.
11 of 11 independent rebuilds agree with the registry.
We rebuilt a sample ourselves, on the same forced toolchain, rather than trusting the registry’s record. A build that compiles nothing is recorded as inconclusive, never as green.proof ↗
40 ambiguous packages independently re-measured.
Rebuilt in our own CI, upstream cloned read-only at the exact revision. Real errors keep a package in the count; a green build removes it.proof ↗
What is actually broken
How we know each package is failing
Compiler errors in the package’s own code
403
Registry build failed before compiling — measurement in progress
52
We rebuilt it ourselves — public build log
34
We rebuilt it on our own machine
11
Why they fail
Uses a name upstream has deprecated
228
Types no longer line up
178
Identifier removed or renamed upstream
155
Proof no longer closes
102
Registry could not fetch its build cache
92
Structure field removed or renamed
90
Name now clashes with upstream
79
Required instance no longer found
73
Stale build artifacts
64
Packages usually fail for several reasons at once, so these do not sum to the total.