[chris-dare-dev]

The emitter is 3.85 min of a 20.7 min CI job on derived-alg-geo-lean, and it runs twice per job. Nothing said which part. Three plausible culprits were available and all three turned out to be wrong.

What the guesses were, and what they measure

guess	reality
collectAxioms per constant is quadratic	No. Since the exportedAxiomsExt extension, an imported constant's axiom closure is a binary search over pre-computed per-module entries — and this emitter's environment is entirely imported. axioms_ms 0 of 547.
Json.pretty 120 on a 38 MB document is expensive	No. Timed standalone against that exact artifact at v4.32.1: pretty 120 206 ms, compress 204 ms. A 2 ms difference, 0.09% of the step.
—	What is there: on this package's own 331-row library, pp_ms 422 and deps_ms 116 of a 547 ms sweep, inside an import_ms of 1825.

Two JSON lines on stderr, built with Json.mkObj so they are valid by construction:

mfc-emit-sweep:  {"rows":331,"sweep_ms":547,"sort_ms":0,"axioms_ms":0,"attrs_ms":5,
                  "pp_ms":422,"deps_ms":116,"cites_ms":0,"pp_chars":157926,
                  "axiom_refs":181,"dep_edges":725,"cite_refs":0}
mfc-emit-phases: {"modules":2275,"import_ms":1825,"emit_ms":692,"render_ms":0,
                  "write_ms":17,"chars":375969}

stderr and nowhere else

A timing field inside emission/1.0 would rotate emission_sha256, break the two-sweep determinism gate the first time a clock ticked differently between runs, and put a measurement of the machine inside a record about the repository. Telemetry and evidence do not share a file.

Forcing is the whole difficulty

A timer that does not force reads zero. ppExpr's result is lazy — the first draft of this reported the entire sweep at single-digit milliseconds and attributed the cost to Json.pretty in the driver, which is merely where the thunks were being demanded.

Every counter is paired with a size the report carries: String.length walks the UTF-8 bytes (utf8ByteSize would not — O(1) off the header), and Array.size demands the array qsort had to build. Reporting the sizes is also what stops the compiler eliminating the force as dead code. The forcing cost stays inside the number it forces.

The artifact does not move — verified, not asserted

Built at origin/main, emitted; rebuilt with this change, emitted again:

• mfc_emit_selftest (12 constants, over a library this file is not part of): byte-identical modulo emitted_at.
• mfc_emit_self (over MathFormalContract, which does contain this file): 37 constants added, 0 removed — every one a Timings projection or _default. Of the 294 in common, 13 differ, and all 13 are declarations in this file whose range moved.

No statement was reordered to fit a timer in. findDocString? stays where it was and contributes two disjoint windows to attrs_ms; moving it to make one clean window would have been a behaviour change hiding inside a measurement.

What this unblocks

Bumping the pin in a topic repo gives a per-run attribution of the emit step in the CI log, which is the input both to deciding whether parallelising the sweep is worth it and to the seconds{} field of a per-merge metrics row.

deps_ms is already suspicious at 21% of a 331-row sweep: sortedNames calls Name.toString inside the qsort comparator, so it rebuilds both strings on every comparison, and a def sorts three times (type, value, then the concatenation). That is a follow-up, with numbers, not a guess folded in here.

🤖 Generated with Claude Code