Repository navigation
Conversation
This comment has been minimized.
This comment has been minimized.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 29888d7498
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| variant.label | ||
| ))); | ||
| }; | ||
| let mut lines = vec!["@dataclass".to_string(), format!("class {}({enum_name}):", variant.label)]; |
There was a problem hiding this comment.
Qualify emitted variant class names by parent type
render_enum_variant defines each sum variant as a top-level Python class named only by variant.label (for example class Some(...)), and the rest of the emitter dispatches on those bare names. Lowering explicitly keeps variant labels out of the global declaration namespace (src/v3/compiler/src/lower.rs 651-655), so different sum types can legally reuse the same label; in emitted Python, the later class definition overwrites the earlier one, causing constructors and isinstance matches for the first type to resolve to the wrong class. Mangle or qualify variant class names with their parent type to preserve type identity.
Useful? React with 👍 / 👎.
| lines.push(format!( | ||
| " {}: {}", | ||
| child.label, | ||
| self.python_type_name_for_decl(child.ty)? |
There was a problem hiding this comment.
Defer evaluation of emitted dataclass annotations
Type fields are emitted as eager annotations (" name: Type"), but Python 3.10 evaluates those expressions while the class body executes. The compiler allows references to declarations resolved from the global symbol table (src/v3/compiler/src/lower.rs 704-709), so forward or mutually-recursive user types can be valid DAGs; the generated module will fail at import time with NameError when an annotation refers to a type defined later. Add from __future__ import annotations (or quote annotation types) before emitting classes.
Useful? React with 👍 / 👎.
briansrls
left a comment
There was a problem hiding this comment.
Director Review — Python target (#484)
This is the cleanest validation of "one spec-file edit per target." Python lands in 2135 insertions:
python.dag(346 lines) — the specemit_python.rs(1356 lines) — table-driven emitter that reads the spec- Cross-target equivalence test (432 lines)
- Zero core compiler changes
For comparison, Go (#483) needed +47 lines in dag.rs and +167 lines refactoring emit_rust.rs. Python needed nothing — it landed entirely additively. That difference is itself a validation: Go required architectural extraction (the TargetExecutionModel infrastructure), Python now benefits from that extraction without any further core changes.
What's good
python_target.memory == GarbageCollectedcorrectly enforced — emitter errors out if the target says anything else- Type realizations are spec-declared, not relying on Python's dynamic typing (
python_int → "int",python_string → "str") - Cross-target equivalence test compares Rust + Python output on the same DAG
- No layer-opacity violations — no hardcoded "python" or "Python" in dispatch logic, only
python_*prefix filtering at index time
One observation (not blocking)
emit_python.rs is 1356 lines. emit_go.rs is 2123 lines. emit_rust.rs is 4000+ lines. There's a real question whether the emitters could share a generic walker — the parts that differ are syntax templates (declared in the spec) and language-specific edge cases. A shared walker reading per-target syntax bundles would dramatically reduce per-target boilerplate. Worth thinking about as the third target lands and patterns emerge.
But that's optimization. For now, this PR delivers what the thesis promised: one spec file, no core changes, equivalence-tested.
LGTM. Ship.
ChatGPT ReviewAccording to documents from 2026-04-16, this loop has crossed from useful iteration into debt-shifting. The diff got better, but the review process is still rediscovering the same class of structural problem instead of graduating it into a rule. 🔁 PAUSE_AND_REGROUP. Loop summary. From the attached history, I can confirm 3 completed review rounds over about 59 minutes: browser at 20:13Z, codex-cli at 20:37Z, browser again at 20:48Z, plus 1 later browser run that had started but was not yet complete by 21:12Z. That gives K = 1 codex review and L = 2 completed browser reviews (with one extra in-progress browser run visible). The exact commit count is not recoverable from the attached artifacts; what the history supports is at least 3 reviewed revisions/states. Forward progress evidence. Real progress happened. The PR genuinely decompressed three flat verification sub-scaffolds into richer carriers: the old diagnostic expectation, port-state split, and cost-threshold split were replaced by more structural shapes, and the consumer side moved with them in the generator, harness, and bootstrap witness tests. Codex also explicitly credited the new fixture-driven predicate checks for exercising compile-boundary behavior instead of only reflected shape. That is real local progress. But it is only a stronger existing L1.5 consumer; it does not unlock a new independent consumer such as L4 semantic verification. The roadmap says Track 12 is only “partially unblocked” and that L4 can start, while the thesis still says L4 semantic correctness is not implemented and remains the critical gap. So the loop improved the substrate locally without creating a new external correctness anchor. Debt accumulation evidence. The loop is still accumulating debt in exactly the way your seven principles warn about. First, the remaining Cheating signal. Mild but real. The implementer is not fully hiding compromises—the scaffold is still labeled as a scaffold, so the debt is at least partially visible. But the most recent fixes are classic finite-budget, low-blast-radius compromises rather than structural closure: an empty-string sentinel instead of a typed “kind-only vs kind+detail” split, a coarse Meta-verdict — 🔁 PAUSE_AND_REGROUP Do not spend the next round fixing one more local instance. The next valuable move is to graduate the class, not patch the symptom: Restore the named dissolution trigger for the remaining |
briansrls
left a comment
There was a problem hiding this comment.
codex · gpt-5.4 · 2d908e5e
BLOCKING (2)
Root Cause
src/v3/spec/python.dagThe PR adds PythonPatternRealization and PythonPatternStrategy but no data authority for List or option lowering, so emit_python falls back to name-based reconstruction; add the pattern realization data and have the emitter index and consume it like emit_rust does.src/v3/compiler/src/emit_python.rsThe Python port copied only the canonical OrderedRing fallback and omitted the operand-type algebra walk already used by inference and emit_rust; reuse that walk here or carry the resolved algebra field id downstream.
Non-blocking — Strengths
src/v3/compiler/tests/m1_4_emit_python_test.rsThe new roundtrip test executes emitted Python and Rust against the same reflected fixtures, which is the right thesis-facing check instead of stopping at string snapshots.src/v3/spec/python.dagUsing DeclarationRef for target and op keeps the Python realization tables keyed by typed identities rather than names, which is the right substrate direction.
| return Ok(None); | ||
| }; | ||
| let empty_variant = variants.iter().find(|v| v.label == "Empty").map(|v| v.ty); | ||
| let cons_variant = variants.iter().find(|v| v.label == "Cons").map(|v| v.ty); |
There was a problem hiding this comment.
BLOCKING: List and optional matches are still reconstructed from hardcoded Empty/Cons/None names plus a baked head/tail payload shape, so match semantics do not flow forward from a single Python target authority (INVARIANTS: facts flow forward; emission is translation, not decision-making).
| let ordered_ring = dag.declaration_by_name("OrderedRing").ok_or_else(|| { | ||
| EmitPythonError::Unsupported( | ||
| "bootstrap is missing canonical OrderedRing declaration".to_string(), | ||
| ) |
There was a problem hiding this comment.
BLOCKING: algebra_field_for_operator throws away operand_type_id and always resolves through OrderedRing, so Python operator emission is no longer keyed by the operand's resolved algebra authority (INVARIANTS: semantic authority after lowering; layer opacity).
|
BLOCKING (2) Root Cause
Non-blocking — Strengths
|
ChatGPT ReviewPrinciple audit. Fail-closed. Mostly good: the new emitter usually returns Illegal states unrepresentable. Satisfied. I do not see a new substrate Rust shape here that uses Facts flow forward. The good part is real: target identity now flows structurally, since Coproduct dissolution. Satisfied for this diff. The new Rust enums ( Single authority. Mostly satisfied. Using API-level enforcement. Mostly satisfied on the new helper APIs, but the Loop path is again the miss: nothing in the API prevents an unsupported L1 behavior from being rendered as an ordinary expression ( Design question. Is this PR landing a real Shape-A Python emitter for the v3 computation substrate, or a deliberately narrow subset for the current lens/use-case? The code and tests already present it as a general target emitter, so the answer matters: if it is general, Verdict. REQUEST_CHANGES. This is real progress — especially the LOOP HEALTH: converging — this round unblocks a real consumer and a real cross-target execution check, but it still leaves one core behavior unmodeled, so the loop is improving rather than just moving debt around. |
Meta-Review (Loop Health)Loop summary. From the attached artifacts, I can confirm 3 visible review events tied to PR #484: one completed browser review at 2026-04-16 20:37Z, one completed codex review at 21:28Z, and one browser review still in progress at 21:45Z. The same history file also contains a separate meta-review block about Forward progress evidence. This loop has accomplished one thing that matters: it enabled a real new consumer. Both the browser review and the codex review independently call out the new Rust-vs-Python roundtrip execution test as the right kind of check, not a snapshot-only test. That matters because the roadmap and thesis both say the real open gap is L4/L5 verification — emitted code executing correctly and cross-language equivalence — and those are only partially unblocked today. Adding a Python emitter plus a cross-target behavioral test is forward motion toward that consumer-facing anchor, not substrate growth for its own sake. The review set is also narrowing. The first browser pass was still flagging three structural classes at once: named-instantiation naming, variant identity loss, and unused pattern authority. The later codex pass is concentrated on the remaining structural misses: pattern authority and operator/algebra resolution. That is convergence, not churn. Debt accumulation evidence. The loop is also adding debt. The clearest case is The codex review then finds the same disease again in operator lowering: the Python emitter copied a canonical Named instantiation/alias handling is the same pattern a third time: the browser review says the emitter preserves authored names for named declarations, but only materializes So Principle 3 is not happening yet. The modeling discipline says facts must flow forward, metadata must have one authority, and substrate-level issues are blocking once they start propagating. The invariants say new semantic boundaries must land end-to-end, and emission must be translation rather than decision-making. This loop is still catching the class by review, not by a new invariant or lens. Cheating signal. Moderate, not fatal. The implementer is not hiding everything: the first browser review says the emitter usually fails closed through Meta-verdict — 📈 KEEP_ITERATING This loop is still making positive marginal progress. It has already enabled a real new consumer — Python emission with cross-target execution testing — and the remaining issues are a short list of structural fixes, not evidence that the substrate itself is wrong. It is not ready to ship; the unresolved issues are still blocking by the project’s own standards. But this is also not a debt-shifting dead loop yet. One more round is likely to add value, because the next move is obvious: wire |
briansrls
left a comment
There was a problem hiding this comment.
codex · gpt-5.4 · d1dff2ca
BLOCKING (2)
Root Cause
src/v3/spec/python.dagTargetExecutionModelmodels multiple execution semantics, but the emitter only implements one and fail-closes on only half the product -> either collapse the model to the supported Python facts or make the emitter reject every unsupported field, includingscope.src/v3/spec/python.dagThe Python target spec introduced new sum types before recording whether each is terminal, scaffold, or dissolvable-now structure -> add per-type receipts or dissolve the compressed choices into structural target facts before more consumers depend on them.
Non-blocking — Strengths
src/v3/compiler/tests/m1_4_emit_python_test.rsThevariant_collisioncase is a useful nominal-identity regression because it proves same-labeled variants from different sums stay distinct in the emitted Python runtime.
Non-blocking — Improvements (fix in-PR if easy, else defer to roadmap)
src/v3/compiler/tests/m1_4_emit_python_test.rsThe suite never exercises the publicemit_pythonprogram mode with top-level value binds, so that entry point can drift independently of the tested module path; roadmap lane M1(4) Multi-target emission.
ROADMAP — Verified
- M1(4) Multi-target emission: The PR does establish the parallel Python spec plus emitter plus executable parity-test path that this deferred lane called for.
ROADMAP — Incomplete
- M1(4) Multi-target emission: The lane is not done yet because the new target model is not fully authoritative downstream:
scopeis declared but not enforced, and the new coproducts still lack dissolution receipts.
|
|
||
| fn emit_python_with_mode(dag: &Dag, mode: EmitPythonMode) -> Result<String, EmitPythonError> { | ||
| let indexes = PythonIndexes::build(dag)?; | ||
| if indexes.target.memory != "GarbageCollected" { |
There was a problem hiding this comment.
BLOCKING: python_target.scope is introduced as target authority, but emit_python_with_mode validates only memory and reduces scope to a comment, so the execution-model fact does not flow from spec to emitter (modeling-discipline section 3, facts flow forward).
| target: DeclarationRef | ||
| strategy: PythonCallableStrategy | ||
| cost: Int | ||
| } |
There was a problem hiding this comment.
BLOCKING: This file adds new coproducts (PythonCallableStrategy, PythonPatternStrategy, MemoryModel, ScopeModel) without the required 🟢/🟡/🔴 dissolution receipts, so the target model lands unfinished per modeling-discipline section 4.
|
BLOCKING (2) Root Cause
Non-blocking — Strengths
Non-blocking — Improvements (fix in-PR if easy, else defer to roadmap)
ROADMAP — Verified
ROADMAP — Incomplete
|
|
Closing in favor of a unified reconciliation approach. The merge-train experiment on Rather than push each branch through another round of rebase-fix-review that would repeatedly rediscover cross-branch conflicts, all six PRs (#482, #483, #484, #485, #486, #487) are being reconciled into a single
All review comments (codex, chatgpt-browser, director) harvested into Class of fixes addressed uniformly in reconciliation:
Thanks for the work — all of it ships through the reconciliation. |
Summary
emit_pythonpath for thev3compilerlens_unused_parameterssurface with executable Python emission and ownership-skip tracing for the GC targetTesting
cargo test -p v3-compiler --test m1_4_emit_python_test -- --nocapturecargo test -p v3-compiler --no-run