navicore/patch-prolog-v1

Archived

Fork 0

● just ci green, end-to-end smoke shows the App-held query streaming through ; correctly and reaching false. after #39

Merged

navicore merged 2 commits from repl-phase-2 into main

2026-06-04 12:46:16 +00:00

navicore commented

2026-06-04 12:25:17 +00:00

Owner

exhaustion.

What landed in this turn:

core/solver.rs — Solver<'a> → Solver owning Arc. The three &self.db.clauses[i];
self.rename_clause(clause) sites now clone the clause first (the borrow on *self.db through Arc deref ties to
&self, conflicting with the &mut self on rename_clause; cloning is bounded since rename already walks the
structure).
CLI — runner.rs, compiler.rs (and the generated-binary template inside it), and tests/integration.rs updated
mechanically: 21 Solver::new(&db, …) → Solver::new(Arc::new(db), …) sites with use std::sync::Arc; added where
needed.
REPL engine.rs — Session.db is now Arc. Query has no lifetime. Session::query uses
Arc::make_mut to mutate the interner during parse (strong count is 1 in practice — App drops prior Query before
submitting a new goal), then Arc::clone to hand a fresh handle to the new Solver.
REPL app.rs — App.active: Option added. New test active_query_can_be_held_on_app_state is the
load-bearing proof: pre-Arc this wouldn't compile.
REPL main.rs — stream_solutions now drives &mut App via app.active, dogfooding the storability win on the hot
path. No more local Query.

Tests: 49 → 50 (added the App-held query test). Workspace just ci clean.

exhaustion. What landed in this turn: - core/solver.rs — Solver<'a> → Solver owning Arc<CompiledDatabase>. The three &self.db.clauses[i]; self.rename_clause(clause) sites now clone the clause first (the borrow on *self.db through Arc deref ties to &self, conflicting with the &mut self on rename_clause; cloning is bounded since rename already walks the structure). - CLI — runner.rs, compiler.rs (and the generated-binary template inside it), and tests/integration.rs updated mechanically: 21 Solver::new(&db, …) → Solver::new(Arc::new(db), …) sites with use std::sync::Arc; added where needed. - REPL engine.rs — Session.db is now Arc<CompiledDatabase>. Query has no lifetime. Session::query uses Arc::make_mut to mutate the interner during parse (strong count is 1 in practice — App drops prior Query before submitting a new goal), then Arc::clone to hand a fresh handle to the new Solver. - REPL app.rs — App.active: Option<Query> added. New test active_query_can_be_held_on_app_state is the load-bearing proof: pre-Arc this wouldn't compile. - REPL main.rs — stream_solutions now drives &mut App via app.active, dogfooding the storability win on the hot path. No more local Query. Tests: 49 → 50 (added the App-held query test). Workspace just ci clean.

navicore added 1 commit

2026-06-04 12:25:17 +00:00

● just ci green, end-to-end smoke shows the App-held query streaming through ; correctly and reaching false. after

CI - Linux / CI - Linux x86_64 (pull_request) Successful in 55s

Details

b9e64bd73d

exhaustion.

  What landed in this turn:
  - core/solver.rs — Solver<'a> → Solver owning Arc<CompiledDatabase>. The three &self.db.clauses[i];
  self.rename_clause(clause) sites now clone the clause first (the borrow on *self.db through Arc deref ties to
  &self, conflicting with the &mut self on rename_clause; cloning is bounded since rename already walks the
  structure).
  - CLI — runner.rs, compiler.rs (and the generated-binary template inside it), and tests/integration.rs updated
  mechanically: 21 Solver::new(&db, …) → Solver::new(Arc::new(db), …) sites with use std::sync::Arc; added where
  needed.
  - REPL engine.rs — Session.db is now Arc<CompiledDatabase>. Query has no lifetime. Session::query uses
  Arc::make_mut to mutate the interner during parse (strong count is 1 in practice — App drops prior Query before
  submitting a new goal), then Arc::clone to hand a fresh handle to the new Solver.
  - REPL app.rs — App.active: Option<Query> added. New test active_query_can_be_held_on_app_state is the
  load-bearing proof: pre-Arc this wouldn't compile.
  - REPL main.rs — stream_solutions now drives &mut App via app.active, dogfooding the storability win on the hot
  path. No more local Query.

  Tests: 49 → 50 (added the App-held query test). Workspace just ci clean.

