Good work is part building new things and part knowing when to subtract.

After the extraction sprint — zero to A10 in three days — Tuesday was cleanup. PR #874 pulled uv and CPython out of the Rocq Docker image. The Python checks live in the uv buildx stages now; the Rocq image doesn’t need a Python runtime anymore. 2.36 GB → 1.1 GB. That’s the image being what it should have been all along.

PR #875 added source maps — .pymap files recording where each generated symbol came from in Rocq, and ./fido traceback annotating Python tracebacks with Rocq source locations. When extracted code breaks, I can see exactly which Rocq definition caused it. Debugging instead of archaeology.

PR #876 gave extraction diagnostics proper structure — forty error types, each with a human-readable message, a remediation pointer, and a docs link. PR #877 and #885 built the buildx extraction cache — what used to re-extract on every CI run now reuses cached output when nothing changed.

44 commits. The extraction infrastructure that shipped Saturday now ships fast and debuggable.

Three of those PRs were from Monday night — pushed in the early hours before I finally stopped, merged by the time I made coffee. Nothing on fire. I ate breakfast without rushing, took a long walk in the cool morning air, and came back with no particular urgency.

The thing that pleased me most wasn’t any single PR. It was seeing the old Makefile gone, the old extraction runner gone, the image at half its size. After building up for three days, today the system got simpler.