# Colim Day-1 Census

Generated by `census/report.py` from `ledger/colim.sqlite`. Do not edit by hand.

| provenance | value |
|---|---|
| Reservoir index snapshot | `2acc551043c37488cf1238059b9c657304e4e16e` |
| snapshot committed | 2026-07-26T15:41:49Z |
| GitHub metadata fetched | 2026-07-27T19:09:08Z |
| evaluation toolchain | `leanprover/lean4:v4.32.1` |
| build coverage on that toolchain | 98.9% of indexed packages |

## Headline

**K = 758**  ·  **M = 500**  ·  **M/K = 66.0%**

500 of 758 in-scope packages in Lean's official registry are red regressions on `leanprover/lean4:v4.32.1` — they build on some earlier toolchain but fail when forced onto the evaluation toolchain.

> **Quote this alongside M:** 52 of those 500 (10.4%) are `infra_uninformative` — Reservoir's build failed on a cache fetch, so its log does not show whether the package's code survives the toolchain. They remain in M because their recorded outcome is red, and they are being resolved by measurement, not assumption. Until that completes, M is an upper bound by up to 52 packages.

## Scope

| | n | meaning |
|---|---|---|
| indexed packages | 790 | every package in the Reservoir index |
| `ARCHIVED` | 24 | upstream archived the repo — excluded from K and M |
| `VANISHED` | 8 | source no longer resolves — excluded from K and M |
| **K** | **758** | indexed, in scope |

## Classification on `leanprover/lean4:v4.32.1`

Denominator K = 758.

| status | n | % of K |
|---|---:|---:|
| `RED_REGRESSION` | 500 | 66.0% |
| `GREEN_CURRENT` | 175 | 23.1% |
| `NEVER_GREEN` | 75 | 9.9% |
| `FORCED_DOWNGRADE` | 7 | 0.9% |
| `UNKNOWN` | 1 | 0.1% |

`NEVER_GREEN` (75) is excluded from the headline by definition: those packages never built green on any toolchain, so they cannot have regressed.

### `FORCED_DOWNGRADE` — pinned ahead of the evaluation toolchain

Reservoir forces the toolchain, so these 7 packages fail because their source is **too new** for `v4.32.1`, not because upstream broke them. A forced-backwards failure is the opposite of a regression, so they are not in M.

| stars | package | pins |
|---:|---|---|
| 3697 | `leanprover-community/mathlib` | `leanprover/lean4:v4.33.0-rc1` |
| 409 | `leanprover-community/batteries` | `leanprover/lean4:v4.33.0-rc1` |
| 179 | `lean-ja/Lean by Example` | `leanprover/lean4:v4.33.0-rc1` |
| 59 | `RemyDegenne/BrownianMotion` | `leanprover/lean4:v4.33.0-rc1` |
| 15 | `artie2000/real-closed-field` | `leanprover/lean4:v4.33.0-rc1` |
| 8 | `oliver-butterley/SpectralThm` | `leanprover/lean4:v4.33.0-rc1` |
| 2 | `int-y1/proofs` | `leanprover/lean4:v4.33.0-rc1` |

## Mathlib-downstream subset (campaign target)

Reported against its own denominator K_m, never swapped for K.

| | n |
|---|---:|
| K_m (mathlib-dependent, in K) | 489 |
| red regressions within K_m | 366 (74.8% of K_m) |
| **Day-6 campaign set** (K_m red, minus release train) | **366** |

## Recency slice

Staleness never excludes a package — abandoned-but-once-green is the market. This slice is shown because a skeptic will ask for it.

| active within | K | M | M/K |
|---|---:|---:|---:|
| 12 months | 564 | 356 | 63.1% |
| 24 months | 666 | 436 | 65.5% |

## Failure origin

Classified from Reservoir's public build logs. Dependency rot is the product
thesis, so the split is counted and disclosed rather than hidden.

| origin | n | % of resolved |
|---|---:|---:|
| `self` | 210 | 53.0% |
| `dependency` | 147 | 37.1% |
| `unknown` | 104 | — |
| `both` | 39 | 9.8% |

Resolved for 396 of 500 reds. The split is reported against the
resolved subset only and is never extrapolated to the remainder.

## Why we believe each red is red (`red_basis`)

Not every red is evidenced the same way, and the differences govern how a row may be quoted.

| basis | n | meaning |
|---|---:|---|
| `code_error` | 403 | log shows Lean/Lake errors in real code |
| `infra_uninformative` | 52 | only a cache fetch failed; Reservoir's log is silent on the code — awaiting measurement |
| `measured_actions` | 34 | rebuilt via our own Actions matrix; run log public |
| `measured_local` | 11 | we rebuilt it here and saw the outcome ourselves |

The 52 `infra_uninformative` packages are **not** excluded by rule. Excluding them would assume they are healthy; counting them silently would assume they are broken. Both are guesses. They are instead being rebuilt in our own repository via a GitHub Actions matrix — upstream cloned at its pinned revision, evaluation toolchain forced, Mathlib cache fetched, `lake build` — with the public run log linked per package. Results reclassify the row: real code errors keep it in M with its error classes, a green build moves it out of M with the delta logged, and a repeat infrastructure failure leaves it flagged.

No forks are involved in measurement and nothing is sent upstream — the workflow runs in our own repository.

## Local reproduction (control on Reservoir)

11 of 11 conclusive reproductions came out red locally under the same forced toolchain (11 attempted).

A `lake build` that exits 0 without compiling anything — a package with no default target — is recorded as **inconclusive**, never as green. A green that ran no kernel checks proves nothing.

| package | verdict | step | local error classes | duration |
|---|---|---|---|---:|
| `0art0/kimina` | red — agrees | build | lake_config_api, not_a_field | 4s |
| `ImperialCollegeLondon/formalising-mathematics-2024` | red — agrees | build | unknown_identifier, deprecated, invalid_field, type_mismatch | 52s |
| `Paper-Proof/paperproof` | red — agrees | build | deprecated, invalid_field, type_mismatch, duplicate_declaration | 210s |
| `chasenorman/Canonical` | red — agrees | build | infra_release_fetch | 18s |
| `digama0/lean4lean` | red — agrees | build | deprecated, duplicate_declaration | 84s |
| `google-deepmind/formal_conjectures` | red — agrees | build | lake_stale_artifact, unknown_identifier, deprecated, invalid_field | 232s |
| `leanprover-community/lean4-metaprogramming-book` | red — agrees | build | deprecated, invalid_field | 8s |
| `leanprover-community/mil` | red — agrees | build | unknown_identifier, invalid_field, type_mismatch, duplicate_declaration | 181s |
| `lecopivo/scilean` | red — agrees | build | infra_release_fetch, lake_stale_artifact, lake_external_command, deprecated | 284s |
| `loganrjmurphy/lib` | red — agrees | build | lake_config_api, lake_stale_artifact, unknown_identifier, deprecated | 283s |
| `teorth/equational_theories` | red — agrees | build | deprecated, invalid_field, type_mismatch, duplicate_declaration | 269s |

## Day-2 spot-check candidates

Top red regressions by stars. `M` marks mathlib-downstream.

| stars | | package | pins | last commit |
|---:|---|---|---|---|
| 1835 | M | `teorth/Analysis` | `v4.29.0-rc8` | 2026-07-17 |
| 1147 | M | `google-deepmind/formal_conjectures` | `v4.27.0` | 2026-07-27 |
| 955 | M | `ImperialCollegeLondon/FLT` | `v4.32.0` | 2026-07-26 |
| 657 | M | `leanprover-community/Physlib` | `v4.32.0` | 2026-07-27 |
| 567 | M | `leanprover-community/mil` | `v4.30.0` | 2026-06-11 |
| 544 | M | `teorth/equational_theories` | `v4.29.1` | 2026-07-21 |
| 537 |  | `Paper-Proof/paperproof` | `v4.29.0-rc8` | 2026-07-20 |
| 522 | M | `lecopivo/scilean` | `v4.28.0-rc1` | 2026-02-18 |
| 396 | M | `PatrickMassot/glimpseOfLean` | `v4.27.0` | 2026-04-17 |
| 351 | M | `leanprover-community/Game` | `v4.23.0` | 2026-07-03 |
| 329 | M | `AlexKontorovich/PrimeNumberTheoremAnd` | `v4.32.0` | 2026-07-24 |
| 318 | M | `Verified-zkEVM/Arklib` | `v4.31.0` | 2026-07-25 |
| 304 |  | `leanprover-community/lean4-metaprogramming-book` | `v4.17.0-rc1` | 2026-07-26 |
| 302 | M | `ufmg-smite/smt` | `v4.32.0` | 2026-07-23 |
| 292 |  | `konne88/functorio` | `v4.20.1` | 2025-10-16 |
| 271 | M | `verse-lab/veil` | `v4.24.0` | 2026-02-11 |
| 256 | M | `ImperialCollegeLondon/formalising-mathematics-2024` | `v4.5.0-rc1` | 2025-03-18 |
| 252 |  | `opencompl/SSA` | `nightly-2025-12-01` | 2026-07-20 |
| 249 | M | `dwrensha/compfiles` | `v4.32.0` | 2026-07-26 |
| 213 |  | `cmu-l3/llmlean` | `v4.23.0` | 2025-10-10 |
| 213 |  | `strata-org/Strata` | `v4.29.1` | 2026-07-27 |
| 204 |  | `leanprover-community/iris-lean` | `?` | 2026-07-27 |
| 198 |  | `digama0/lean4lean` | `v4.29.0` | 2026-07-06 |
| 168 | M | `Verified-zkEVM/Clean` | `v4.30.0` | 2026-07-06 |
| 155 | M | `verse-lab/Loom` | `v4.24.0` | 2026-02-21 |

## Caveats that travel with these numbers

1. **Reservoir forces the toolchain.** Packages are built against `leanprover/lean4:v4.32.1` regardless of the toolchain they pin. "Red" therefore means *fails when forced onto v4.32.1*, not *the maintainer's own pinned build is broken*. That is the intended regression question, stated in those words.
2. **24 archived and 8 vanished packages are outside K and M.** Vanished packages can never enter N — there is no repo to fork.
3. **Classification uses Reservoir's recorded outcomes, not local rebuilds.** Day 2 reproduces a sample locally to check Reservoir against reality.
4. **Coverage is not 100%.** The evaluation toolchain has a recorded outcome for 98.9% of indexed packages; the remainder is `UNKNOWN`, never guessed.