A replay of one real repair. Every panel below shows output that was
actually produced — nothing is simulated, and nothing compiles in your browser.
Reproduce it yourself in about six seconds with ./demo/run_render.sh.
kmill/lean4-raytracer is a raytracer written in Lean 4. It works. Its author has not touched it since 2024-05-16.
Nothing is wrong with the code. The compiler moved underneath it — that is the entire problem Colim exists to solve.
Lean’s official registry rebuilds every indexed package against each new toolchain. Here is what it recorded, verbatim:
error: Main.lean:291:42: Unknown constant `Array.mkArray` error: Lean exited with code 1 error: build failed
One removed name. The package is dead on the current compiler until somebody edits it.
Lean and Mathlib mark most renames with a deprecation alias, and Colim extracts them automatically — 4,515 renames from the sources at the target revision.
$ grep Array.mkArray fixers/tier1/renames.json (no match)
Array.mkArray is not in that map. It was removed outright, with no
alias left behind, so no amount of automatic extraction will find it. This is the
class of failure that makes naive rename tooling stall.
The replacement exists — it just was not advertised. Colim records it as a curated entry, and every curated entry must cite upstream:
old = "Array.mkArray" new = "Array.replicate" kind = "rename" evidence = "https://github.com/leanprover/lean4/pull/7544"
No entry may rest on recollection. A test refuses to load the map if any entry lacks an evidence link.
Colim clones the package at the exact revision the registry built, bumps the toolchain pin, and applies the rename maps at identifier boundaries — never inside strings or comments.
Main.lean - let mut pixels : Array (Color Float) := Array.mkArray (height * width) Color.black + let mut pixels : Array (Color Float) := Array.replicate (height * width) Color.black lean-toolchain -leanprover/lean4:v4.8.0-rc1 +leanprover/lean4:v4.32.1 old/vec.lean - array := Array.mkArray (Enumerable.card ι) a + array := Array.replicate (Enumerable.card ι) a
2 source lines, plus the toolchain pin. That is the whole change.
The repaired branch is pushed to our own fork and built by CI there. Nothing is proposed upstream. The verdict is machine-emitted:
"verified_green": true "built_nothing": false ← it really compiled something "toolchain_intact": true ← on the toolchain we pinned "targets": ["Render", "render"]
Those three booleans are the guards. A build that exits zero without compiling anything, or that ran on a toolchain something swapped underneath us, cannot be reported as green.
kmill/render builds green on v4.32.1, checked by the Lean kernel.