⏺ ;-paging is in — clippy -D warnings, 16 tests (4 new), fmt, and full workspace #13

Merged

navicore merged 2 commits from paging into main 2026-06-17 00:39:16 +00:00

Conversation 1 Commits 2 Files changed 3 +378 -61

navicore commented 2026-06-17 00:15:46 +00:00

Owner

Copy link

all green.

How it works, given stateless binaries:

• A query fetches a batch (PAGE_BATCH = 25) and reveals one solution at a time.
  The transcript reads like SWI:
  plg> ?- p(X, Y).
  X = tom, Y = bob ;
  X = bob, Y = ann ;
  X = ann, Y = sue .
• Trailing ; means more may follow; . marks the last (paging auto-ends).
• Keys while paging: ; or space → next solution; any other key stops; Ctrl-C/D
  still quits. The input line is replaced by a dim ; next · any other key stop
  hint, and the editor cursor/mode indicator are suppressed (you're not editing).
• Running past the batch: if you page to the end and the engine wasn't
  exhausted, it re-fetches with double the limit (the stateless-binary re-fetch
  the design called for) and continues seamlessly. Batch is small so we don't
  over-compute when you only want the first answer.

The trickier part was the wire format. Text renders terms canonically (point(1,
2), [a, b, c]) but doesn't delimit solutions; JSON delimits + has exhausted
but renders compounds as ugly nested objects. So fetch() takes only
count/exhausted (and error detection) from JSON and the rendered lines from
text, then splits the lines into count equal groups — every solution emits the
same number of Var = Value lines (anonymous vars aren't reported; an
all-anonymous solution is true.). This reuses the engine's term writer instead
of reimplementing it — the alternative (a JSON→Prolog renderer) would've been
shadow logic. Two execs per fetch is the honest cost; I noted it in run.rs.

The pure pieces are unit-tested (multi-var/single-var/all-anonymous splitting,
count/error parsing). The interactive ; loop is inherently TUI, so give it a
hands-on spin: define a few facts, query with multiple solutions, press ; to
walk them and a non-; key to stop early — and try a 30+ solution query to see
the re-fetch kick in past 25.

That clears the last parked item. The REPL now has the full Prolog-native query
loop.

all green. How it works, given stateless binaries: - A query fetches a batch (PAGE_BATCH = 25) and reveals one solution at a time. The transcript reads like SWI: plg> ?- p(X, Y). X = tom, Y = bob ; X = bob, Y = ann ; X = ann, Y = sue . - Trailing ; means more may follow; . marks the last (paging auto-ends). - Keys while paging: ; or space → next solution; any other key stops; Ctrl-C/D still quits. The input line is replaced by a dim ; next · any other key stop hint, and the editor cursor/mode indicator are suppressed (you're not editing). - Running past the batch: if you page to the end and the engine wasn't exhausted, it re-fetches with double the limit (the stateless-binary re-fetch the design called for) and continues seamlessly. Batch is small so we don't over-compute when you only want the first answer. The trickier part was the wire format. Text renders terms canonically (point(1, 2), [a, b, c]) but doesn't delimit solutions; JSON delimits + has exhausted but renders compounds as ugly nested objects. So fetch() takes only count/exhausted (and error detection) from JSON and the rendered lines from text, then splits the lines into count equal groups — every solution emits the same number of Var = Value lines (anonymous vars aren't reported; an all-anonymous solution is true.). This reuses the engine's term writer instead of reimplementing it — the alternative (a JSON→Prolog renderer) would've been shadow logic. Two execs per fetch is the honest cost; I noted it in run.rs. The pure pieces are unit-tested (multi-var/single-var/all-anonymous splitting, count/error parsing). The interactive ; loop is inherently TUI, so give it a hands-on spin: define a few facts, query with multiple solutions, press ; to walk them and a non-; key to stop early — and try a 30+ solution query to see the re-fetch kick in past 25. That clears the last parked item. The REPL now has the full Prolog-native query loop.

navicore added 1 commit 2026-06-17 00:15:46 +00:00

⏺ ;-paging is in — clippy -D warnings, 16 tests (4 new), fmt, and full workspace ... 3472ac2834

all green.

  How it works, given stateless binaries:
  - A query fetches a batch (PAGE_BATCH = 25) and reveals one solution at a time.
  The transcript reads like SWI:
  plg> ?- p(X, Y).
    X = tom, Y = bob ;
    X = bob, Y = ann ;
    X = ann, Y = sue .
  - Trailing  ; means more may follow;  . marks the last (paging auto-ends).
  - Keys while paging: ; or space → next solution; any other key stops; Ctrl-C/D
  still quits. The input line is replaced by a dim ;  next · any other key  stop
  hint, and the editor cursor/mode indicator are suppressed (you're not editing).
  - Running past the batch: if you page to the end and the engine wasn't
  exhausted, it re-fetches with double the limit (the stateless-binary re-fetch
  the design called for) and continues seamlessly. Batch is small so we don't
  over-compute when you only want the first answer.

  The trickier part was the wire format. Text renders terms canonically (point(1,
  2), [a, b, c]) but doesn't delimit solutions; JSON delimits + has exhausted
  but renders compounds as ugly nested objects. So fetch() takes only
  count/exhausted (and error detection) from JSON and the rendered lines from
  text, then splits the lines into count equal groups — every solution emits the
  same number of Var = Value lines (anonymous vars aren't reported; an
  all-anonymous solution is true.). This reuses the engine's term writer instead
  of reimplementing it — the alternative (a JSON→Prolog renderer) would've been
  shadow logic. Two execs per fetch is the honest cost; I noted it in run.rs.

  The pure pieces are unit-tested (multi-var/single-var/all-anonymous splitting,
  count/error parsing). The interactive ; loop is inherently TUI, so give it a
  hands-on spin: define a few facts, query with multiple solutions, press ; to
  walk them and a non-; key to stop early — and try a 30+ solution query to see
  the re-fetch kick in past 25.

  That clears the last parked item. The REPL now has the full Prolog-native query
  loop.

navicore commented 2026-06-17 00:20:38 +00:00

Author

Owner

Copy link

Review — ;-paging for query solutions

The overall shape is right. The split between run::fetch (returns a Fetch enum — pure I/O outcome), app::Paging (state machine across ; presses), and ui (suppress editor cursor + render hint) is clean. Refetch-with-doubled-limit is the documented design for stateless binaries, and reusing the engine's text writer instead of re-rendering JSON terms is the right call — point you made in the PR description and I agree.

Issues below, ordered by impact.

Real concerns

1. Refetch is O(n²) total work for long enumerations. Each refetch re-executes the binary with a doubled limit and re-renders every prior solution. A 1000-solution query enumerated to completion runs fetches at 25 → 50 → 100 → 200 → 400 → 800 → 1600. Each fetch is two execs and a full text render — total ~3175 solution-renders for 1000 solutions, plus 14 process spawns. Interactive use is fine (a few ; and done); a user who actually pages through everything pays this cost. Mitigations:

• Track the high-water mark of seen solutions; only render+display the tail past pos.
• Cap doubling at some ceiling (e.g. 1024).
• Or just document the cost — the comment in run.rs:9 calls out "two execs per fetch" but not the cumulative re-render.

2. json_count is called twice on the same payload. run.rs:81-86:

match json_count(&json) {
    Some(0) | None => return Fetch::NoSolutions,
    _ => {}
}
let count = json_count(&json).unwrap_or(0);

Should be one match that binds count:

let count = match json_count(&json) {
    Some(0) | None => return Fetch::NoSolutions,
    Some(n) => n,
};

Cosmetic, but reads as a forgotten cleanup.

3. JSON scraping is fragile to wire-format changes. json.find("\"count\":") matches anywhere the substring appears — today the engine only emits one count key, but if it ever grows a line_count/subgoal_count/etc., this picks the wrong one silently. Same for json.contains("\"exhausted\":true"). Two options:

• Anchor with a leading delimiter: find(",\"count\":") / find("{\"count\":"). Cheap; pins the position.
• Or use serde_json for the small JSON header — one more dep but kills the class.

The two-exec design also quietly assumes the engine produces identical solutions in both passes (count from JSON, lines from text). Pure Prolog: yes. Anything with side effects (time/1, random, assertz): could drift. Worth one line in the module doc that this depends on inter-run determinism.

4. split_solutions non-uniform fallback can silently misreport count. run.rs:115-117: if lines.len() % count != 0, it falls back to lines.into_iter().map(str::to_string).collect() — returning lines.len() strings as solutions even when count (the authoritative JSON value) said something else. The user pages through what looks like lines.len() solutions with no signal that something is off. Three lines (a self.log(" warn: malformed engine output") from app, or returning Fetch::Failed(...) from fetch) would surface it.

Small observations

5. No test for the refetch path. This is the only stateful piece of paging (limit doubling, pos carries over, new batch overwrites). The pure pieces are tested, but the most likely-to-break thing isn't — page_next's borrow gymnastics around need_more + refetch are exactly where a refactor would silently regress. A test would need run::fetch to be injectable (trait or fn pointer); not in scope here, but flagging the gap.

6. Doubling is unbounded. limit.saturating_mul(2) keeps growing as the user pages. With a divergent goal and a long PLG_REPL_TIMEOUT, you can find yourself waiting longer and longer per refetch with no cap. Modest defensive ceiling (e.g. 4096) would bound the worst case without affecting realistic use.

7. Paging assumes the engine produces solutions in a limit-independent order. The refetch relies on solutions[pos] in the new (bigger) batch being the same as the unrevealed tail of the old. Standard left-to-right SLD resolution gives that, but it's worth a one-liner in the Paging doc — it's the invariant that keeps pos carrying across refetches.

8. UI hint text uses literal spaces for spacing. ui.rs:21 — " ; next solution · any other key stop". Hand-tuned centering shifts oddly at narrow widths (and dimming applies to the leading spaces too, which is invisible but ratatui still walks them). Layout-aware (Rect-split and right-justify the hint) would be sturdier; pedantic.

9. Ctrl-C mid-paging quits the REPL, not just the paging. Reasonable choice — matches "Ctrl-C/D still quits" in the description — but worth confirming intent vs. SWI (which I think takes Ctrl-C as a soft cancel of the current goal). If q or a (SWI bindings for "stop" / "abort") feel natural, easy to add to the match arm.

What's good

• Reuses the engine's term writer via --format text instead of forking it into the REPL. The JSON-only alternative would have been shadow logic with all the precision-loss footguns.
• Atomic batch reveal. The Paging struct either holds a full batch or paging ends — no half-fetched state.
• UI suppresses editor cursor and mode indicator while paging. Correct UX signal that the input line isn't an editor right now. Hint is dimmed.
• Stale-buffer guard in run_query. A pending edit forces a recompile before fetch — paging can't run against a stale binary.
• Fetch enum keeps app ignorant of subprocess mechanics. NoSolutions / Failed / Timeout / Error / Found cleanly distinguish the cases the UI needs.
• Both ; and space advance. Matches SWI muscle memory.
• The pure pieces are unit-tested. split_solutions covers multi-var/single-var/all-anonymous; json_count/json_error pinned. The interactive seam is honestly acknowledged as untested.

Suggested order

#1 (re-render cost), #2 (double json_count), #3 (anchor JSON scrape) are quick wins worth doing before merge. #4 (silent misreport) is mostly defensive — fine as a follow-up unless you've seen the case fire. #5 onwards are taste/scope.

## Review — `;`-paging for query solutions The overall shape is right. The split between `run::fetch` (returns a `Fetch` enum — pure I/O outcome), `app::Paging` (state machine across `;` presses), and `ui` (suppress editor cursor + render hint) is clean. Refetch-with-doubled-limit is the documented design for stateless binaries, and reusing the engine's text writer instead of re-rendering JSON terms is the right call — point you made in the PR description and I agree. Issues below, ordered by impact. ### Real concerns **1. Refetch is O(n²) total work for long enumerations.** Each refetch re-executes the binary with a doubled limit and re-renders every prior solution. A 1000-solution query enumerated to completion runs fetches at 25 → 50 → 100 → 200 → 400 → 800 → 1600. Each fetch is two execs and a full text render — total ~3175 solution-renders for 1000 solutions, plus 14 process spawns. Interactive use is fine (a few `;` and done); a user who actually pages through everything pays this cost. Mitigations: - Track the high-water mark of seen solutions; only render+display the tail past `pos`. - Cap doubling at some ceiling (e.g. 1024). - Or just document the cost — the comment in `run.rs:9` calls out "two execs per fetch" but not the cumulative re-render. **2. `json_count` is called twice on the same payload.** `run.rs:81-86`: ```rust match json_count(&json) { Some(0) | None => return Fetch::NoSolutions, _ => {} } let count = json_count(&json).unwrap_or(0); ``` Should be one match that binds `count`: ```rust let count = match json_count(&json) { Some(0) | None => return Fetch::NoSolutions, Some(n) => n, }; ``` Cosmetic, but reads as a forgotten cleanup. **3. JSON scraping is fragile to wire-format changes.** `json.find("\"count\":")` matches anywhere the substring appears — today the engine only emits one `count` key, but if it ever grows a `line_count`/`subgoal_count`/etc., this picks the wrong one silently. Same for `json.contains("\"exhausted\":true")`. Two options: - Anchor with a leading delimiter: `find(",\"count\":")` / `find("{\"count\":")`. Cheap; pins the position. - Or use `serde_json` for the small JSON header — one more dep but kills the class. The two-exec design also quietly assumes the engine produces identical solutions in both passes (count from JSON, lines from text). Pure Prolog: yes. Anything with side effects (`time/1`, random, `assertz`): could drift. Worth one line in the module doc that this depends on inter-run determinism. **4. `split_solutions` non-uniform fallback can silently misreport count.** `run.rs:115-117`: if `lines.len() % count != 0`, it falls back to `lines.into_iter().map(str::to_string).collect()` — returning `lines.len()` strings as solutions even when `count` (the authoritative JSON value) said something else. The user pages through what looks like `lines.len()` solutions with no signal that something is off. Three lines (a `self.log(" warn: malformed engine output")` from app, or returning `Fetch::Failed(...)` from fetch) would surface it. ### Small observations **5. No test for the refetch path.** This is the only stateful piece of paging (limit doubling, `pos` carries over, new batch overwrites). The pure pieces are tested, but the most likely-to-break thing isn't — `page_next`'s borrow gymnastics around `need_more` + refetch are exactly where a refactor would silently regress. A test would need `run::fetch` to be injectable (trait or fn pointer); not in scope here, but flagging the gap. **6. Doubling is unbounded.** `limit.saturating_mul(2)` keeps growing as the user pages. With a divergent goal and a long `PLG_REPL_TIMEOUT`, you can find yourself waiting longer and longer per refetch with no cap. Modest defensive ceiling (e.g. 4096) would bound the worst case without affecting realistic use. **7. Paging assumes the engine produces solutions in a limit-independent order.** The refetch relies on `solutions[pos]` in the new (bigger) batch being the same as the unrevealed tail of the old. Standard left-to-right SLD resolution gives that, but it's worth a one-liner in the `Paging` doc — it's the invariant that keeps `pos` carrying across refetches. **8. UI hint text uses literal spaces for spacing.** `ui.rs:21` — `" ; next solution · any other key stop"`. Hand-tuned centering shifts oddly at narrow widths (and dimming applies to the leading spaces too, which is invisible but ratatui still walks them). Layout-aware (`Rect`-split and right-justify the hint) would be sturdier; pedantic. **9. `Ctrl-C` mid-paging quits the REPL, not just the paging.** Reasonable choice — matches "Ctrl-C/D still quits" in the description — but worth confirming intent vs. SWI (which I think takes Ctrl-C as a soft cancel of the current goal). If `q` or `a` (SWI bindings for "stop" / "abort") feel natural, easy to add to the match arm. ### What's good - **Reuses the engine's term writer** via `--format text` instead of forking it into the REPL. The JSON-only alternative would have been shadow logic with all the precision-loss footguns. - **Atomic batch reveal.** The `Paging` struct either holds a full batch or paging ends — no half-fetched state. - **UI suppresses editor cursor and mode indicator while paging.** Correct UX signal that the input line isn't an editor right now. Hint is dimmed. - **Stale-buffer guard in `run_query`.** A pending edit forces a recompile before fetch — paging can't run against a stale binary. - **`Fetch` enum keeps `app` ignorant of subprocess mechanics.** `NoSolutions` / `Failed` / `Timeout` / `Error` / `Found` cleanly distinguish the cases the UI needs. - **Both `;` and space advance.** Matches SWI muscle memory. - **The pure pieces are unit-tested.** `split_solutions` covers multi-var/single-var/all-anonymous; `json_count`/`json_error` pinned. The interactive seam is honestly acknowledged as untested. ### Suggested order #1 (re-render cost), #2 (double `json_count`), #3 (anchor JSON scrape) are quick wins worth doing before merge. #4 (silent misreport) is mostly defensive — fine as a follow-up unless you've seen the case fire. #5 onwards are taste/scope.

navicore added 1 commit 2026-06-17 00:36:45 +00:00

⏺ The review was useful, and one headline claim was worth pushing back on. ... fd67f6cf0b

Summary:

  Corrected (not a bug):
  - #1 "O(n²)" — actually O(N). Doubling makes total re-render work
  geometric; the reviewer's own figures (3175 renders for 1000 solutions ≈
  3×N) prove it's linear, not quadratic. So I fixed the documentation to
  state the honest ~2–3N cumulative cost instead of changing the algorithm,
  and added a cap (their #6) to bound the worst case.

  Fixed:
  - #2 — collapsed the double json_count into one match that binds count.
  - #3 — replaced the bare json.find("\"count\":") scrapes with top_field,
  which only matches a top-level key (preceded by {/,), so a future header
  field or a nested count functor in a solution can't be mistaken for the
  count. Added a test binding X to a count(9) compound to pin it. Also
  documented the inter-run determinism the two-exec design assumes (safe by
  construction — the engine has no random/assert/time).
  - #4 — split_solutions now returns None on a non-uniform shape and fetch
  surfaces Fetch::Failed("malformed query output…") instead of silently
  paging a wrong grouping. Tested.
  - #6 — re-fetch limit is capped at SOLUTION_CAP = 4096; hitting it logs
  stopped at N solutions (batch cap). rather than growing per-fetch
  cost/timeout unbounded.
  - #7 — documented the limit-independent-order invariant on Paging that
  makes pos carry across re-fetches.

  Deliberately skipped (with reasons):
  - #5 refetch test — real gap, but needs fetch injectable
  (trait/fn-pointer) to unit-test the stateful path; that's a bigger
  refactor and genuinely out of this slice's scope.
  - #8 hint spacing — pedantic.
  - #9 q/a to stop — already covered: any non-; key stops paging, so q/a
  work today; Ctrl-C quitting the REPL is the intended, documented choice.

  The "what's good" notes also re-confirmed the core call (reuse the
  engine's text writer rather than fork it into the REPL), which was the
  main design risk worth a second opinion.

navicore merged commit 11a0e1ada8 into main 2026-06-17 00:39:16 +00:00

navicore deleted branch paging 2026-06-17 00:39:16 +00:00

navicore referenced this pull request from a commit 2026-06-17 00:39:18 +00:00

Merge pull request '⏺ ;-paging is in — clippy -D warnings, 16 tests (4 new), fmt, and full workspace' (#13) from paging into main

Sign in to join this conversation.

Reviewers

No reviewers

Labels

Clear labels

No items

No labels

Milestone

Clear milestone

No items

No milestone

Projects

Clear projects

No items

No project

Assignees

Clear assignees

No assignees

1 participant

Notifications

Subscribe

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference

navicore/patch-prolog!13

No description provided.