Repository navigation
D - #544
D#544
Conversation
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 87e7404124
ℹ️ 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".
| ResolvedByStructure(DeclarationId), | ||
| /// A resolved identifier reached by name-keyed fallback. | ||
| /// Produced by `resolve_pending_identifiers` when an | ||
| /// unresolved stub is repaired via `declaration_by_name`. | ||
| ResolvedByName(DeclarationId), |
There was a problem hiding this comment.
Keep
ResolvedIdentifier compatibility until callers migrate
Renaming AtomPayload::ResolvedIdentifier to ResolvedByStructure/ResolvedByName here breaks the build immediately because the rest of the compiler still constructs and matches ResolvedIdentifier (for example lower.rs:538 and infer.rs:168 in this same commit), so cargo check -p v3-compiler fails with dozens of E0599 errors. This change needs to be landed with call-site migrations (or a temporary compatibility variant) in the same commit to keep the branch buildable.
Useful? React with 👍 / 👎.
|
What changed
Four call sites updated:
Substrate audit (Q4 coproduct dissolution)Per the substrate-principle-audit memo, Q4 splits a compressed variant when N distinct causes need downstream distinction:
Q4 mechanically landed right, but E-6 (no substrate change without a same-PR consumer) is violated: the split lands without anything that actually CARES about the distinction. The The likely motivating consumer (not in this PR)α (#533) §8 Spec reading protocol says "The walker MUST NOT call If that's the motivating use case, it's a fine Q4 split — but the first consumer needs to land either in this PR or as a tightly-scheduled follow-up:
Additional concerns
Merge pathEither (Option A) add a first consumer in this PR OR (Option B) name the dissolution trigger explicitly with a follow-up ROADMAP entry. Without one of those, this is a preemptive split that adds coproduct surface with no enforcement. The underlying substrate decision is right — emission-visible provenance is the kind of thing α §8 wants to lock structurally. Just needs to close the loop between substrate and consumer before landing. |
|
ChatGPT review in progress... (view conversation) Check back in ~30 minutes for the full review. |
Cold-init path for the cost.dag OnceLock cache key takes ~2.5s on CI cold runners vs the default 2s budget. Cache hits are fast (~1s locally) but the first compile legitimately bears the one-time cost. Matches the sibling cost_generated_module_matches_checked_in_snapshot's custom 15s budget for the same kind of one-time-expensive work. Unblocks downstream PRs that inherit the failure on rebase (#542, #543, #544, #545). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Main now has commit The |
This comment has been minimized.
This comment has been minimized.
briansrls
left a comment
There was a problem hiding this comment.
codex · gpt-5.4 · 68bd42db
✅ Review (blocking: 0, non-blocking: 0+/0-)
ROADMAP — Verified
- DB-17 reference-resolution provenance:
ResolvedByNameis now reflected insubstrate.dag, exposed throughlens_structural_resolution, and covered by consumer/test updates, so the scheduled-deletion row matches the shipped surface.
✅ No blocking issues; the provenance split is modeled as a first-class substrate fact and the touched lowering, inference, emitter, reflection, and test paths all carry it forward consistently.
This comment has been minimized.
This comment has been minimized.
|
E-6 concern from my prior review fully addressed. The first consumer landed structurally: New consumer:
|
|
claude-review — LGTM modulo two clarification asks. What's right
Asks before merge
Sequencing risk |
|
Principle audit. Fail-closed. This looks good. The changed lowering path still fails through the existing diagnostic sweep rather than introducing a silent success path: unresolved identifier stubs are rewritten to a resolved form inside Illegal states unrepresentable. Also improved. The diff takes a fact that used to be collapsed into one “resolved identifier” shape and makes the distinction explicit in the substrate with Facts flow forward. Good. The new fact is not introduced and then dropped; it survives lower → reflected substrate → lens consumer. Coproduct dissolution. This is my one blocking concern. I buy Single-authority metadata. Mostly satisfied. There is now one substrate-carried place to read this provenance, and the new lens is a pure derived reader rather than a parallel store. The only place I still see authority split is the classification/enforcement story above: code comment, lens comment, and roadmap row currently describe API-level enforcement. This is the same concern from a different angle. The real invariant is not just “we can list Design question. Is Path to convergence. Before merge, make the status of As tracked follow-up debt, I would keep the stronger user-only structural consumer for the reflected boundary, and add one end-to-end test where a real compiled user module produces a LOOP HEALTH: converging — this round turns hidden name-fallback repair into first-class substrate data and immediately gives it a real consumer, but it should bank that progress with one honest scaffold/enforcement story before merge. Verdict. REQUEST_CHANGES The main code movement looks right, and I do not see broader issues in the infer/emit/test plumbing. I would merge this after |
|
The bot's ChatGPT session has expired. Reviews are paused until re-login. To fix:
The bot will resume automatically on its next cycle. |
briansrls
left a comment
There was a problem hiding this comment.
codex · gpt-5.4 · 6d2a4ea0
✅ Review (blocking: 0, non-blocking: 1+/0-)
Non-blocking — Strengths
src/v3/compiler/src/lower.rsThe provenance split stays structural and fail-closed: direct wiring sites emit ResolvedByStructure, sweep repairs emit ResolvedByName, and unresolved survivors still diagnose.
✅ I did not find a new blocking concern in the touched lines after the DB-17 provenance split.
|
✅ Review (blocking: 0, non-blocking: 1+/0-) Non-blocking — Strengths
✅ I did not find a new blocking concern in the touched lines after the DB-17 provenance split. |
|
Meta-review in progress... (view conversation) Loop-health check: is this review cycle making forward progress, or shifting debt? Posts in ~5-15 minutes. |
Meta-Review (Loop Health)Generated by gpt-5-4-pro According to a document from 2026-04-19, this loop is making real progress, but the review loop on this PR has already hit diminishing returns. Merge the PR and carry the explicitly tracked debt. Loop summary. 5 recorded review events over about 70 minutes, from 00:30:36Z to 01:40:39Z on 2026-04-19. Of those, 2 are substantive codex reviews and 3 are browser-side events. But only 1 browser event contains any substance, and that one is generic modeling-discipline boilerplate rather than a PR-specific review; the other browser event is just “review in progress,” and the last is a session-expiry failure. Commit count is not recoverable from the supplied artifacts, so I will not invent one. Forward progress evidence. This PR is not substrate growth without a consumer. The recorded review says the DB-17 provenance split made The debt is also accounted for instead of hidden. ROADMAP says deferrals must live in one place, and the scheduled-deletions table gives More importantly, this repo has already shown the right meta-behavior once before: the PR #445 meta-review turned a recurring authority leak into the invariant “Semantic authority after lowering,” explicitly because repeated local fixes were not enough. This PR is in that same direction: it promotes “resolved structurally vs resolved by name fallback” into a substrate fact that future lenses and ratchets can enforce. That is principle 3, not whack-a-mole. Debt accumulation evidence. DB-17 does not close the whole class. ROADMAP explicitly says compiler-internal There is also still scaffold load around The loop quality itself is also weak on reviewer diversity. The browser reviewer added almost no PR-specific signal and then died. The only real loop signal here is the two codex passes, both of which converge on “no blocker; provenance split is structural.” That means another round on this PR is more likely to produce ceremony than value. Cheating signal. Low cheating from the implementer. The compromises are documented, named, and scheduled. ROADMAP’s rule is that every scaffold gets a row with trigger and enforcement path, and this PR follows that pattern. That is “cheating with accounting,” which is acceptable. The most recent fixes are structural, not “good enough for now.” The review record describes the change as a provenance split carried through lowering, inference, emitter, reflection, and tests, not a cheap local patch. The bluff is elsewhere: pretending another review lap on this PR will materially improve loop health. I do not buy that. Path to convergence. Merge this PR now. The acceptable debt to carry is small and already named:
The follow-up artifact should be the existing ROADMAP machinery, not more review churn on this PR. If one thing is missing, it is only this: add or tighten the explicit follow-up row for turning the new Meta-verdict ⚖️ SHIP_WITH_DEBT This loop is not shifting debt blindly. It banked a real structural gain: one recurring leak class is now an explicit fact with a consumer and a scheduled dissolution path. But the review loop around it has already converged. Merge it, and spend the next cycle on the named follow-ups, not on another “still looks structural” lap. |
6d2a4ea to
d57d7b8
Compare
|
ChatGPT review in progress... (view conversation) Check back in ~30 minutes for the full review. |
ChatGPT ReviewGenerated by gpt-5-4-pro Principle audit. Fail-closed. Looks good. The strict sweep still routes unresolved survivors through diagnostics, and the new lowering regression test pins that repaired stubs become a resolved form rather than silently disappearing. This remains a boundary gate more than a type-level proof, but the diff does not weaken it. Illegal states unrepresentable. Good improvement. Splitting the old resolved-identifier shape into Facts flow forward. Satisfied. The new provenance fact is produced in lowering, survives through infer/emit by explicit two-variant handling, and now has a real downstream reader in Coproduct dissolution. The code shape is better, and the new lens means Single-authority metadata. Mostly satisfied. There is now one substrate-carried provenance fact, and infer/emit/lens are all readers of that same fact rather than parallel encodings. The only authority split I still see is the classification story above: the variant’s status is not yet described in one place the same way. API-level enforcement. Mostly satisfied. The distinction between structural resolution and name-fallback resolution is enforced by the type shape itself. The remaining non-structural piece is the user/bootstrap boundary: Design question. Is Path to convergence. Before merge, I do not see a structural code change that must land. The one cleanup I would strongly want soon is to sync the local Tracked follow-up debt can stay explicit: reflect the user/bootstrap boundary as a first-class substrate fact so LOOP HEALTH: converging — this round turns previously hidden name-fallback repair into first-class substrate data and immediately gives it a lens plus regression pins; the remaining gap is receipt/enforcement polish, not another hidden bridge. Verdict. APPROVE_WITH_COMMENTS The provenance split itself looks clean, and I do not see a new blocking concern in the mechanics. My only comment is to tighten the classification story around |
briansrls
left a comment
There was a problem hiding this comment.
codex · gpt-5.4 · d57d7b82
BLOCKING (1)
Root Cause
src/v3/compiler/src/dag.rsThe substrate split preserves resolution provenance, but this helper restores the pre-split convenience API on the substrate type -> remove the helper and keep any provenance-erasing collapse local to the specific implementation site that can justify dropping it.
Non-blocking — Strengths
src/v3/lenses/structural_resolution.dagThe new NameKeyedReference lens keeps the scheduled-deletion signal as a pure substrate read instead of another side table.
| TypeParam(String), | ||
| } | ||
|
|
||
| impl AtomPayload { |
There was a problem hiding this comment.
BLOCKING: AtomPayload::resolved_id() collapses ResolvedByStructure and ResolvedByName back into the old merged view, reintroducing a bridge that weakens API-level enforcement of the new provenance fact (principles 3 and 6; INVARIANTS no bridges).
|
BLOCKING (1) Root Cause
Non-blocking — Strengths
|
Opened from session-dashboard for session
zesty-carp-794.