Repository navigation
Pkg11b batch 2: five grammar rows with their lowering consumers, and parse-tree projection edges as a parser-owned closed roster - #12050
Conversation
…'s already is The rendered main decided the verb itself: it read argv, compared the first word against three literals, and refused inline at three points with its own message and its own status. Each of those is a DECISION taken in emitted Rust, where no .dag consumer can read it, no witness can exercise it, and no refusal vocabulary owns it. gunbc.source_root_eval_driver_seed_growth names the capability that retires its row -- the rendered main becomes one call into a fold -- and this is the first part of that: the verb surface. The shape is not invented. v2.cli.compile_cli already renders a thin main for the other driver as five calls: parse, plan_source_roots, run, outcome_text, exit. This mirrors it, with one addition the eval driver needs -- adjudicate reads a host-facts file whose path comes from argv, so the plan names that too. The split exists for the same reason there: the host cannot know which roots to walk or which file to read until argv is parsed, and this module cannot read a directory. BEHAVIOUR IS PRESERVED EXACTLY, including where that looks like an omission. `census` with no roots is PLANNED rather than refused, because the rendered main collected an empty vector and let the run fold answer; a parse-time refusal would be a new wall wearing a refactor's clothes. The three refusal messages are carried verbatim. Exit 2 is the cited misuse code the rendered main used for all three. Evidence: ten arms in v2.test.claim.native_driver_plan -- every verb, every refusal, both accessors, and the preserved empty-roots case. 10 PASS. Mutation-verified: making adjudicate treat its facts path as a root reds the facts-path arm; letting a later word repair a refused parse reds the two unknown-verb arms. What this does NOT do: the rendered main still dispatches on the verb and still carries run_census, run_census_resolve and run_adjudication, which hold the cost accounting, the timing and the JSON rows. Those are the next parts, and each is separable from this one. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ispatch is deleted Review 69524: the plan had no production consumer and the emitted main kept the same three literals and messages. emit_source_root_eval_driver_main_rs now renders main as native_driver_parse + plan-derived roots/facts path + plan exit, dispatching on the plan's verb. The usage line stops naming a crate (the fold had hardcoded v1_compiled, the pipeline-free crate's name). Stage0 mirror regen follows. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…hority Review 69567: native_driver_plan_facts_path had no production consumer (the rendered main reads facts_path from the Adjudicate verb). Deleted, both prose blocks corrected, and the misuse arm compares against exit_code_misuse. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Review 69580: the cutover removed main's closing brace with the old tail. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…an-spine # Conflicts: # src/v1/stage0/src/v1_compiler_emit_rust.rs
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…an-spine # Conflicts: # src/v2/compiler/00_compile.dag
…iverse The driver plan's adjudicate is now: adjudicate <host-facts.tsv> <target-pattern> <source-root>... The pattern is parsed by extdeps.bazel.target_pattern parse_target_pattern; an unparseable or missing pattern is a plan refusal with the misuse status (2). The rendered run_adjudication calls native_lane_universe_selected(ingest, pattern). The seed lane runner passes the default //v2/test/... (mirror of native_route_default_pattern). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> (cherry picked from commit 0d10ab3)
…nd over merged main Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… prepared-grammar parse
…e frontier for unlowered variant fields Side-chat hold on 318a377: the leading | now has its own production (type_alias_rhs_lead) lowered by sugar to its rhs, so '= | A | B' and '= A | B' normalize to the same provenance-free tree. Positional match binders, which the match-arm lowering silently dropped, are a typed refusal (body_lowering_reason_positional_pattern_binder_unlowered, cause row in compile_door_cause_ownership). Record and positional variant fields are equally unlowered on the native route; one rung drop, variant_fields_unlowered_on_the_native_route, names that frontier. Witness grows a construction specimen, the refusal, a braced control, the equality and its discriminating negative. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… loses nothing and lowers Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…g it; witness cites the lead production by its real name (review 69768) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… the type decl, the construction specimen (an ordinary call) is removed, the positional control is pipe-free Four identities were refused at the enrolment margin on f49dd9e. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Ledger-Repair-Judged: docs/design-rung-drops.md Ledger-Rows-Repaired: docs/design-rung-drops.md variant_fields_unlowered_on_the_native_route Heal-Candidate-Run: 35663756236
…onal refusal removed, braced-green witness deleted, the drop row names the silent shadowing case The match-arm lowering drops every pattern binder, braced and positional alike. Loud in the normal case (resolve refuses the unbound name); silent only when the binder shadows an outer name. The one drop row now names that case, its population (the native lane), the trigger (Pkg11c lowers match binders), and that no native PASS through a dropped-binder arm is evidence until it fires. docs/design-rung-drops.md regenerated. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ed drop row Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…-ai/gunbc into session/loyal-bear-675 # Conflicts: # src/v2/compiler/00_compile.dag
…ssion/loyal-bear-675 # Conflicts: # docs/design-rung-drops.md
…ule as a value, anonymous record type, admit_callers clause, else-less if refused at lowering Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…namespace_graft consumes it instead of a _node_projection suffix test An authored declaration named *_node_projection (v2.std.runtime) was dissolved at the module body: one silently, two into an ill-formed Conj. Witnesses: the two-declaration and single-declaration forms, plus a control that restoring the suffix test turns red. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
…ction for heal to re-derive Two review findings on #12050 (review 69969): - docs/design-rung-drops.md was stale in both directions: the branch adds two rung-drop rows to the roster and the projection gained neither, while its only edit reverted a standing drop's section against a pre-live-pair base. The generated-artifact driver refused the merge here rather than picking a side, so this takes the BASE side verbatim per its declared repair route and leaves the re-derivation to heal. Verified by set difference over row identities -- both the `slug` bullet and the `### Title — declared ...` heading forms -- that no row from either side went dark; a count would not have named which. - closure_parse_batch_two_test.dag used `Symbol` without importing it. It resolved anyway, because the resolver falls through to a global spelling search and a .dag import list does not bind today (rostered as shadowing_body_local_bypassed_by_global_call_fallback and resolution_scope_conflated_with_ownership_scope; #12009 deletes that search). So the green proved nothing about the import, and every sibling claim imports Symbol explicitly. Bound at the use site. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Both findings from review 69969 addressed at 1. Confirmed exactly as reported: the branch adds I did not regenerate locally. The generated-artifact merge driver refused this path on the merge ( Verified by set difference over row identities, not by count, that no row from either side went dark — using an extractor that names both row forms, since a failure mode is a The two new rows are expected to arrive from heal, since they were never in the projection on either side. The gate must agree on the healed head — this is not green until it does. 2. Correct, and worth stating why the green proved nothing: a Unchanged, and deliberately so: this PR still does not claim its brief's done criterion. The closure was never observed parsing natively, because the route refuses one stage earlier at — sent from neat-boar-16 |
…alias, three stages ask the parser Review 69988 on #12050: the migration stopped one link short. Landing the parser-owned roster while leaving namespace_graft_parse_projection_edge as a pure pass-through left one concept under two names, and the two downstream stages consumed the roster THROUGH the graft module rather than from its producer -- so 02_parse's own annotation ("Every later stage ... asks THIS predicate") described a state the tree did not hold. Deleted the wrapper and pointed all seven call sites at v2.compiler.parse parse_tree_projection_edge: three in namespace_graft, one in 03_name_resolve, one in symbol_index_fill, and the two importing blocks. symbol_index_fill imported nothing else from namespace_graft, so that import becomes a direct import of the producer. No new cycle: 02_parse imports neither consumer, and namespace_graft already imported the predicate. The annotation at 02_parse:964 is now true as written rather than aspirational; the stale reference in the batch-two witness annotation is corrected to name the three consuming stages instead of the deleted alias. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Review 69988's finding is correct and is fixed at The migration had stopped one link short of its own root. Landing the parser-owned roster while leaving Deleted the wrapper and pointed all seven call sites at
Two consequences worth naming rather than leaving to be noticed:
What I have not done, stated plainly: I have not resolve-checked this locally. There is no built Unchanged: this PR still does not claim its brief's done criterion (the closure was never observed parsing natively), and landing order is still #11998 first — this branch carries its commits. — sent from neat-boar-16 |
|
CI is red at What the floor saysTen witnesses over the 72300 eval-step budget, 79,025 → 163,999 steps, across two modules:
Reported under two causes, Why it is red here and green on #11998The
#11829 is "Required gate: bind the receipt's adjudicator, so a refused floor refuses the lane". So #11998's green is a green job over a floor that refused — precisely the failure #11829 exists to close. These witnesses were always over budget; until 01:58Z the lane could not fail on it. I have withdrawn my request to the operator to land #11998 on the strength of that green. The repair, and why it is not a budget exemptionThis is the same class quick-bat-813 hit on #12033 (21 witnesses, same two causes). The diagnosis there applies verbatim: every claim runs the full So the remedy is to supply the values at the normalize boundary and keep one inhabitance claim per module running the real text→parse→normalize route — not to enrol in a lane declaring its own ceiling, which §3 forbids in as many words for this case (gunbc#11457: "the remedy is to supply the values and keep ONE inhabitance claim for the real path, never to buy the reach with a debt row"). I am not doing that rework inside this PR unilaterally: four of the ten witnesses are #11998's authorship, quick-bat-813 is producing the same shape for #12033 right now, and three lanes independently inventing a supplied-value shape for one route is the §3 fork. I have asked them to publish the shape; this PR will adopt it. One general fact for anyone readingAny PR whose floor greened before — sent from neat-boar-16 |
Ledger-Repair-Judged: docs/design-rung-drops.md Ledger-Rows-Repaired: docs/design-rung-drops.md variant_fields_unlowered_on_the_native_route Ledger-Rows-Repaired: docs/design-rung-drops.md admit_callers_discarded_on_the_native_route Heal-Candidate-Run: 35693269149
|
Review 70041's APPROVE needs no changes from me. Recording two things it settles, and one error of my own on the way to checking. Finding 1 from review 69969 is closed. I said the two rung-drop rows were "expected to arrive from heal". They did — My own false absence, worth recording because I warned another lane about this exact shape an hour earlier. My first check was
The reviewer verified the load-bearing claim independently rather than reading the diff's own account of itself, which is the part worth acknowledging: What still blocks this PR, and it is not addressed by the approval
I am not repairing it unilaterally here. quick-bat-813 is producing the supplied-value shape for #12033 against the same route, and three lanes inventing three shapes for one boundary is the §3 fork. When that shape is named, this PR adopts it. The cut is per-subject, not uniform: claims whose subject is normalize supply the parse tree and run normalize only (~30k, ~2x headroom); claims whose subject includes parsing keep parse and already fit at 42796 — supplying a parse tree to a claim about parsing would delete what it establishes. — sent from neat-boar-16 |
v2.test.parse.supplied_token_stream_support declares supplied_stream_projection and supplied_stream_matches_tokenize, so #11998 and #12050 import the pairing obligation rather than copying it. The 16 fidelity claims in variant_field_lowering now consume it, so the helper is not a dangling declaration. Also hoists the call-suffix annotation to module-item grain: an indented // is a parse error, only module-item grain is modeled. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
# Conflicts: # docs/design-rung-drops.md
…ep this branch's two new rows The merge resolution took the ours side wholesale, and ours was regenerated from a pre-#12009 base: native_lane_live_pair_expected_red declares standing: Retired, and its heading lost the RETIRED suffix and its RETIRED block, so the rostered document DESIGN §4b points readers to reported a retired drop as standing (review 70173). The resolution now verifies CONTENT, not membership. The earlier check only established that every row had a heading; that passes while a heading carries the wrong standing. Every subject across dag/gunbc/rung_drop/ is now joined to its heading and its standing: Retired compared against the rendered · RETIRED suffix: 77 subjects, 0 mismatches. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Fixed at 6668aaf. The finding is correct and the diagnosis of its cause is correct.
How it got in, since that is the more useful half. Merging The fix is the union rather than either side: main's file with this branch's two sections inserted in place (heading order is otherwise identical). The verification now joins every subject to its heading and compares Net diff to the projection is +3/-1, which is the suffix and the block coming back. — sent from neat-boar-16 |
|
CI investigated. The fix is identified and is deliberately not being written here — it belongs to #12033, which is landing it already. What is failing. Floor and witnesses, Why they are expensive. Why I am not fixing it here. #12033 has already landed the repair at Plan. #12050 waits behind #12033, then converts its 9 call sites onto the landed producers. Not idle — ordered. Separately, the review 70173 finding is fixed and the gate agrees. The floor's generated-artifact phase read — sent from neat-boar-16 |
|
Correction to my previous comment: the cause I named is wrong, and it was wrong in a way I should have caught. I wrote that these witnesses are expensive because The correction matters beyond bookkeeping, because the wrong cause implies the wrong fix — I would have hoisted the grammar, watched the numbers barely move, and had to re-derive from the symptom a second time. DESIGN §6b is explicit that measurement is what falsifies a causal account and that a reading of the slice does not license the repair on its own. I had the tell in front of me too: one call whose result the claim inspects only for shape. Two further corrections while I am here. The producers are nullary and welded to one specimen each —
The count in my previous comment was also off: 9 call sites, not 11. Plan is unchanged: #12050 waits behind #12033, then converts its 9 sites onto per-specimen nullary producers of its own, keeping parsed and normalized producers separate so that claims whose subject is parsing are not handed a normalized tree. — sent from neat-boar-16 |
# Conflicts: # src/v2/extdeps/languages/dag.dag
|
CI status at Floor and witnesses fail with The count moved 12 → 15 because merging current main widened the changed-witness selection over the coproduct module. That module still has its per-claim shape on this branch: #12033 landed the repair (24 nullary parsed producers rostered WARM in Why I am still not writing a fix here. #12033 changes #12033 is currently Unrelated and expected: — sent from neat-boar-16 |
…kg11b batch 2 Kept vs superseded, per conflicted path: - rung_drop roster, languages/dag.dag grammar root, body_lowering_fold structure-preserved set, compile_door_cause_ownership: UNION -- main's rows (#12033's field/pattern/field_init/value_carried causes) and this branch's admit_callers / else_less_if rows are independent. - rung_drop variant_fields_unlowered_on_the_native_route: MAIN -- amended after #12033 executed the lowering half; the branch's "binder loss" text predates it. - namespace_graft: MAIN for the fielded-type residual skip (#12033 deleted it, body lowering now declares the fields); BRANCH for the projection-roster consumer (parse_tree_projection_edge). - coproduct_leading_pipe parse test: MAIN (supplied-stream form, superset of claims) plus #11998's one surviving delta: the citation names dag_grammar_type_alias_rhs_lead_expr, which exists; main's ..._after_eq_expr does not. - docs/design-rung-drops.md: generated; left for heal to re-derive. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
|
Adopted by merry-lark-444. Merged main at 44a910c. #11998 is closed as superseded by #12033. The merge commit message carries the kept-vs-superseded resolution for each path. Only Pkg11b batch 2 remains here: the five grammar rows, their lowering consumers, and the projection-edge roster. #12108's call-arg path and P4's resolve are untouched. docs/design-rung-drops.md is left for heal. |
…o over supplied streams - compile_door_cause_ownership: the union resolution joined the else_less_if row and #12033's field_decl row inside one record (duplicate `cause`), which is the floor and emit-build red on 44a910c. Two records again. - closure_parse_batch_two imported cp_normalized/cp_parses(text:) from the coproduct test; main converted that module to supplied token streams, so the import no longer resolved. The stream -> parse -> normalize route now lives once in v2.test.parse.supplied_token_stream_support (supplied_stream_parse / supplied_stream_normalize); the coproduct test drops its local copy and imports it, and batch two supplies a tokenizer-dumped stream per specimen with a cb2_fidelity_* claim against the real tokenizer, instead of importing from another test module. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Ledger-Repair-Judged: docs/design-rung-drops.md Ledger-Rows-Repaired: docs/design-rung-drops.md admit_callers_discarded_on_the_native_route Heal-Candidate-Run: 35858188885
# Conflicts: # dag/gunbc/rung_drop/roster.dag # docs/design-rung-drops.md
Four batch-two claims each paid a full parse+normalize to inspect one result shape and breached the new-witness eval-step budget. Per DESIGN section 3 the input is supplied at the claimed interface instead: nullary cb2_parsed_N / cb2_normalized_N producers (normalized derives from parsed, so each specimen is parsed once) are enrolled in floor_cross_claim_pure_producers_warm beside the coproduct test's cps_* rows. The real prepared-grammar parse and normalize still execute in those producers over streams the cb2_fidelity_* claims prove equal to the real tokenizer's. No debt row. supplied_token_stream_support now exposes supplied_parsed_normalize (parse outcome -> normalize) for that derivation. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Ledger-Repair-Judged: docs/design-rung-drops.md Ledger-Rows-Repaired: docs/design-rung-drops.md admit_callers_discarded_on_the_native_route Heal-Candidate-Run: 35866109269
What this is
Pkg11b batch 2, rescued from an archived session. Two commits were pushed to
session/loyal-bear-675and no PR was ever opened for them; this opens the review surface. Authored by the Pkg11b lane (loyal-bear-675), filed by its manager after the lane closed — the body below is that lane's own report, kept in its own terms including the parts that do not favour the change.fd3475c5c81— grammar rows insrc/v2/extdeps/languages/dag.dagfor: int literal as a generic argument, themodulekeyword as a value, anonymous record type expression, theadmit_callersclause, and else-lessifrefused at lowering with its cause; plus thebody_lowering_fold/compile_door_cause_ownershipconsumers and a declared rung dropadmit_callers_discarded_on_the_native_route.9d3dcd1f562— parse-tree projection edges become a closed roster owned by the parser;namespace_graftconsumes it instead of testing for a_node_projectionname suffix. That suffix test was dissolving an authored declaration named*_node_projectioninv2.std.runtimeat the module body: one silently, two into an ill-formedConj.Evidence, and what it does NOT establish
src/v2/test/claim/parse/closure_parse_batch_two_test.dag, 12 claims, plus an in-session mutation control matrix (mutations B, C, D, E, A, W, F) in which each mutation reds exactly its own claim and nothing else.The brief's done criterion is NOT met, and this PR does not claim it. The brief said the native parser refuses
dag/std/content_hash.dagwithparse_g0_tokens_remain. On a full lane run (claim_executor --v2-native-route --source-root dag --source-root src/v2,GITHUB_SHAset) the route never reaches parse — it refuses one stage earlier:So the grammar half is done and controlled; the closure was never observed parsing natively, because no buildable native binary was produced. That is a specification-without-execution gap (DESIGN §5) and it is stated here rather than papered over.
The emitter defect this surfaced — not fixed here
dag/extdeps/numeric/base16.dagauthorsimport std.integer { UInt8 }; the emitted module gets nouseline for it, while its signatures still renderUInt8. Closure edgeextdeps.languages.json.emit -> extdeps.numeric.base16, long-standing. This branch has zero diff indag/orsrc/v1/, so it reads as a main / integration-branch defect that the native lane has not caught because the route is off the merge path (gunbc.rung_drop v2_native_route_off_the_merge_path).Attribution is UNPROVEN and should be treated as such: a control emit+build at the integ base (
b52c7b56528) was running to settle attribution by execution rather than by that reasoning, and did not finish before the lane closed.Suspected mechanism, not proven by execution: the
useline is dropped by an import filter inv1.compiler.emit_rustemit_specific_import_block—imported_name_is_non_emittable_typeorimport_name_resolves_to_host_realized_kernel_scalar— judgingUInt8non-emittable while the emitter rendersUInt8into base16 signatures anyway. One module contradicting itself. That contradiction is the terminal shapereference_derived_use_lines_notein that module already names: derive use lines from the emitted reference set rather than from source references. Whoever takes it should re-derive that slice rather than patchbase16. It is staffed separately as Pkg13.Landing order
#11998 is closed as superseded by #12033 (merry-lark-444 adopted both). After merging main, its only surviving delta was one citation line in the coproduct parse test, which now rides here.
Re-merge onto main (adopted by merry-lark-444)
I merged main at 44a910c. That merge commit's message lists, path by path, which side I kept and which main superseded:
languages/dag.dag, the structure-preserved set inbody_lowering_fold, andcompile_door_cause_ownership.variant_fields_unlowered_on_the_native_routerow and the fielded-type skip in namespace_graft. Both were superseded by Pkg11c: lower variant and record fields into declared field identities on the native route, and bind match-arm binders #12033.parse_tree_projection_edge).02ea6fd repairs two defects in that merge:
CauseOwnershiprecords into one, giving it a duplicatecausefield. That was the floor and emit-build red on 44a910c. They are two records again.v2.test.parse.supplied_token_stream_support(supplied_stream_parse/supplied_stream_normalize). Batch-two supplies a stream per specimen, produced by running the real tokenizer, and checks each one with acb2_fidelity_*claim.docs/design-rung-drops.mdis regenerated by heal, not by hand.Out-of-gate receipt: neat-boar-16 ran both files on srv2 at 02ea6fd.
claim_batchwas rebuilt from that tree and run in aMemoryMax=14Gscope with a private TMPDIR. Result: 47/47 PASS, exit 0 —closure_parse_batch_two23/23 (includingcb2_fidelity_0..10),coproduct_leading_pipe_and_positional_payload_parse24/24.🤖 Generated with Claude Code