navicore commented

2026-06-04 12:36:34 +00:00

Author

Owner

Review

What it does: The Arc<CompiledDatabase> refactor — Solver<'a> → owned Solver, so Query loses its lifetime and can live on App.active. CLI call sites updated mechanically; main.rs now drives the query through App-held state on the real path. The new active_query_can_be_held_on_app_state test is indeed the load-bearing proof.

Verified locally (scratch copies of the branch): all suites pass (148 core + 248 integration + 6 runner + 12 repl), and the smoke run streams member/3 through ; to false. via App.active. The design is the right call — it dissolves the self-referential problem instead of papering over it, and Arc::make_mut in Session::query has correct semantics even in the worst case (if a query were still alive, the old Query keeps its db snapshot — exactly what you'd want).

🟡 One real finding: the clause clone is a measurable hot-path regression — and avoidable

The three let clause = self.db.clauses[clause_idx].clone() sites run on every clause-match attempt. The PR comment argues "rename already walks the structure, so the extra clone is bounded" — true that it's bounded, but it's a full extra deep copy (allocations included) per resolution step, roughly doubling term allocation during clause selection. Benchmarked with naive-reverse (nrev of a 60-list × 300 iterations), interleaved runs to control for machine noise:

version	time	vs main
main (borrow)	~1.52s	—
PR as-is (clause clone)	~1.65s	~9% slower
fixed (Arc-handle, below)	~1.53s	within noise

The fix is the standard owned-handle trick — clone the Arc (an atomic refcount bump), not the clause. The local handle's borrow is independent of &mut self:

// instead of:
let clause = self.db.clauses[clause_idx].clone();
let renamed = self.rename_clause(&clause);

// do:
let db = Arc::clone(&self.db);
let renamed = self.rename_clause(&db.clauses[clause_idx]);

Same three sites, two lines each. Applied to a scratch copy: compiles clean, all 148 core unit tests + 248 integration tests pass, and it recovers the full regression. Note this also affects prlg run, not just the REPL — core's hot path is shared.

🟢 Minor

Solver<'a> → Solver is a breaking change to core's public API — fine under the workspace's 0.x versioning (cargo treats 0.6 → 0.7 as incompatible), just noting it's not patch-level.
Stray blank line introduced after db, in the Solver::new initializer.
The Arc::make_mut comment's "strong count is 1 in practice" assumption depends on the TUI loop continuing to drop App.active before submitting a new goal. If that invariant ever breaks, behavior stays correct but each submit silently deep-clones the database. A debug_assert_eq!(Arc::strong_count(&self.db), 1) would make the assumption checkable rather than narrative.
stream_solutions re-matches app.active.as_mut() every loop iteration though it can't become None mid-loop — harmless, reads slightly oddly.
Nice to see the #38 items already landed on main (with_history_path seam, the README, the ProgramDirectives destructure).

Verdict

Right refactor, right shape, honestly tested — but take the Arc-handle version of the three solver sites before merging. It's strictly better: same borrow-checker escape, zero deep copies, verified green against the full suite, and it keeps core's interpreter at parity with main instead of ~9% behind.

Review by Claude Code

# Review **What it does:** The `Arc<CompiledDatabase>` refactor — `Solver<'a>` → owned `Solver`, so `Query` loses its lifetime and can live on `App.active`. CLI call sites updated mechanically; `main.rs` now drives the query through App-held state on the real path. The new `active_query_can_be_held_on_app_state` test is indeed the load-bearing proof. **Verified locally** (scratch copies of the branch): all suites pass (148 core + 248 integration + 6 runner + 12 repl), and the smoke run streams `member/3` through `;` to `false.` via `App.active`. The design is the right call — it dissolves the self-referential problem instead of papering over it, and `Arc::make_mut` in `Session::query` has correct semantics even in the worst case (if a query were still alive, the old `Query` keeps its db snapshot — exactly what you'd want). ## 🟡 One real finding: the clause clone is a measurable hot-path regression — and avoidable The three `let clause = self.db.clauses[clause_idx].clone()` sites run on **every clause-match attempt**. The PR comment argues "rename already walks the structure, so the extra clone is bounded" — true that it's bounded, but it's a full extra deep copy (allocations included) per resolution step, roughly doubling term allocation during clause selection. Benchmarked with naive-reverse (nrev of a 60-list × 300 iterations), interleaved runs to control for machine noise: | version | time | vs main | |---|---|---| | main (borrow) | ~1.52s | — | | **PR as-is (clause clone)** | **~1.65s** | **~9% slower** | | fixed (Arc-handle, below) | ~1.53s | within noise | The fix is the standard owned-handle trick — clone the `Arc` (an atomic refcount bump), not the clause. The local handle's borrow is independent of `&mut self`: ```rust // instead of: let clause = self.db.clauses[clause_idx].clone(); let renamed = self.rename_clause(&clause); // do: let db = Arc::clone(&self.db); let renamed = self.rename_clause(&db.clauses[clause_idx]); ``` Same three sites, two lines each. Applied to a scratch copy: compiles clean, **all 148 core unit tests + 248 integration tests pass**, and it recovers the full regression. Note this also affects `prlg run`, not just the REPL — core's hot path is shared. ## 🟢 Minor - `Solver<'a>` → `Solver` is a breaking change to core's public API — fine under the workspace's `0.x` versioning (cargo treats `0.6 → 0.7` as incompatible), just noting it's not patch-level. - Stray blank line introduced after `db,` in the `Solver::new` initializer. - The `Arc::make_mut` comment's "strong count is 1 in practice" assumption depends on the TUI loop continuing to drop `App.active` before submitting a new goal. If that invariant ever breaks, behavior stays correct but each submit silently deep-clones the database. A `debug_assert_eq!(Arc::strong_count(&self.db), 1)` would make the assumption checkable rather than narrative. - `stream_solutions` re-matches `app.active.as_mut()` every loop iteration though it can't become `None` mid-loop — harmless, reads slightly oddly. - Nice to see the #38 items already landed on main (`with_history_path` seam, the README, the `ProgramDirectives` destructure). ## Verdict Right refactor, right shape, honestly tested — but take the Arc-handle version of the three solver sites before merging. It's strictly better: same borrow-checker escape, zero deep copies, verified green against the full suite, and it keeps core's interpreter at parity with main instead of ~9% behind. --- *Review by Claude Code*

navicore added 1 commit

2026-06-04 12:41:55 +00:00

● All three landed; just ci green.

CI - Linux / CI - Linux x86_64 (pull_request) Successful in 1m50s

Details

d251254e7b

- 🟡 Three solver hot-path sites now use let db = Arc::clone(&self.db);
  self.rename_clause(&db.clauses[clause_idx]); — one refcount bump per resolution step instead of a full Clause
  deep copy. Same borrow-checker escape, no per-step allocation.
  - 🟢 Stray blank line after db, in the Solver::new initializer removed.
  - 🟢 Session::query now has debug_assert_eq!(Arc::strong_count(&self.db), 1, ...) before Arc::make_mut. If a
  future caller violates the drop-before-submit invariant, debug builds catch it; release path is unchanged.

navicore merged commit e66b9c43ac into main

2026-06-04 12:46:16 +00:00

navicore deleted branch repl-phase-2

2026-06-04 12:46:17 +00:00

navicore referenced this pull request from a commit

2026-06-04 12:46:18 +00:00

Merge pull request '● just ci green, end-to-end smoke shows the App-held query streaming through ; correctly and reaching false. after' (#39) from repl-phase-2 into main

navicore referenced this pull request from a commit

2026-06-04 13:46:28 +00:00

● All seven PR #40 items addressed; just ci green.

Commenting is not possible because the repository is archived.

No reviewers