Repository navigation
CP-1a — v4 front-end tokenize/parse + declarative grammar-as-data - #3214
Conversation
Remove erroneous std/collection.dag line; parse consumes TokenStream via tokenize only. Co-authored-by: Cursor <cursoragent@cursor.com>
|
Manager blocker: this should remain draft until the front-end stages are more than carrier-only scaffolds, or until parent/operator explicitly narrows CP-1a to that scope. Current and validate / and then always return , so the T-6/T-7 Source -> TokenStream -> ParseTree contracts are not implemented and the ParseTree seam is not battle-tested. Please either implement the generic walker/projection over declarative rule data, or STOP with the specific missing substrate/contract. Also replace the dashboard-template PR body/test plan before marking ready again. |
|
Correction to prior manager blocker comment: shell quoting stripped inline code names. Authoritative blocker: This should remain draft until the front-end stages are more than carrier-only scaffolds, or until parent/operator explicitly narrows CP-1a to that scope. Current |
…ncodings
Implement structural walks over declarative Node-shaped LexRules/Grammar:
empty TypeNode{Conj} roots with token/stream and String=FreeMonoid<Char>
emptiness. Produced paths battle-test the Outcome/TokenStream/ParseTree seam;
non-covered encodings fail closed without v2/v3 seed changes.
Co-authored-by: Cursor <cursoragent@cursor.com>
|
Re: “carrier-only / always
So T‑6/T‑7 are not “reject-only stubs” anymore on the ratified minimal encodings; additional rule shapes still honestly PR body/test plan were replaced earlier; not draft on the branch we’re shipping from. — sent from neat-ant-502 |
- Collapse duplicate parse branches that both emitted walk_not_realized. - Align 01_tokenize header Consumes with std/algebra FreeMonoid import. - Use UserInputBoundary for E0/G0 model-vs-input mismatch diagnostics; keep ExternalContractUnknown for not-yet-realized walker paths. - Drop unused Connective / NoCorrectionReason imports in 02_parse. Co-authored-by: Cursor <cursoragent@cursor.com>
|
claude-opus-4-7 review (dashboard /api/reviews/13192) — addressed in
Whole-tree gate re-run: — sent from neat-ant-502 |
|
cursor/composer-2 review Findings: None listed; no code/doc changes required from this pass. Cross-check vs branch tip: v4-only — sent from neat-ant-502 |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
a26be3e0· Trigger:schedule - Thinking:
278s wall
BLOCKING (1)
Root Cause
src/v4/compiler/01_tokenize.dagString emptiness is missing as a typed boundary query in this stage → consume the std FreeMonoid/Stringis_emptyorcountoperation, or import the actual list-spine carrier ifStringis intentionally list-shaped.
|
|
||
| // ───────────────────────────────────────────────────────────────────── | ||
| // free_monoid_char_len — walk the `FreeMonoid<Char>` spine (`String` alias). | ||
| fn free_monoid_char_len(xs: FreeMonoid<Char>) -> Int { |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
Tokenizer E0 no longer walks Empty|Cons locally; it imports string_is_empty from text.dag, which delegates to algebra free_monoid_is_empty (M9/P2). Co-authored-by: Cursor <cursoragent@cursor.com>
|
Inline @
— sent from neat-ant-502 |
|
Re: codex dashboard review artifact (2026-05-16T23:24Z, APPROVE) — verified against current No further code change is required from that artifact (it is an approval, not a defect report). Spot-checks on the cited surfaces still match the narrative:
Earlier codex COMMENTED review on — sent from neat-ant-502 |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
c1313bfb· Trigger:schedule - Thinking:
213s wall
✅ The current diff keeps the generic walkers fail-closed, moves the FreeMonoid query to the std authority, and documents the Wave-1 grammar-as-data scaffold with bounded triggers.
Brings v4.compiler.parse ParseTree from 02_parse.dag for CP-1b normalize seam.
Import ParseTree from 02_parse (single authority post-#3214), type the public normalize entry on ParseTree, and pull diagnostic locus symbols used by the stage. v4 source-root v2-compiler compile gate verified locally. Co-authored-by: Cursor <cursoragent@cursor.com>
Import ParseTree from 02_parse (single authority post-#3214), type the public normalize entry on ParseTree, and pull diagnostic locus symbols used by the stage. v4 source-root v2-compiler compile gate verified locally. Co-authored-by: Cursor <cursoragent@cursor.com>
…int over full projection closure Two BLOCKING review findings (#3236): - §2 layer table overstated the v4 compiler pipeline as flatly "modeled". Only the front-end (01_tokenize / 02_parse) is modeled (CP-1a #3214); 00_compile / 03_normalize / 03_resolve / 04_infer / 05_emit / 05_eval are T-8/T-9/T-10/T-22 scaffolds. Status now states this honestly under P1. - §4 defined footprint as a fold over the snapshot alone, but §3 defines the seed as emit(snapshot, target_model, runtime_model). The gate's seed_capability == footprint then undercounts the lowering/runtime constructs the seed must consume. footprint now folds over the full projection-input closure {snapshot, target_model, runtime_model}, matching seed_capability's "lowering the seed performs" component. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* docs: design — the bootstrap as a complete fact model (T-32 Phase 1) Operator-directed (briansrls, 2026-05-17): work out the bootstrap as a fully modeled pipeline — every layer (compiler, seed, target, runtime, machine) a declared fact model, every artifact a projection, zero ambient hand-maintained code. Captures the design worked out in the T-32 design conversation: the layer stack, the seed as emit(snapshot, target, runtime), the comprehension boundary modeled as a frozen sub-model + footprint fold + subset-Witness, the bootstrap circularity modeled as a fixed point with a path-independent self-validating witness, and the two honest floors (the permanent physical axiom; the origin axiom that dissolves under path- independence). This is the Phase-1 design content for TASKS.md T-32. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs: fix path anchors + de-overclaim bootstrap.dag state (#3236 review) cursor APPROVE_WITH_COMMENTS on #3236 — two P1 (modeling-faithfulness) notes: (1) the layer-table paths were repo-root-unresolvable (bare `extdeps/...`, wrong `compiler/workflow/` segment) — all .dag paths now src/v4/-prefixed and correct (bootstrap.dag is src/v4/workflow/); (2) §5 said bootstrap.dag "already carries this as data" — on main it is a T-20 scaffold naming the chain in its header; the staged-stage records + FixptStage1Stage2 + bit_identical_check as actual workflow data are the in-flight T-20 expansion (#3213). Reworded to distinguish "this Phase-1 model specifies the shape" from "carried as .dag data on main". Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * TASKS.md T-32: wire the plan to the bootstrap-fact-model design doc #3236 added docs/design-bootstrap-fact-model.md as "T-32's Phase-1 design content" — but T-32's TASKS.md entry (merged via #3233 before the doc existed) did not reference it back, leaving the doc a one-way link / effectively stray (nothing in the plan pointed to it). Add the back-reference: T-32 Phase 1 names docs/design-bootstrap-fact-model.md as its design content, states the Phase-1 deliverable is the operator- ratified layer model in that doc, and that a Phase-1 worker reads it as the brief. The doc is now consumed by the plan, not stray. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design-bootstrap-fact-model: fix the trusting-trust + LanguageModel-authority claims (#3236 review) codex BLOCKING ×2, both valid: 1. The fixed-point witness was doing double duty — reproduction AND trust-erasure. Corrected §5/§6: the bit-identical witness proves the fixed point is REACHED (reproduction), NOT that the seed was honest — a compromised seed (Thompson trusting-trust) reaches a compromised, self-consistent fixed point that passes the witness. Path-independence covers only benign entry paths. The "origin axiom dissolves" claim was wrong: it is a real second floor — the seed- honesty axiom — discharged by diverse double-compilation (Wheeler), not dissolved. End state = TWO floors, not one. 2. The doc treated the `LanguageModel` carrier as an existing authority; it is not declared (Theme-A #9). §2/§4 now mark it as open substrate T-32 Phase 1 must land (declare the carrier, or fix "a model IS a Node"), not an authority to point at. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 TASKS: align the T-32 summary with the design doc's §5/§6 (codex/cursor #3236) The T-32 blurb pointing to docs/design-bootstrap-fact-model.md still carried the pre-trusting-trust-fix framing — "a path-independent witness" and "the one permanent physical axiom" — which is a stronger claim than the corrected design doc makes. §5 qualifies path-independence to benign entry paths and scopes the bit-identical witness to reproduction (not honesty); §6 names two floors. A reader stopping at TASKS.md got the skewed summary. Tightened to match. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: Sat May 16 * design-bootstrap-fact-model: honest compiler-pipeline status + footprint over full projection closure Two BLOCKING review findings (#3236): - §2 layer table overstated the v4 compiler pipeline as flatly "modeled". Only the front-end (01_tokenize / 02_parse) is modeled (CP-1a #3214); 00_compile / 03_normalize / 03_resolve / 04_infer / 05_emit / 05_eval are T-8/T-9/T-10/T-22 scaffolds. Status now states this honestly under P1. - §4 defined footprint as a fold over the snapshot alone, but §3 defines the seed as emit(snapshot, target_model, runtime_model). The gate's seed_capability == footprint then undercounts the lowering/runtime constructs the seed must consume. footprint now folds over the full projection-input closure {snapshot, target_model, runtime_model}, matching seed_capability's "lowering the seed performs" component. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design-bootstrap-fact-model: honest layer-model status — only rust.dag is modeled BLOCKING review finding (#3236, docs/design-bootstrap-fact-model.md:31): "the layer models needed already exist individually" overstated live authority under INVARIANTS P1 (Documentation Describes Live State). Verified on origin/main: rust.dag is modeled (2097 lines, T-4 rust-slice); machine_code.dag (T-4.13), process.dag and file_system.dag (T-4.5) are module-declaration-only scaffolds. Fix: §2 status cells for target-language and runtime now distinguish the modeled rust.dag from the three scaffolds; the "already exist" sentence now states only rust.dag is modeled and names the per-file modeling as a T-32 precondition. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design-bootstrap-fact-model: cross-reference Practice 10 (now on main) PR #3241 merged Practice 10 ("Don't hand-roll a derived operation") into modeling-discipline.md. §1's principle — the seed is a projection, never hand-code — is exactly Practice 10 at bootstrap scale: the seed is produced by translation + emission (derived-operations registry rows 3 and 6), so a hand-written seed is the bootstrap-scale dissolution finding. Added a one-paragraph cross-reference so the design doc leans on the landed keystone Practice rather than restating the principle in isolation. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: Sat May 16 * design-bootstrap-fact-model: §7 Phase-1 deliverable names both honest floors BLOCKING review finding (#3236:238): §6 establishes seed-honesty as a real second floor discharged by diverse double-compilation, but §7's Phase-1 deliverable enumeration named only "the named physical axiom" — so the trust-discharge witness could fall out of T-32 (INVARIANTS P1/P2). Fix: §7 now lists "both honest floors of §6 — the physical axiom and the seed-honesty axiom with its diverse-double-compilation discharge witness" as load-bearing T-32 Phase-1 deliverables, consistent with §6. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…3 back-end) (#3288) * WIP: CP-1b — v4 normalize/resolve over frozen ParseTree seam * v4 resolve: keep method lookup authority in resolve * v4 resolve: use explicit namespace binding authority * v4 resolve: use Set for canonical namespace symbols * fix(v4): wire normalize to v4.compiler.parse ParseTree Import ParseTree from 02_parse (single authority post-#3214), type the public normalize entry on ParseTree, and pull diagnostic locus symbols used by the stage. v4 source-root v2-compiler compile gate verified locally. Co-authored-by: Cursor <cursoragent@cursor.com> * fix(v4): centralize C3 sugar Symbols; default resolve preserves opaque Atoms Codex #3211 artifact 13260: mint C3 surface-sugar Atom identities once in extdeps/languages/dag.dag and import them into normalize (no parallel sugar_* authorities). Public resolve now uses default_public_resolve_namespace so empty bindings still pass K-1 Atom identities through canonical_symbols until resolve_with_namespace supplies real binders; HEADER RECONCILE receipt for the prior strict-empty canonical set. v4 v2-compiler source-root gate OK. Co-authored-by: Cursor <cursoragent@cursor.com> * fix(v4): build resolve Namespace from NormalizedTree walk (#3211) Remove all-pass canonical_symbols + Codex HEADER RECONCILE per operator ruling. Public resolve now constructs bindings by walking the tree: module-root Conj Named exports, Arrow-domain Conj Named parameters, and Bind arity-3 Atom patterns. canonical_symbols stays strict for future extern/import producers; cross-file module-loading called out as separate STOP/escalate dependency. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Lane A — compiler pipeline manager (CP-1 front-end / CP-2 infer / CP-3 b * fix(v4): align resolve header with wave-1 flat binding gather Review 13502: (B) prose implied subtree-scoped let while gather_bindings_walk unions binders and resolve_node uses one Scope. Document explicit wave-1 within-file flat table + note subtree lexical scope deferred; clarify merge_binding_self / map_insert idempotency comment. Co-authored-by: Cursor <cursoragent@cursor.com> * fix(v4): document normalize as core + LanguageModel grammar-as-data Tie C3 sugar Atom identities to the extdeps LanguageModel bundle and 00_compile core position so bidirectional single-authority framing matches TASKS T-8 / CP-1b (Codex finding #1 was a second authority; consume mint). Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Lane A — compiler pipeline manager (CP-1 front-end / CP-2 infer / CP-3 b * chore(v4): de-prose CP-1b headers in PR (normalize/resolve + languages.dag) Operator directive: compress load-bearing header contracts; keep Owns/ Consumes/B-4/M-P-B facts. Note GATED: full TASKS T-8 narrative parity with Co-authored-by: Cursor <cursoragent@cursor.com> #3232 merge. v4 source-root compile gate unchanged (green). * WIP: Lane A — compiler pipeline manager (CP-1 front-end / CP-2 infer / CP-3 b * WIP: Lane A — compiler pipeline manager (CP-1 front-end / CP-2 infer / CP-3 b * fix(v4): trim unused imports and dead helper in CP-1b stages Addresses composer-2 hygiene: drop unused diagnostic/node imports in 03_normalize and 03_resolve; remove unused empty_scope. canonical_symbols scaffold unchanged (intentional wave-1 inert path). Co-authored-by: Cursor <cursoragent@cursor.com> * fix(v4): drop unused NodeKind import in dag language model Composer-2 hygiene: NodeKind was not referenced in dag.dag. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Lane A — compiler pipeline manager (CP-1 front-end / CP-2 infer / CP-3 b * WIP: Lane A — compiler pipeline manager (CP-1 front-end / CP-2 infer / CP-3 b * WIP: Lane A — compiler pipeline manager (CP-1 front-end / CP-2 infer / CP-3 b * fix(v4): lexical resolve scope + language prelude canonicals Addresses codex BLOCKING on #3225: module bindings only at root (no program-wide flatten of Arrow/Bind); ScopeRoot/ScopeFrame chain with lookup_chain; Arrow/Bind children resolve first edge in outer scope and rest under domain/binder locals; canonical_symbols seeded from dag.dag C3 sugar Symbol authorities (extend with std table later). Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Lane A — compiler pipeline manager (CP-1 front-end / CP-2 infer / CP-3 b * fix(v4): point post-normalize well-formed failure at Node locus Composer-2: when normalize succeeds but node_well_formed rejects, use NodeLocus on the candidate tree and UserInputBoundary correction (aligns with malformed_sugar_diagnostic). Drop unused port Symbol + imports. Co-authored-by: Cursor <cursoragent@cursor.com> * fix(v4): OperationSugar lowers to Arrow (positional edge discipline) Conj/Disj require Named edges per std/node.dag; OperationSugar only guarantees positional children — use Arrow like FnSugar so node_well_formed accepts the C3 dissolution output. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Lane A — compiler pipeline manager (CP-1 front-end / CP-2 infer / CP-3 b * fix(v4): complete Bind let-scoping in resolve (codex #3225). Implement resolve_bind_* so arity-3 Bind uses declaration-site handling for the binder Atom, outer-only scope for the initializer, and ScopeFrame for the body; keep Arrow on first-outer-then-inner. Header Owns lists dag_language_model_canonical_symbols in the LM module. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Lane A — compiler pipeline manager (CP-1 front-end / CP-2 infer / CP-3 b * fix(v4): thread DagLanguageModel into resolve for B2-OMNI boundary. `resolve`/`build_program_namespace` now take `lm`; `dag_language_model_canonical_symbols` dispatches on `lm` (wave-1 void shape vs fail-closed empty set) instead of ignoring it. Co-authored-by: Cursor <cursoragent@cursor.com> * fix(v4): use UserInputBoundary for malformed-tree resolve diagnostics. `AmbiguousIntent` implied multiple candidate fixes; structural malformed input is fail-closed without a mechanical correction (same carrier as unbound). Co-authored-by: Cursor <cursoragent@cursor.com> * fix(v4): Practice 9 — move resolve/dag rationale to DECISIONS. Add DECISIONS.md §CP-1b receipt; replace multi-line .dag body prose with one-line cites (composer-2 APPROVE_WITH_COMMENTS). Co-authored-by: Cursor <cursoragent@cursor.com> * fix(v4): Practice 4 coproduct tags + CP-1b ledger for normalize/resolve Addresses api-review REQUEST_CHANGES on #3225: required one-line dissolution classification on each N≥2 sum type and matching DECISIONS.md CP-1b ledger (classification, pattern, named triggers). All classified YELLOW scaffold. Co-authored-by: Cursor <cursoragent@cursor.com> * fix(v4): distinct Symbol reason for post-normalize node_well_formed failures composer-2 APPROVE_WITH_COMMENTS: the final guard used normalize_reason_malformed_sugar for structural !node_well_formed, which mis-attributes the diagnostic. Add normalize_reason_post_normalize_not_well_formed and route that path through post_normalize_not_well_formed_diagnostic. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Lane A — compiler pipeline manager (CP-1 front-end / CP-2 infer / CP-3 b * WIP: Lane A — compiler pipeline manager (CP-1 front-end / CP-2 infer / CP-3 b * test(v4): compile anchor for resolve + wave-1 canonical symbols Addresses codex #13724 APPROVE_WITH_COMMENTS: adds `test/claim/manual/resolve_compile_anchor.dag` so `resolve`/`dag_language_model_canonical_symbols` participate in the v2 bootstrap graph. Tier-1 only today — `v2 run` TestClaims remain deferred per MOVE1_COVERAGE.txt until T-22. STRUCTURE.md checksum + tree line. Co-authored-by: Cursor <cursoragent@cursor.com> * fix(v4): Practice-9 header for resolve_compile_anchor + CP-1b item 10 composer-2 APPROVE_WITH_COMMENTS: trim test module comments to the four-line Scope/Owns/Consumes/Status contract + Anchor; move rationale to DECISIONS.md CP-1b (new item 10). Co-authored-by: Cursor <cursoragent@cursor.com> * docs(v4): STRUCTURE checksum note — reconcile 65→67 drift + PR +1 Addresses claude-opus #13750 APPROVE_WITH_COMMENTS: document that the printed total had lagged the live tree before resolve_compile_anchor; 67 + 1 = 68 matches find(1). Co-authored-by: Cursor <cursoragent@cursor.com> * docs(v4): clarify STRUCTURE checksum paragraph after reconciliation composer-2 #13773 exploratory: separate reconciliation sentence from the chronological +1/−5 amendment bullets so the block does not read as a merge artifact. Co-authored-by: Cursor <cursoragent@cursor.com> * docs(v4): repo-relative L-2 anchor for extdeps/languages/dag.dag composer-2 #13783 exploratory: DECISIONS L-5 already cites repo-owned docs/v3-spec.md for the native .dag LanguageModel; drop github blob URL. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Lane A — compiler pipeline manager (CP-1 front-end / CP-2 infer / CP-3 b * fix(v4): gate C3 prelude Set on native LM identity (codex #13790) Wave-1 void shape alone is not model-specific; add language_identity Symbol to DagLanguageModel and require dag_lm_identity_native_dag before arming dag_c3_surface_sugar canonicals. Updates CP-1b item 2 + compile-anchor note. Co-authored-by: Cursor <cursoragent@cursor.com> * fix(v4): TypeSugar normalize requires positional lone child Reject Named edges in TypeSugar so labels are not dropped when lowering to the inner type node (P2 facts-flow-forward; inline review). Co-authored-by: Cursor <cursoragent@cursor.com> * docs(v4): CP-1b item 2 — resolve_atom contract when canonical Set empty Record that empty canonical_symbols disables only the prelude shortcut; resolve_atom still rejects unknown Atoms via unbound_symbol_diagnostic. Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: Cursor <cursoragent@cursor.com>
Summary
compiler/01_tokenize.dagandcompiler/02_parse.dagover declarativeNode-shaped rule data (B2-OMNI), with realProducedpaths (not unconditionalwalk_not_realized).Nodewith connectiveConjand zero children denotes a void fragment (zero productions). The walkers match this shape structurally (NodeKind+count(children)==0), never by surface spelling or language-id branching.String(viaFreeMonoid<Char>spine length) ⇒Produced { TokenStream { tokens: [] } }. E0 + non-empty source ⇒ fail-closedRejected(tokenize_lex_e0_source_not_exhausted). Other rule shapes ⇒Rejectedwithtokenize_lexical_walk_not_realizeduntil additional encodings are ratified in the LanguageModel data.TokenStream⇒Produced { value: grammar }(degenerateParseTree/Nodeseam). G0 + non-empty tokens ⇒Rejected(parse_g0_tokens_remain). Non-G0 grammars with empty tokens (or non-empty streams where the walker has no production match yet) ⇒Rejectedwithparse_walk_not_realized.extdeps/languages/dag.dag: canonical E0/G0 voidNodebuilders (dag_wave1_e0_void_lex,dag_wave1_g0_void_grammar,dag_language_model_wave1_void) plusDagLanguageModelbundle; anchors remain repo-owned (docs/v3-spec.md+ v4 tree). DECISIONS.md L-5 + STRUCTURE.md closed-tree admission (operator Option A, relay merry-ibex-337).Test plan
src/v2/src/v3hand-Rust changes):target/release/v2-compiler compile --source-root src/v4 --output-dir <tmp> --target dagExpect 65 modules resolved, 0 diagnostics.
src/v4/changes.dag.dagand extend the walkers bymatchon those shapes only — still no language-1 hardcoding incompiler/*.