Three follow-ups from #2718. One is a fix, one is a negative result, one was already done.
union(enum) — the last of the 31
ParsedCommand's payloads were recovered in #2718 and could not be written down: the emitter answered use of undeclared identifier 'union'.
There is no KwUnion in the lexer — union arrives as an Ident, and the ( is what distinguishes the type constructor from a field or variable of that name. The body is name : Type throughout, which parse_struct_body already reads, so only the keyword differs and a flag carries it.
pub const ParsedCommand = union(enum) {
namespaced : ParsedCommandNamespaced,
flat : ParsedCommandFlat,
help : void,
};
namespace.t27 compiles and runs 2 tests. ast-check valid 295 → 296, errors 589 → 588, 0 specs worse, parse gate holds.
Small demand, stated plainly: one declaration in the corpus needs this. I did it because the alternative was leaving recovered data unlandable — not because the construct is in wide use.
31 of 31 now resolved.
The converter is NOT losing files silently — a negative result
I expected to find more of the same family. It is not there.
ancestors: 366
converted: 160
skipped: 206 "No route found for: X", one line each on stderr
The converter has a route table naming which ancestors are in t27's scope, announces every skip, and counts them. Checked against the corpus: 157 ancestors have a same-named spec in t27, 209 do not — and the ones without are upstream research specs (black_hole_information, before_big_bang, autonomous_universe_engine) that were never meant to convert.
The enum-variant bug was a silent loss with no diagnostic. This is the opposite: a declared scope, loudly enforced.
My first pass at this reported "292 behaviors, 104 functions, 95 constants missing" and every one of those numbers was my own extractor's noise — it was pulling the YAML key name out of - name: X bullets and reading # Lifecycle thresholds comment lines as declaration names. I am not publishing them. The one figure that survived scrutiny is the route-table split above.
tools/converter in the gate — already there
Added at .github/workflows/formal-yosys.yml:929, by manifest path, with the reason recorded in a comment: promoting it to a workspace member rewrites Cargo.lock, which carries someone else's uncommitted work. It cargo checks clean today.
The pre-commit hook is a different matter and I am leaving it alone: its gate logic lives in bootstrap/src/hooks.rs, which currently holds 306 lines of someone else's uncommitted changes. Adding a converter check there would entangle my change with theirs.
Three follow-ups from #2718. One is a fix, one is a negative result, one was already done.
union(enum) — the last of the 31
ParsedCommand's payloads were recovered in #2718 and could not be written down: the emitter answereduse of undeclared identifier 'union'.There is no
KwUnionin the lexer —unionarrives as anIdent, and the(is what distinguishes the type constructor from a field or variable of that name. The body isname : Typethroughout, whichparse_struct_bodyalready reads, so only the keyword differs and a flag carries it.namespace.t27compiles and runs 2 tests. ast-check valid 295 → 296, errors 589 → 588, 0 specs worse, parse gate holds.Small demand, stated plainly: one declaration in the corpus needs this. I did it because the alternative was leaving recovered data unlandable — not because the construct is in wide use.
31 of 31 now resolved.
The converter is NOT losing files silently — a negative result
I expected to find more of the same family. It is not there.
The converter has a route table naming which ancestors are in t27's scope, announces every skip, and counts them. Checked against the corpus: 157 ancestors have a same-named spec in t27, 209 do not — and the ones without are upstream research specs (
black_hole_information,before_big_bang,autonomous_universe_engine) that were never meant to convert.The enum-variant bug was a silent loss with no diagnostic. This is the opposite: a declared scope, loudly enforced.
My first pass at this reported "292 behaviors, 104 functions, 95 constants missing" and every one of those numbers was my own extractor's noise — it was pulling the YAML key
nameout of- name: Xbullets and reading# Lifecycle thresholdscomment lines as declaration names. I am not publishing them. The one figure that survived scrutiny is the route-table split above.tools/converter in the gate — already there
Added at
.github/workflows/formal-yosys.yml:929, by manifest path, with the reason recorded in a comment: promoting it to a workspace member rewritesCargo.lock, which carries someone else's uncommitted work. Itcargo checks clean today.The pre-commit hook is a different matter and I am leaving it alone: its gate logic lives in
bootstrap/src/hooks.rs, which currently holds 306 lines of someone else's uncommitted changes. Adding a converter check there would entangle my change with theirs.