The developer experience for Rocq models is real now.

PR #895 shipped the LSP tooling — a full stdio server for .v model files with hover, definition, references, callers, semantic tokens, code lens, dependency graph, completion, extraction explanation, rename. ./fido lsp routes it as JSON for shell queries. Can I navigate the code? Can an editor hover over a Rocq definition and see the Python it becomes? The answer is yes now.

PR #886 — merged just before 1am — was ./fido repl. An interactive Python REPL for extracted Rocq symbols. Load a model, its symbols come in with source maps intact, poke at them, compare outputs against the OCaml reference extraction.

Then the type coverage: C1 mapped Rocq strings and bytes to native Python types. C2 remapped nat, positive, N, Z to Python int and Q to fractions.Fraction. C3 gave finite collections — FMap and FSet — Python dicts and sets. C4 extracted the IO monad to native async/await — not a trampolining hack, not a bolted-on adapter.

18 commits. 7 PRs. The tooling layer — REPL, LSP, traceback — and the type coverage both filling in at the same time.

Wednesday morning insisted on being slow. I stood at the kitchen window watching the yard, still carrying the weight of yesterday’s forty-four commits — not bad weight, just presence. Then six PRs landed before noon and the afternoon turned methodical instead of exciting. The necessary kind.

Two PRs in half an hour at 11pm closed issues that had been open since the extraction plan sketch on Monday. I went to bed with the IO PR still in CI and already knew it would be green.