Skip to content

feat(native): run pivot proofs, opt-out checks and semantic completion through the native session - #1067

Closed
kvlonge wants to merge 3 commits into
mainfrom
feat/native-project-session
Closed

kvlonge wants to merge 3 commits into
mainfrom
feat/native-project-session

Conversation

@kvlonge

@kvlonge kvlonge commented Oct 9, 2026 •

Copy link
Copy Markdown
Contributor

Why

M4i parts 2 and 3. Under native-preview, pivot proofs, opt-out syntax checks and semantic completion's model facts come from the finished native analysis session.

Changes

  • finish returns a FinishedSession (pivot tables, pool, model facts), passed as an argument, never stored on CompiledProject.
  • Part 2: pivot models outside analysis are proven in one batch (session tables, or one standalone call); opt-out checks use check_native_sql_syntax. Panicking proofs and unrejected opt-outs defer. Deleted as dead on every tier: the per-model proof binding, prove_dynamic_contract.rs, _prove_native_dynamic_contract.py, _helpers/dynamic_contract.py.
  • Part 3: type recovery and completion read output names and lineage from the session for models it analysed natively and successfully with no dynamic proof replacing names; others keep the payload. No Python became dead on every tier (lineage_payload still feeds the rest).
  • Expectation changes:
    • test_native_analysis_seams: analysis returns NativeModelAnalyses with a session.
    • StandalonePivotProofTestCase gains expected_session_proofs; new no-analysis case.
    • Batched proofs can record deferrals for pivots Python never reaches after an earlier raise.
    • Failure corpus gains semantic-recovered-uses-through-intermediate (321→322).
    • SemanticInputs gains native_session.
  • New tests: pivot/opt-out parity; session-fed completion parity vs payload and Python on both shared generated corpora, with exact deterministic counts (44/28 and 67/29 session/payload models, 11 proven); Rust facts test.

Verification

  • Sabotage (reverted), each fails tests: session proofs defer or refused; batch ignored; opt-out skipped; session lineage emptied; session names dropped; selection empty; proof exclusion removed.
  • CI-flag differential 322 identical vs native-preview; shipped differential 308.
  • Touched tests, compile/differential E2E, cargo test/clippy/fmt, make check-ci, hygiene.

Base automatically changed from feat/native-project-integration to main October 9, 2026 15:43
…rough the native session

The finished analysis session is kept on CompiledProject.native_session and proves pivot models outside it from its own tables; without a session one batched standalone call sends the tables once. The per-model native proof path is deleted. SQL-analysis opt-out syntax checks use the native checker under the preview engine. Rule hosts drop the session before pickling.
@kvlonge
kvlonge force-pushed the feat/native-project-session branch from 95d26f8 to c51b7c4 Compare October 9, 2026 16:06
@kvlonge
kvlonge enabled auto-merge October 9, 2026 16:06
…sion

Type recovery and completion read each analysed model's output names and lineage from the
finished native session instead of payload rows rebuilt from CompiledProject. Models whose
analysis Python answered, failed, or whose names a dynamic pivot proof replaced keep the payload.
@kvlonge kvlonge changed the title feat(native): batch dynamic pivot proofs and opt-out syntax checks through the native session feat(native): run pivot proofs, opt-out checks and semantic completion through the native session Oct 9, 2026
@kvlonge
kvlonge disabled auto-merge October 9, 2026 16:46
@kvlonge
kvlonge enabled auto-merge October 9, 2026 16:56
@kvlonge
kvlonge added this pull request to the merge queue Oct 9, 2026
@kvlonge
kvlonge removed this pull request from the merge queue due to a manual request Oct 9, 2026
@kvlonge
kvlonge added this pull request to the merge queue Oct 9, 2026
@kvlonge

kvlonge commented Oct 9, 2026

Copy link
Copy Markdown
Contributor Author

Landed together in #1075 to cut merge-queue CI runs; review history stays here.

@kvlonge kvlonge closed this Oct 9, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to a manual request Oct 9, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant