Merge remote-tracking branch 'gh/main' into fix/90ea-fmt-root-package
# Conflicts: # context/test-evidence/tooling.md
This commit is contained in:
+18
-15
File diff suppressed because one or more lines are too long
@@ -126,9 +126,16 @@ Two agents each adding a workspace member will still collide in
|
||||
reports spurious failures. And **never pipe a gate**: `$?` must be the gate's
|
||||
own, and `check-comment-runs.py --check-evidence` prints two lines with the
|
||||
comment cap **first**, so `| tail -1` silently drops half of it.
|
||||
4. **Do not push, do not merge to `main`.** The orchestrator merges.
|
||||
5. The commit-message trailers, spelled out.
|
||||
6. **What to report**: branch and commits, what changed per ticket, *what could
|
||||
4. **Commit frequently, so the work is safe in git.** A WIP commit after the
|
||||
first green test, and again after every meaningful step. A worktree is not
|
||||
durable storage: an agent finished a whole ticket with every gate green and
|
||||
lost all of it, uncommitted, when its worktree was deleted during a disk
|
||||
cleanup. Tidying the history before the PR is fine; losing it is not.
|
||||
5. **Do not merge to `main`.** The orchestrator merges. Pushing the agent's own
|
||||
branch (`git push gh HEAD:refs/heads/<branch>`) is encouraged once it is
|
||||
worth keeping.
|
||||
6. The commit-message trailers, spelled out.
|
||||
7. **What to report**: branch and commits, what changed per ticket, *what could
|
||||
not be verified and why*, and proposed repo-map/`kb.pl` text. Ask explicitly
|
||||
for the thing the agent learned that the ticket did not predict — that is
|
||||
consistently the most valuable part of a hand-back, and agents omit it unless
|
||||
|
||||
+17
-2
@@ -891,8 +891,23 @@ gotcha 47 asks for — closing e24v has to come to that line and delete it.
|
||||
broadcasts nothing, so it reaches this user and no one else. This argument
|
||||
arrived as `edit_or_drill`'s, i.e. about `i`/`a` on an aggregate, and for a
|
||||
while it read as doctrine for `>` while `>` was still silent. Both doors now
|
||||
refuse, and **they refuse with different sentences on purpose**: "this key is
|
||||
not built yet" and "this cell is not yours to write" are different facts.
|
||||
refuse, and **they name the same missing feature in the same words** —
|
||||
`not_yet("drill")` — because they reach the same one. In the TUI,
|
||||
`EditOrDrill` hands an aggregate straight to `DrillIntoCell`, so an aggregate
|
||||
*is* writable there, by drilling; `i` on it is drill by another door. `i`'s
|
||||
sentence adds only *why* it drilled rather than edited ("an aggregate is
|
||||
edited by drilling in — …"), and `>` still says nothing about aggregates,
|
||||
because it is refused whatever the cell is.
|
||||
|
||||
This **reverses** what this bullet said until improvise-s8h7: that the two
|
||||
refused with different sentences on purpose, "this key is not built yet"
|
||||
against "this cell is not yours to write". The second half was false about
|
||||
the application — nothing refuses a write to an aggregate; the TUI drills —
|
||||
and the separate wording hid from a browser user that `i` and `>` were one
|
||||
missing feature. The help page's `edit-or-drill` caption carried the same
|
||||
error, calling `i` only "Edit current cell"; it now says it drills into an
|
||||
aggregate, which is true in both front ends because the browser's refusal
|
||||
names drill. Delivering drill is `improvise-obtu`'s, not this bullet's.
|
||||
- **The commit's write is not spelled again here.** It is
|
||||
`Client::typed_cell`'s, the same one click-to-edit uses, so a browser keyboard
|
||||
commit and a browser mouse commit cannot disagree about what `""` or `"42"`
|
||||
|
||||
@@ -83,8 +83,67 @@ argument but the last, so `doctrine(Name,_)` keys on the name and
|
||||
through, and it overwrites in place — a count that grew would be two clauses
|
||||
under one name.
|
||||
|
||||
**A write may not end up short of HEAD** (improvise-usus). `kb add` wrote four
|
||||
facts onto a working-tree `kb.pl` that had already lost 276 of its 801, and
|
||||
reported success: `kb_consistent` asks whether the facts are *consistent*, never
|
||||
whether they are all *there*, and a knowledge base missing a prefix of a
|
||||
predicate is perfectly consistent. `kb-merge` printed `529 before` beside a last
|
||||
known 805 and nothing compared them. The cause was never settled between a
|
||||
`kb replace` killed mid-write and git being moved under the session, so the
|
||||
guard had to catch both, and only a comparison against something *outside* the
|
||||
working tree can: a guard that compares the file against its own pre-write
|
||||
count passes a file that was truncated before the write began, which is exactly
|
||||
what happened. So every write runs `kb-merge.pl complete` on the candidate,
|
||||
before `kb_consistent`, against `git show HEAD:prolog-sessions/kb.pl`, and
|
||||
refuses unless every clause HEAD has is still present **by key**. It runs first
|
||||
so that the refusal names the loss rather than whatever consistency error the
|
||||
loss happens to cause.
|
||||
|
||||
It compares keys rather than counts, although the ticket asked for a count,
|
||||
because a count can be masked: uncommitted adds in one predicate offset a
|
||||
truncation in another, and the count comes out even. Keys cost the same (0.26s
|
||||
for a write, most of it trealla start-up) and the message still names both
|
||||
totals and the number missing.
|
||||
|
||||
**How the count legitimately falls.** `add` never lowers it and `replace`
|
||||
overwrites in place, so neither can trip the guard. `kb rm` is the only
|
||||
intended removal, and it records the keys it removed in a **ledger** that later
|
||||
writes read: a clause missing from the working tree is excused only if its key
|
||||
is in the ledger. The ledger lives in the git dir (`git rev-parse --git-path
|
||||
kb-removed.pl`), so it is per-worktree and can never be committed; with
|
||||
`KB_FILE` set it sits beside that file. It prunes itself on every write, keeping
|
||||
only keys HEAD still has and the candidate does not, so an entry drops once the
|
||||
removal is committed, and once the key is re-added. That second case matters:
|
||||
without it, a re-added clause that was lost again would still be excused. There
|
||||
is deliberately no override flag. The way out of a refusal is to restore
|
||||
`kb.pl` from HEAD and re-apply, or to commit the removal so HEAD moves.
|
||||
|
||||
**The write is a rename.** The candidate used to come from `mktemp` in
|
||||
`$TMPDIR`, and `mv` from there onto the repository crosses a device wherever
|
||||
`/tmp` is its own filesystem. That makes `mv` a copy and an unlink, so a kill
|
||||
partway through leaves a truncated `kb.pl`. The candidate is now a sibling of
|
||||
`kb.pl` (`kb.pl.cand.XXXXXX`), so publishing it is `rename(2)`. The ledger is
|
||||
renamed first. A kill between the two renames then leaves a ledger naming keys
|
||||
the kb still has, and the next write prunes those entries. Until it does, they
|
||||
would excuse the loss of exactly those clauses, which is a narrower hole than a
|
||||
kb.pl that is already short.
|
||||
|
||||
**Exit codes.** 0 done, 1 refused, 2 usage, 3 HEAD's `kb.pl` could not be read,
|
||||
127 no `tpl`. Only 1 is a verdict. 3 is separate because "could not compare"
|
||||
is not "compared and refused" (improvise-b4ks). A pre-existing wart survives:
|
||||
failing to acquire the lock exits 1 too.
|
||||
|
||||
## What no test here reaches
|
||||
|
||||
The completeness guard trusts HEAD. A loss that has been **committed** is
|
||||
invisible to it by construction. That was the right trade for this incident,
|
||||
where HEAD held all 801, but a bad commit of `kb.pl` becomes the new floor.
|
||||
|
||||
A `SIGKILL` leaves its `kb.pl.cand.*` and `kb.pl.lock` behind, because no trap
|
||||
runs. The lock already had that property. The stray candidate is new: it is
|
||||
never read, but it shows as untracked in `prolog-sessions/`, where a `git add
|
||||
-A` would pick it up.
|
||||
|
||||
The key rule is looser than `functional/1` for `crate/3`, which keys on the
|
||||
first argument alone; `kb_consistent` is the backstop for that case rather than
|
||||
the merge.
|
||||
|
||||
@@ -1389,28 +1389,74 @@ happened* passes against a page that has stopped listening, so it presses `i`
|
||||
afterwards and requires `#status` to change. Without that, this file would be
|
||||
folklore with a green tick.
|
||||
|
||||
### the_drill_key_and_an_aggregate_edit_refuse_for_different_reasons
|
||||
### an_aggregate_edit_names_the_same_missing_drill_as_the_drill_key
|
||||
|
||||
The Rust half of the interim, and the assertion that carries the whole weight.
|
||||
Two keys on the same aggregate cell must both refuse and must **not** refuse
|
||||
with the same sentence: `>` says drill is unavailable, `i` says drilling into an
|
||||
aggregate needs the host. Collapsing them into one message would be the
|
||||
tempting tidy-up and would lose the distinction between "this key does nothing
|
||||
here yet" and "this cell is not one you may write".
|
||||
improvise-s8h7. Until it, this test was
|
||||
`the_drill_key_and_an_aggregate_edit_refuse_for_different_reasons` and asserted
|
||||
the opposite: that `i` and `>` on an aggregate must refuse with *different*
|
||||
sentences, "this key does nothing here yet" against "this cell is not one you
|
||||
may write". The second half was false about the application. `EditOrDrill`
|
||||
hands an aggregated cell to `DrillIntoCell`, so in the TUI `i` on an aggregate
|
||||
**is** drill — nothing refuses the write, it drills — and the browser's
|
||||
separate wording ("drilling into an aggregate needs the host") hid that `i` and
|
||||
`>` are one missing feature. The reasoning is `context/code/clients.md`.
|
||||
|
||||
**The injection, and why it is not the obvious one.** Replacing `>`'s sentence
|
||||
with the *aggregate* sentence looks like it should fail on the first assertion —
|
||||
and does not: that sentence contains both "drill" and "browser", so it clears
|
||||
the substring check. What fires is the anti-aggregate assertion lower down. The
|
||||
claim that the second assertion is the load-bearing one was doubted on review,
|
||||
tested, and confirmed; record it here because the first assertion reads like the
|
||||
discriminating one and is not.
|
||||
So the test now asserts four things on one aggregate fixture: `>` names drill
|
||||
and the browser; `>` does **not** mention aggregates (it is refused whatever the
|
||||
cell is); `i`'s sentence **contains** `>`'s sentence verbatim; and `i`'s
|
||||
sentence mentions "aggregate", so it still says why it drilled rather than
|
||||
edited. The fixture is `client_on(CellId::Aggregate(..))` rather than the old
|
||||
empty `in_mode` state, because `i` needs a cell under the cursor to reach the
|
||||
`Aggregate` arm at all — on an empty grid it answers nothing and only `>` was
|
||||
ever exercised.
|
||||
|
||||
The harness sibling (`drill.spec.js`) asserts the same distinction in a browser,
|
||||
but its `not.toContainText("aggregate")` is **decoration under the only
|
||||
injection that exists** — Playwright throws at the positive assertion above it
|
||||
first, so that line is never reached. The Rust assertion is the guard; the
|
||||
harness one is end-to-end confirmation that the string survives the wire.
|
||||
**Three injections, each failing at a different assertion.** Run, not reasoned:
|
||||
|
||||
- `i` says only `not_yet("drill")` — the "why" dropped. Fails at the last
|
||||
assertion, "and `i` must still say why". This is the tempting over-tidy fix.
|
||||
- `>`'s `declined` subject becomes "drilling into an aggregate". Fails at the
|
||||
anti-aggregate assertion on `>`. Note that `i` still contains `>`'s *old*
|
||||
sentence here, because `edit_or_drill` calls `not_yet("drill")` itself rather
|
||||
than going through `declined` — so the containment assertion alone would not
|
||||
have caught a `>` that started blaming the cell.
|
||||
- `i` paraphrases ("… drill needs the host"). Fails at the containment
|
||||
assertion: the same feature named in different words is exactly what the
|
||||
ticket reported.
|
||||
|
||||
The harness sibling (`drill.spec.js`) asserts the same wording in a browser.
|
||||
Its `not.toContainText("aggregate")` on `>` is still **decoration under the
|
||||
only injection that exists** — Playwright throws at the positive assertion
|
||||
above it first — so the Rust assertion is the guard and the harness is
|
||||
end-to-end confirmation that the string survives the wire.
|
||||
|
||||
### the_edit_key_row_says_it_drills_into_an_aggregate
|
||||
|
||||
improvise-s8h7, the help-page half. The `edit-or-drill` row on the Editing page
|
||||
read "Edit current cell", while `i`/`a` on an aggregate drill in the TUI and
|
||||
name drill in the browser. The row is found by its **keys** — the labels
|
||||
`keys_for(Normal, "edit-or-drill", ["editing"])` returns — not by its caption,
|
||||
and exactly one row must carry them, so a caption fix that also moved or
|
||||
duplicated the row fails on the `let [..]` pattern rather than passing on
|
||||
whichever copy was found first. Failed at HEAD on the caption; the injection
|
||||
"Edit current cell, or drill" (drill named, aggregate not) fails it too, since
|
||||
`>` is also drill and the row must say *when* `i` drills.
|
||||
|
||||
### only_the_edit_key_is_captioned_as_editing_the_cell
|
||||
|
||||
Found while fixing improvise-s8h7, not predicted by it. The row below the edit
|
||||
key read `Enter Edit current cell (same as i)`, but Normal-mode Enter is bound
|
||||
to `enter-advance` alone — not a `Binding::Sequence` — and `EnterAdvance` only
|
||||
moves the cursor down, wrapping to the next column. The test takes every help
|
||||
row captioned "Edit current cell" and requires its keys to be a subset of
|
||||
`edit-or-drill`'s; at HEAD it failed naming `["Enter"]`. The fix moved the row
|
||||
to the Navigation page's "Cursor movement" section with a caption that says
|
||||
what it does.
|
||||
|
||||
Its reach is stated rather than implied: it checks the one phrase that was
|
||||
false. A caption that misdescribes Enter in *other* words passes it: a caption
|
||||
is prose, and nothing checks it against the command it documents. That is a
|
||||
neighbour of improvise-wk18, not the same gap — wk18 is about `literal()` rows
|
||||
whose *keys* go unchecked; here the keys were right and the words were wrong.
|
||||
|
||||
### a_view_row_click_focuses_moves_and_switches_to_the_row_clicked
|
||||
|
||||
@@ -4041,17 +4087,18 @@ Demonstrated at `e7de19d`: the first test below reports `Some("")`.
|
||||
|
||||
### `an_editing_mode_with_no_edit_buffer_shows_the_cell_rather_than_a_blank`
|
||||
|
||||
The fallback is `improvise_protocol::edit_seed`, which is the **existing** home
|
||||
of "what an editor opened here starts with" — `seed_at` at the cursor, the
|
||||
function `enter-advance` already seeds from. A second reconciliation of the
|
||||
scroll offset inside `render.rs` would have been gotcha 42's own trap, so the
|
||||
one-line fallback cost one `pub` rather than a copy.
|
||||
**Superseded in part by improvise-ktlk** (entry at the end of this file). As
|
||||
first landed, the fallback lived in `render.rs`: `editing` fell back to
|
||||
`edit_seed` while `commit` and `append-char` still read the absent buffer as
|
||||
`""`, so the overlay showed `1200` and Enter cleared it. The fallback now lives
|
||||
in the fold (`ClientState::settle_editor`), which seeds the buffer itself, and
|
||||
`render.rs` reads the same buffer `commit` does. The test's first assertion
|
||||
changed with it: it used to check that the buffer was still absent after the
|
||||
fold, and now checks that the fold seeded it.
|
||||
|
||||
The test asserts three things in order, and the middle one is why it is not
|
||||
vacuous: that the buffer really is absent, that the cell really holds `1200`,
|
||||
and only then what `editing` says. Without the first two a fixture that happened
|
||||
to carry an `edit` buffer, or a grid whose cell was blank anyway, would pass
|
||||
against the bug.
|
||||
The test asserts three things in order: what the fold put in the buffer, that
|
||||
the cell really holds `1200`, and only then what `editing` says. Without the
|
||||
second, a grid whose cell was blank anyway would pass against the bug.
|
||||
|
||||
**Fault injected:** `unwrap_or_default()`, the original expression. Fails with
|
||||
`Some("")`.
|
||||
@@ -4177,3 +4224,40 @@ and converged.
|
||||
|
||||
**Fault injected:** the same `Binding::Prefix` → `Upstream` reversion. Fails on
|
||||
the second press.
|
||||
|
||||
## improvise-ktlk — the overlay and the commit read one buffer
|
||||
|
||||
PR #162 (improvise-xg1z) changed what the overlay **draws** for an `Editing`
|
||||
mode that arrived without its `edit` buffer, and not what Enter **commits**.
|
||||
`render.rs` painted `edit_seed(state)`, while `resolve.rs::commit` and
|
||||
`append-char` read `read_buffer(&state.view, "edit")`, which is `""` for an
|
||||
absent key. So the overlay showed the value, Enter composed `ClearCell`, and one
|
||||
typed character replaced the shown text rather than extending it. #162's tests
|
||||
only looked at the drawing, and none of them pressed a key.
|
||||
|
||||
The fix gives the fact one home. The fold seeds the missing buffer
|
||||
(`ClientState::settle_editor`, called after every fold, bootstrap and refusal,
|
||||
beside `settle_mode`), and `render.rs` reads the buffer through `read_buffer`,
|
||||
as `commit` does. `edit_seed` is `pub(crate)` again and no renderer calls it.
|
||||
Seeding happens only when there is a cell under the cursor that has
|
||||
`edit_text`. With no such cell the buffer stays absent, which reads as `""`
|
||||
on both paths, and `commit` declines anyway for want of a cell.
|
||||
|
||||
### `an_editor_entered_without_its_buffer_commits_and_extends_the_cell`
|
||||
|
||||
The fixture's display text (`1,200.50`) and edit text (`1200.5`) **differ**.
|
||||
With `CellDisplay::number("1200")`, as #162 used, a fallback that seeds from the
|
||||
formatted `text` passes too (gotcha 8). The test folds `ChangeMode(editing)`
|
||||
with no `SetBuffer`, then presses the keys: Enter must compose
|
||||
`SetCell(Number(1200.5))`, and after a typed `5`, Enter must compose
|
||||
`SetCell(Number(1200.55))`.
|
||||
|
||||
**Faults injected, each run:**
|
||||
- The tree before this fix (render-only fallback). The buffer assertion fails
|
||||
with `""`. With that assertion removed, the Enter assertion fails on its own
|
||||
with `None`, because the first command is `ClearCell`.
|
||||
- `edit_seed` returning the drawn `text` instead of `edit_text`. Fails with
|
||||
`"1,200.50"`.
|
||||
- The over-broad seed, "absent **or empty**, refill". This test passes, and
|
||||
`an_edit_buffer_the_user_has_emptied_is_not_refilled_from_the_cell` fails,
|
||||
as it did against the same rival in `render.rs`.
|
||||
|
||||
@@ -503,3 +503,51 @@ to `src/ui/text.rs` is reported (`Diff in …/src/ui/text.rs:72`).
|
||||
should not is not detected, and a package in a directory the find excludes
|
||||
(`target/`, `.claude/`, `node_modules/`) is outside the invariant by
|
||||
construction.
|
||||
|
||||
### The kb tool's completeness guard and atomic write — `scripts/kb-test.sh` cases 18–22
|
||||
|
||||
improvise-usus: `scripts/kb add` wrote onto a working-tree `kb.pl` that had lost
|
||||
276 of its 801 clauses, and `kb_consistent` passed. The argument for the fix
|
||||
(compare with HEAD by key, record `kb rm` removals in a ledger, publish by
|
||||
rename) is in `context/code/kb-tool.md`. This entry covers what each case was
|
||||
watched to catch.
|
||||
|
||||
**Reproduced at `40b8913` before any fix.** A copy of HEAD's `kb.pl` with 34 of
|
||||
its 35 `location/3` facts removed still passes `kb_consistent`, and
|
||||
`kb add` onto it printed `775 before, 1 in delta, 776 after` and exited 0.
|
||||
Against the unfixed tool, the new cases gave 33 passed, 5 failed: 18, 19, 20b,
|
||||
21 and 22 failed. Case 20 passed there because an rm followed by an add has no
|
||||
guard to trip.
|
||||
|
||||
**The fixture has to fail in the incident's shape.** The ticket's "truncate to
|
||||
half" fixture also breaks `kb_consistent`, because the rules live in the second
|
||||
half. So the unfixed tool refused it too, by the wrong guard. Removing a whole
|
||||
predicate is an existence error, and removing cited clauses fails the citation
|
||||
check. Case 18 keeps one `location/3` fact and asserts that the fixture passes
|
||||
`kb_consistent` before using it. Case 19 keeps the ticket's half-truncation, and
|
||||
`said()` is what makes it evidence: the completeness guard runs first and must
|
||||
be the one that answers.
|
||||
|
||||
**Rivals injected into `scripts/kb`, one at a time. Each failed only its own
|
||||
case:**
|
||||
|
||||
- baseline taken from the file's own pre-write state rather than HEAD: 18, 19
|
||||
and 20b failed (35/38 passed). This is the guard that would have passed the
|
||||
real incident.
|
||||
- ledger never consulted: 20 and 20b failed. A legitimate rm then blocks every
|
||||
later write.
|
||||
- guard stands down whenever the ledger is non-empty: 20b failed.
|
||||
- candidate built by plain `mktemp` in `$TMPDIR`: 22 failed on the directory
|
||||
check.
|
||||
- candidate copied over `kb.pl` before the publish point: 22 failed as
|
||||
modified.
|
||||
- unreadable baseline exiting 1 rather than 3: 21 failed.
|
||||
|
||||
**A rival can fail wider than its fault.** The first form of the "stands down"
|
||||
rival skipped `merge complete` altogether. That also skipped writing
|
||||
`$cand.ledger`, so the later `mv` crashed under `set -e` and five unrelated
|
||||
cases failed. It proved nothing until it was rewritten to carry the ledger
|
||||
forward.
|
||||
|
||||
**Checked by hand, not in the suite:** the ledger prunes an entry once the key
|
||||
is re-added and once HEAD stops having it (a committed removal).
|
||||
|
||||
@@ -74,6 +74,7 @@ impl ClientState {
|
||||
self.apply_projection(projection);
|
||||
}
|
||||
self.settle_mode();
|
||||
self.settle_editor();
|
||||
self.revision += 1;
|
||||
}
|
||||
|
||||
@@ -85,6 +86,7 @@ impl ClientState {
|
||||
other => reduce_view(&mut self.view, other),
|
||||
}
|
||||
self.settle_mode();
|
||||
self.settle_editor();
|
||||
self.revision += 1;
|
||||
}
|
||||
|
||||
@@ -124,6 +126,7 @@ impl ClientState {
|
||||
}
|
||||
self.last_rejection = Some(rejection);
|
||||
self.settle_mode();
|
||||
self.settle_editor();
|
||||
self.revision += 1;
|
||||
}
|
||||
|
||||
@@ -158,6 +161,21 @@ impl ClientState {
|
||||
self.view.mode = settled_mode(&self.view.mode, self.grid.records);
|
||||
}
|
||||
|
||||
/// An editor that arrived without its buffer is seeded here, so what is
|
||||
/// drawn and what Enter commits read one buffer (improvise-ktlk).
|
||||
fn settle_editor(&mut self) {
|
||||
let absent = self
|
||||
.view
|
||||
.mode
|
||||
.minibuffer()
|
||||
.filter(|_| self.view.mode.is_editing())
|
||||
.map(|mb| mb.buffer_key.clone())
|
||||
.filter(|key| !self.view.buffers.contains_key(key));
|
||||
if let (Some(key), Some(seed)) = (absent, crate::resolve::edit_seed(self)) {
|
||||
self.view.buffers.insert(key, seed);
|
||||
}
|
||||
}
|
||||
|
||||
/// The widget dispatch: a projection names the widget it is addressed to.
|
||||
/// The `CategoryTreeCache`/`TileBarCache` overlap is deliberate (gotcha 32).
|
||||
fn apply_projection(&mut self, projection: &Projection) {
|
||||
|
||||
@@ -439,6 +439,12 @@ fn navigation() -> Vec<HelpLine> {
|
||||
Some(HelpLine::Heading("Cursor movement")),
|
||||
Some(HelpLine::Blank),
|
||||
keys(n, "move-selection", None, "Move one cell"),
|
||||
keys(
|
||||
n,
|
||||
"enter-advance",
|
||||
None,
|
||||
"Move down, wrapping to the next column",
|
||||
),
|
||||
Some(literal("gg", "Jump to first row")),
|
||||
keys(n, "jump-last-row", None, "Jump to last row"),
|
||||
keys(n, "jump-first-col", None, "Jump to first column"),
|
||||
@@ -513,8 +519,12 @@ fn editing() -> Vec<HelpLine> {
|
||||
Some(HelpLine::Blank),
|
||||
Some(HelpLine::Heading("Entering edit mode")),
|
||||
Some(HelpLine::Blank),
|
||||
keys(n, "edit-or-drill", Some(&["editing"]), "Edit current cell"),
|
||||
keys(n, "enter-advance", None, "Edit current cell (same as i)"),
|
||||
keys(
|
||||
n,
|
||||
"edit-or-drill",
|
||||
Some(&["editing"]),
|
||||
"Edit current cell (drill into an aggregate)",
|
||||
),
|
||||
keys(
|
||||
e,
|
||||
"clear-buffer",
|
||||
@@ -950,6 +960,58 @@ mod tests {
|
||||
"an undescribed name falls back to itself rather than to silence"
|
||||
);
|
||||
}
|
||||
|
||||
fn rows() -> Vec<(Vec<String>, &'static str)> {
|
||||
pages()
|
||||
.into_iter()
|
||||
.flat_map(|page| page.lines)
|
||||
.filter_map(|line| match line {
|
||||
HelpLine::Keys { keys, description } => Some((keys, description)),
|
||||
_ => None,
|
||||
})
|
||||
.collect()
|
||||
}
|
||||
|
||||
fn labels_of(command: &str, args: Option<&[String]>) -> Vec<String> {
|
||||
keys_for(&ModeKey::Normal, command, args)
|
||||
.iter()
|
||||
.map(|(c, m)| key_label(c, *m))
|
||||
.collect()
|
||||
}
|
||||
|
||||
/// improvise-s8h7: `i` on an aggregate drills in the TUI, so the row
|
||||
/// that documents it must say so. See `context/test-evidence/clients.md`.
|
||||
#[test]
|
||||
fn the_edit_key_row_says_it_drills_into_an_aggregate() {
|
||||
let edit = labels_of("edit-or-drill", Some(&["editing".to_string()]));
|
||||
let found: Vec<_> = rows().into_iter().filter(|(k, _)| *k == edit).collect();
|
||||
let [(_, description)] = &found[..] else {
|
||||
panic!("expected one help row keyed {edit:?}, got {found:?}");
|
||||
};
|
||||
assert!(
|
||||
description.contains("drill") && description.contains("aggregate"),
|
||||
"{edit:?} drills into an aggregate and the row must say so: {description}"
|
||||
);
|
||||
}
|
||||
|
||||
/// improvise-s8h7: Normal's Enter is `enter-advance`, which only moves.
|
||||
/// See `context/test-evidence/clients.md`.
|
||||
#[test]
|
||||
fn only_the_edit_key_is_captioned_as_editing_the_cell() {
|
||||
let edit = labels_of("edit-or-drill", Some(&["editing".to_string()]));
|
||||
let claims: Vec<_> = rows()
|
||||
.into_iter()
|
||||
.filter(|(_, d)| d.contains("Edit current cell"))
|
||||
.collect();
|
||||
assert!(!claims.is_empty(), "the check needs a row to check");
|
||||
for (keys, description) in claims {
|
||||
assert!(
|
||||
keys.iter().all(|k| edit.contains(k)),
|
||||
"{keys:?} is captioned {description:?} but only {edit:?} edit"
|
||||
);
|
||||
}
|
||||
}
|
||||
|
||||
/// Not an assertion: a printout for a human to read once. `cargo test -p
|
||||
/// improvise-protocol eyeball -- --nocapture --ignored`.
|
||||
#[test]
|
||||
|
||||
@@ -34,7 +34,7 @@ pub use render::{
|
||||
WizardProposal, WizardStepKind, header_level_widths,
|
||||
};
|
||||
pub use resolve::{
|
||||
Click, KeyOutcome, Request, click, edit_seed, read_buffer, resolve, typed, typed_cell_command,
|
||||
Click, KeyOutcome, Request, click, read_buffer, resolve, typed, typed_cell_command,
|
||||
};
|
||||
pub use viewmodel::{CatTreeEntry, flatten_cat_tree, view_axis_summary};
|
||||
// `improvise-core`'s, because the index that resolves one lives in
|
||||
|
||||
@@ -748,9 +748,10 @@ fn edit_or_drill(state: &ClientState, mode: AppMode) -> Option<Vec<Command>> {
|
||||
},
|
||||
Command::ChangeMode(mode),
|
||||
]),
|
||||
CellId::Aggregate(_) => Some(vec![Command::SetStatus(
|
||||
"drilling into an aggregate needs the host — not in the browser yet".to_string(),
|
||||
)]),
|
||||
CellId::Aggregate(_) => Some(vec![Command::SetStatus(format!(
|
||||
"an aggregate is edited by drilling in — {}",
|
||||
not_yet("drill")
|
||||
))]),
|
||||
CellId::Derived { target } => Some(vec![Command::SetStatus(format!(
|
||||
"{target} is computed by a formula — edit the formula, not the cell"
|
||||
))]),
|
||||
@@ -954,11 +955,10 @@ fn record_at_cursor(state: &ClientState) -> Option<crate::RecordHash> {
|
||||
}
|
||||
}
|
||||
|
||||
/// What an editor opened on the cursor starts with. The one home, so a
|
||||
/// renderer does not reconcile the scroll offset again (gotcha 42).
|
||||
pub fn edit_seed(state: &ClientState) -> String {
|
||||
let (row, col) = state.view.cursor().selected;
|
||||
seed_at(state, row, col)
|
||||
/// What an editor opened on the cursor starts with, or `None` with no cell
|
||||
/// there to seed from. Read by the fold, never a renderer (improvise-ktlk).
|
||||
pub(crate) fn edit_seed(state: &ClientState) -> Option<String> {
|
||||
cell_at_cursor(state)?.edit_text.clone()
|
||||
}
|
||||
|
||||
/// The display text at an absolute grid position, as the cache holds it.
|
||||
@@ -2435,28 +2435,38 @@ mod tests {
|
||||
);
|
||||
}
|
||||
|
||||
/// The advertised key must say what is actually true. Two refusals, two
|
||||
/// subjects — see `context/test-evidence/clients.md`.
|
||||
/// `i` on an aggregate IS drill in the TUI, so both doors name one missing
|
||||
/// feature; only `i` says why. See `context/test-evidence/clients.md`.
|
||||
#[test]
|
||||
fn the_drill_key_and_an_aggregate_edit_refuse_for_different_reasons() {
|
||||
let mut state = in_mode(AppMode::Normal);
|
||||
state.grid.extent = GridExtent { rows: 2, cols: 2 };
|
||||
state.window = (2, 2);
|
||||
|
||||
let KeyOutcome::Local(drill) = resolve(&state, ev(KeyCode::Char('>'))) else {
|
||||
panic!("`>` is advertised in the hint line; it must answer");
|
||||
};
|
||||
let [Command::SetStatus(said)] = &drill[..] else {
|
||||
panic!("expected one status, got {drill:?}");
|
||||
fn an_aggregate_edit_names_the_same_missing_drill_as_the_drill_key() {
|
||||
let aggregate = CellId::Aggregate(
|
||||
serde_json::from_str("\"aa4c8e5e9cbd578e0d388f4b2b5a7879\"").unwrap(),
|
||||
);
|
||||
let state = client_on(aggregate);
|
||||
let said = |key| match resolve(&state, ev(key)) {
|
||||
KeyOutcome::Local(commands) => match &commands[..] {
|
||||
[Command::SetStatus(said)] => said.clone(),
|
||||
other => panic!("expected one status, got {other:?}"),
|
||||
},
|
||||
other => panic!("{key:?} is advertised; it must answer, got {other:?}"),
|
||||
};
|
||||
let (drill, edit) = (said(KeyCode::Char('>')), said(KeyCode::Char('i')));
|
||||
assert!(
|
||||
said.contains("drill") && said.contains("browser"),
|
||||
"the status must name drill and say it is the browser that lacks it: {said}"
|
||||
drill.contains("drill") && drill.contains("browser"),
|
||||
"the status must name drill and say it is the browser that lacks it: {drill}"
|
||||
);
|
||||
assert!(
|
||||
!said.contains("aggregate"),
|
||||
"a sentence about aggregates is TRUE-SOUNDING about the wrong thing — \
|
||||
`>` is refused whatever the cell is: {said}"
|
||||
!drill.contains("aggregate"),
|
||||
"`>` is refused whatever the cell is, so it must not blame the cell: {drill}"
|
||||
);
|
||||
assert!(
|
||||
edit.contains(&drill),
|
||||
"`i` reached the same missing feature and must name it the same way: \
|
||||
{edit:?} does not contain {drill:?}"
|
||||
);
|
||||
assert!(
|
||||
edit.contains("aggregate"),
|
||||
"and `i` must still say why it drilled rather than edited: {edit}"
|
||||
);
|
||||
}
|
||||
|
||||
@@ -3017,6 +3027,55 @@ mod tests {
|
||||
));
|
||||
}
|
||||
|
||||
/// improvise-ktlk: what an editor shows and what Enter commits are one
|
||||
/// fact. See `context/test-evidence/clients.md`.
|
||||
#[test]
|
||||
fn an_editor_entered_without_its_buffer_commits_and_extends_the_cell() {
|
||||
let mut client = client_on(record_cell());
|
||||
let mut cell = CellDisplay::number("1,200.50");
|
||||
cell.edit_text = Some("1200.5".into());
|
||||
cell.id = Some(record_cell());
|
||||
client.fold(&Command::Project(Projection::Grid(GridUpdate::Cells(
|
||||
vec![((0, 0), cell)],
|
||||
))));
|
||||
client.fold(&Command::ChangeMode(AppMode::editing()));
|
||||
assert_eq!(
|
||||
read_buffer(&client.view, "edit"),
|
||||
"1200.5",
|
||||
"the buffer is what the overlay paints and what a commit reads"
|
||||
);
|
||||
|
||||
let committed = |client: &ClientState| {
|
||||
let KeyOutcome::Local(commands) = resolve(client, ev(KeyCode::Enter)) else {
|
||||
panic!("Enter in Editing must resolve here");
|
||||
};
|
||||
match &commands[0] {
|
||||
Command::Model {
|
||||
cmd: ModelCommand::SetCell { value, .. },
|
||||
..
|
||||
} => Some(value.clone()),
|
||||
_ => None,
|
||||
}
|
||||
};
|
||||
assert_eq!(
|
||||
committed(&client),
|
||||
Some(CellValue::Number(1200.5)),
|
||||
"Enter on an editor showing the cell must not clear it"
|
||||
);
|
||||
|
||||
let KeyOutcome::Local(typed) = resolve(&client, ev(KeyCode::Char('5'))) else {
|
||||
panic!("a character in Editing is append-char");
|
||||
};
|
||||
for command in &typed {
|
||||
client.fold(command);
|
||||
}
|
||||
assert_eq!(
|
||||
committed(&client),
|
||||
Some(CellValue::Number(1200.55)),
|
||||
"a typed character extends what the editor showed, not replaces it"
|
||||
);
|
||||
}
|
||||
|
||||
/// At the bottom-right corner `EnterAdvance` returns `AbortChain`, so the
|
||||
/// commit leaves the user in normal mode. See the evidence file.
|
||||
#[test]
|
||||
|
||||
@@ -294,16 +294,13 @@ pub fn render_model(state: &ClientState) -> RenderModel {
|
||||
help: help_rows(&state.view),
|
||||
help_page: state.view.help_page,
|
||||
help_titles: help_titles(&state.view),
|
||||
// An ABSENT buffer is not an empty one: blanking the overlay over a
|
||||
// real value is one Enter from clearing it (improvise-xg1z).
|
||||
editing: state.view.mode.is_editing().then(|| {
|
||||
state
|
||||
.view
|
||||
.buffers
|
||||
.get("edit")
|
||||
.cloned()
|
||||
.unwrap_or_else(|| improvise_protocol::edit_seed(state))
|
||||
}),
|
||||
// The buffer Enter commits, never a second derivation of it: the fold
|
||||
// seeds an absent one (improvise-xg1z, improvise-ktlk).
|
||||
editing: state
|
||||
.view
|
||||
.mode
|
||||
.is_editing()
|
||||
.then(|| improvise_protocol::read_buffer(&state.view, "edit")),
|
||||
minibuffer: state.view.mode.minibuffer().map(|mb| RenderMinibuffer {
|
||||
prompt: mb.prompt.clone(),
|
||||
value: improvise_protocol::read_buffer(&state.view, &mb.buffer_key),
|
||||
@@ -912,10 +909,11 @@ mod tests {
|
||||
client
|
||||
.state_mut()
|
||||
.fold(&Command::ChangeMode(improvise_protocol::AppMode::editing()));
|
||||
assert!(
|
||||
!client.state().view.buffers.contains_key("edit"),
|
||||
"the fixture must really be missing the buffer, or this proves \
|
||||
nothing about the fallback"
|
||||
assert_eq!(
|
||||
client.state().view.buffers.get("edit").map(String::as_str),
|
||||
Some("1200"),
|
||||
"the fold seeds the missing buffer, so the overlay and a commit \
|
||||
read one thing (improvise-ktlk)"
|
||||
);
|
||||
assert_eq!(
|
||||
client.model().rows[0].cells()[0].text,
|
||||
|
||||
@@ -36,12 +36,14 @@ async function anAggregateGrid(page) {
|
||||
test.describe("drill is refused in the browser, not broken", () => {
|
||||
// The honest half: `i`/`a` on an aggregate declines OUT LOUD, because
|
||||
// `edit_or_drill` answers the `CellId::Aggregate` arm with a status.
|
||||
test("editing an aggregate says drill needs the host", async ({ page }) => {
|
||||
test("editing an aggregate says it is edited by drilling, and drill is missing", async ({
|
||||
page,
|
||||
}) => {
|
||||
await anAggregateGrid(page);
|
||||
|
||||
await page.keyboard.press("i");
|
||||
await expect(page.locator("#toast")).toContainText(
|
||||
"drilling into an aggregate needs the host",
|
||||
"an aggregate is edited by drilling in — drill is not available in the browser yet",
|
||||
);
|
||||
// And it really is a refusal: no editor opened, no mode change.
|
||||
await expect(page.locator("#mode")).toHaveText("NORMAL");
|
||||
@@ -63,16 +65,15 @@ test.describe("drill is refused in the browser, not broken", () => {
|
||||
);
|
||||
await expect(page.locator("#mode")).toHaveText("NORMAL");
|
||||
|
||||
// The two refusals have two SUBJECTS, and conflating them would be a
|
||||
// true-sounding sentence about the wrong thing — worse than silence,
|
||||
// because it stops the reader looking. `>` must not talk about aggregates.
|
||||
// `>` is refused whatever the cell is, so it must not blame the cell.
|
||||
await expect(page.locator("#toast")).not.toContainText("aggregate");
|
||||
|
||||
// And `i` still gives the OTHER refusal, which is what proves the two are
|
||||
// distinct rather than one message reached by two keys.
|
||||
// `i` reaches the SAME missing feature (in the TUI it drills), so it names
|
||||
// it the same way and adds only why — improvise-s8h7, clients.md.
|
||||
await page.keyboard.press("i");
|
||||
await expect(page.locator("#toast")).toContainText("an aggregate is edited by drilling in");
|
||||
await expect(page.locator("#toast")).toContainText(
|
||||
"drilling into an aggregate needs the host",
|
||||
"drill is not available in the browser yet",
|
||||
);
|
||||
});
|
||||
});
|
||||
|
||||
+60
-10
@@ -9,6 +9,8 @@ KB="${KB_FILE:-$repo/prolog-sessions/kb.pl}"
|
||||
# Test seam: kb-test.sh injects a pre-fix kb-merge.pl to prove the arithmetic
|
||||
# check catches a merge that drops a clause.
|
||||
MERGE="${KB_MERGE:-$here/kb-merge.pl}"
|
||||
# Exit codes: 0 done, 1 REFUSED (a verdict on the write), 2 usage, 3 the
|
||||
# completeness baseline could not be read, 127 no tpl. Only 1 is a verdict.
|
||||
|
||||
# trealla comes from the dev shell, which direnv puts on PATH. Reaching it
|
||||
# through `nix shell` per invocation cost more than the work it did: this
|
||||
@@ -62,7 +64,39 @@ acquire_lock() {
|
||||
fi
|
||||
sleep 0.1
|
||||
done
|
||||
trap 'rmdir "$KB.lock" 2>/dev/null || true' EXIT
|
||||
trap 'rm -f "${scratch[@]}"; rmdir "$KB.lock" 2>/dev/null || true' EXIT
|
||||
}
|
||||
|
||||
# Every temporary a writing command makes. The candidate lives BESIDE the kb, so
|
||||
# publishing it is a rename(2): a mv from $TMPDIR may cross a device and copy.
|
||||
scratch=()
|
||||
new_cand() {
|
||||
cand="$(mktemp "$KB.cand.XXXXXX")"
|
||||
scratch+=("$cand" "$cand.delta" "$cand.removed" "$cand.ledger" "$cand.base")
|
||||
}
|
||||
|
||||
# What `kb rm` removed that HEAD still has: the record that tells an intended
|
||||
# removal from a lost clause. A fixture's sits beside it; the real one in .git.
|
||||
ledger_path() {
|
||||
if [ -n "${KB_FILE:-}" ]; then echo "$KB.removed"
|
||||
else git -C "$repo" rev-parse --path-format=absolute --git-path kb-removed.pl
|
||||
fi
|
||||
}
|
||||
|
||||
# The committed knowledge base, which no write may end up short of.
|
||||
# KB_BASELINE is the test seam, naming a file.
|
||||
baseline_to() {
|
||||
if [ -n "${KB_BASELINE:-}" ]; then cp -f "$KB_BASELINE" "$1"
|
||||
else git -C "$repo" show HEAD:prolog-sessions/kb.pl > "$1" 2>/dev/null
|
||||
fi
|
||||
}
|
||||
|
||||
# Test seam: SIGKILL once the candidate is complete and checked, before it is
|
||||
# published -- where a killed write dies. Records the candidate's path first.
|
||||
kill_hook() {
|
||||
[ -n "${KB_TEST_KILL:-}" ] || return 0
|
||||
echo "$1" > "$KB_TEST_KILL"
|
||||
kill -9 $$
|
||||
}
|
||||
|
||||
# Test seam: simulate another writer landing between the read and the commit.
|
||||
@@ -83,14 +117,17 @@ usage: kb <command>
|
||||
replace <delta.pl> add clauses, overwriting existing keys
|
||||
rm <keys.pl> remove clauses by key; refuses if any key is absent
|
||||
|
||||
Every writing command verifies the result reads back as the clauses intended
|
||||
and passes kb_consistent before it replaces the knowledge base.
|
||||
Every writing command verifies the result reads back as the clauses intended,
|
||||
still holds every clause HEAD has that no `kb rm` removed, and passes
|
||||
kb_consistent before it replaces the knowledge base.
|
||||
|
||||
Exit: 0 done, 1 refused, 2 usage, 3 HEAD's kb.pl unreadable, 127 no tpl.
|
||||
EOF
|
||||
exit 2
|
||||
}
|
||||
|
||||
commit() { # $1 = candidate file, $2 = stamp of the kb before it was read
|
||||
local cand="$1" was="${2:-}"
|
||||
commit() { # $1 = candidate, $2 = stamp of the kb as read, $3 = keys a rm removes
|
||||
local cand="$1" was="${2:-}" removing="${3:-}" ledger
|
||||
race_hook
|
||||
if [ -n "$was" ] && [ "$(stamp_of "$KB")" != "$was" ]; then
|
||||
rm -f "$cand"
|
||||
@@ -98,11 +135,24 @@ commit() { # $1 = candidate file, $2 = stamp of the kb before it was read
|
||||
echo "kb: another writer won; re-run and your delta applies on top." >&2
|
||||
exit 1
|
||||
fi
|
||||
ledger="$(ledger_path)"
|
||||
if ! baseline_to "$cand.base"; then
|
||||
echo "kb: cannot read the committed kb.pl to compare against; $KB is unchanged" >&2
|
||||
exit 3
|
||||
fi
|
||||
{ if [ -f "$ledger" ]; then cat "$ledger"; fi
|
||||
if [ -n "$removing" ]; then cat "$removing"; fi; } > "$cand.removed"
|
||||
if ! merge complete "$cand.base" "$cand" "$cand.removed" "$cand.ledger"; then
|
||||
echo "kb: REFUSED -- clauses HEAD has are gone, with no kb rm recorded; $KB is unchanged." >&2
|
||||
echo "kb: restore it from HEAD and re-apply your deltas, or commit the removal." >&2
|
||||
exit 1
|
||||
fi
|
||||
if ! check_file "$cand"; then
|
||||
rm -f "$cand"
|
||||
echo "kb: REFUSED -- kb_consistent fails on the result; $KB is unchanged" >&2
|
||||
exit 1
|
||||
fi
|
||||
kill_hook "$cand"
|
||||
mv -f "$cand.ledger" "$ledger"
|
||||
mv -f "$cand" "$KB"
|
||||
}
|
||||
|
||||
@@ -138,7 +188,7 @@ case "$cmd" in
|
||||
fmt)
|
||||
acquire_lock
|
||||
was="$(stamp_of "$KB")"
|
||||
cand="$(mktemp)"
|
||||
new_cand
|
||||
: > "${cand}.delta"
|
||||
if ! merge add "$KB" "${cand}.delta" "$cand" >/dev/null 2>&1; then
|
||||
rm -f "$cand" "${cand}.delta"
|
||||
@@ -153,20 +203,20 @@ case "$cmd" in
|
||||
[ $# -eq 1 ] || usage
|
||||
acquire_lock
|
||||
was="$(stamp_of "$KB")"
|
||||
cand="$(mktemp)"
|
||||
new_cand
|
||||
if ! merge remove "$KB" "$1" "$cand"; then
|
||||
rm -f "$cand"
|
||||
echo "kb: REFUSED -- $KB is unchanged" >&2
|
||||
exit 1
|
||||
fi
|
||||
commit "$cand" "$was"
|
||||
commit "$cand" "$was" "$1"
|
||||
echo "kb: $KB updated"
|
||||
;;
|
||||
add|replace)
|
||||
[ $# -eq 1 ] || usage
|
||||
acquire_lock
|
||||
was="$(stamp_of "$KB")"
|
||||
cand="$(mktemp)"
|
||||
new_cand
|
||||
if ! merge "$cmd" "$KB" "$1" "$cand"; then
|
||||
rm -f "$cand"
|
||||
echo "kb: REFUSED -- $KB is unchanged" >&2
|
||||
|
||||
+36
-1
@@ -10,7 +10,9 @@ main :-
|
||||
-> run(Mode, KbFile, DeltaFile, OutFile)
|
||||
; Argv = [CountStr, KbFile], CountStr == "count"
|
||||
-> count_only(KbFile)
|
||||
; die('usage: kb-merge.pl <add|replace> <kb> <delta> <out> | count <kb>')
|
||||
; Argv = [CS, BaseFile, CandFile, ExcFile, LedgerOut], CS == "complete"
|
||||
-> complete(BaseFile, CandFile, ExcFile, LedgerOut)
|
||||
; die('usage: kb-merge.pl <add|replace|remove> <kb> <delta> <out> | count <kb> | complete <baseline> <candidate> <removed> <ledger-out>')
|
||||
).
|
||||
|
||||
% argv arrives as strings; every later comparison is on an atom.
|
||||
@@ -321,5 +323,38 @@ count_only(KbFile) :-
|
||||
length(Terms, Total),
|
||||
format("total=~w~n", [Total]).
|
||||
|
||||
% Consistency is not completeness: a kb that lost 276 clauses still passed
|
||||
% kb_consistent. Why by key and against HEAD: context/code/kb-tool.md.
|
||||
complete(BaseFile, CandFile, ExcFile, LedgerOut) :-
|
||||
terms_of(BaseFile, Base),
|
||||
terms_of(CandFile, Cand),
|
||||
terms_of(ExcFile, Exc),
|
||||
ground_keys(Cand, CandKeys),
|
||||
ground_keys(Exc, ExcKeys),
|
||||
findall(T, ( member(T, Base), ground_key(T, K),
|
||||
\+ memberchk(K, CandKeys), \+ memberchk(K, ExcKeys) ), Missing),
|
||||
length(Base, NB), length(Cand, NC),
|
||||
( Missing == []
|
||||
-> ground_keys(Base, BaseKeys),
|
||||
findall(E, ( member(E, Exc), ground_key(E, K),
|
||||
memberchk(K, BaseKeys), \+ memberchk(K, CandKeys) ), Kept),
|
||||
write_terms(LedgerOut, Kept),
|
||||
length(Kept, NK),
|
||||
format("kb-merge: complete -- baseline ~w, result ~w, ~w removal(s) recorded~n",
|
||||
[NB, NC, NK])
|
||||
; length(Missing, NM),
|
||||
format("kb-merge: REFUSED -- the baseline has ~w clauses and the result ~w; ~w of the baseline's are missing and no kb rm recorded their removal:~n",
|
||||
[NB, NC, NM]),
|
||||
forall(( nth1(I, Missing, T), I =< 10 ), format(" ~q~n", [T])),
|
||||
( NM > 10 -> Rest is NM - 10, format(" ... and ~w more~n", [Rest]) ; true ),
|
||||
halt(2)
|
||||
).
|
||||
|
||||
ground_key(T, C) :- clause_key([], T, K), canon_key(K, C).
|
||||
|
||||
ground_keys(Terms, Sorted) :-
|
||||
findall(C, ( member(T, Terms), ground_key(T, C) ), Cs),
|
||||
sort(Cs, Sorted).
|
||||
|
||||
die(Msg) :- format("kb-merge: ~w~n", [Msg]), halt(2).
|
||||
die_file(F) :- format("kb-merge: cannot read ~w~n", [F]), halt(2).
|
||||
|
||||
+113
-2
@@ -5,9 +5,15 @@ set -uo pipefail
|
||||
|
||||
here="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
|
||||
repo="$(cd "$here/.." && pwd)"
|
||||
KB="$repo/prolog-sessions/kb.pl"
|
||||
work="$(mktemp -d)"
|
||||
trap 'rm -rf "$work"' EXIT
|
||||
# Fixtures are HEAD's kb.pl, never the working tree's: the tool now measures a
|
||||
# write against HEAD, and the working tree is the thing that can be damaged.
|
||||
KB="$work/head.pl"
|
||||
if ! git -C "$repo" show HEAD:prolog-sessions/kb.pl > "$KB"; then
|
||||
echo "kb-test: cannot read HEAD:prolog-sessions/kb.pl" >&2
|
||||
exit 2
|
||||
fi
|
||||
|
||||
pass=0
|
||||
fail=0
|
||||
@@ -15,7 +21,8 @@ ok() { printf ' ok %s\n' "$1"; pass=$((pass+1)); }
|
||||
bad() { printf ' FAIL %s\n' "$1"; fail=$((fail+1)); }
|
||||
|
||||
# Each case runs against its own copy, so a bug cannot reach the real file.
|
||||
fresh() { cp "$KB" "$work/kb.pl"; }
|
||||
# Also clears the ledger, the lock and any candidate a killed case left behind.
|
||||
fresh() { rm -rf "$work"/kb.pl.*; cp "$KB" "$work/kb.pl"; }
|
||||
kb() { KB_FILE="$work/kb.pl" "$here/kb" "$@"; }
|
||||
unchanged() { diff -q "$KB" "$work/kb.pl" >/dev/null; }
|
||||
# A refusal is only evidence when it is the refusal you NAMED: two of these
|
||||
@@ -500,5 +507,109 @@ else
|
||||
bad "add refused a key holding a variable: the fold matched by unification"
|
||||
fi
|
||||
|
||||
echo "kb-test: completeness against HEAD (improvise-usus)"
|
||||
|
||||
# 18. The incident's shape: clauses gone from the working tree and the rest
|
||||
# still CONSISTENT -- 276 of 801 were lost and kb_consistent passed, so the
|
||||
# add landed. The fixture must keep kb_consistent green, or a different
|
||||
# guard refuses it and the case proves nothing: dropping a whole predicate
|
||||
# is an existence error, and dropping cited clauses fails the citation
|
||||
# check. So it keeps one location/3 fact and drops the other 34. No
|
||||
# KB_BASELINE: this case runs the real `git show HEAD` path, which is also
|
||||
# what a guard counting the file against ITSELF would pass.
|
||||
fresh
|
||||
awk '/^location\(/ { if (seen++) next } { print }' "$KB" > "$work/kb.pl"
|
||||
cp "$work/kb.pl" "$work/lost.pl"
|
||||
if ! KB_FILE="$work/lost.pl" "$here/kb" check >/dev/null 2>&1; then
|
||||
bad "the lossy fixture fails kb_consistent -- case 18 proves nothing"
|
||||
else
|
||||
kb add "$work/new.pl" >"$work/out" 2>&1; rc=$?
|
||||
if [ "$rc" -eq 0 ]; then
|
||||
bad "add wrote onto a kb missing 34 of HEAD's clauses"
|
||||
elif ! cmp -s "$work/kb.pl" "$work/lost.pl"; then
|
||||
bad "the loss was refused but the kb was MODIFIED"
|
||||
elif [ "$rc" -ne 1 ]; then
|
||||
bad "the loss was refused with exit $rc, not the verdict code 1"
|
||||
elif said "$work/out" "34 of the baseline's are missing"; then
|
||||
ok "add refuses a kb that lost clauses HEAD has, and names how many"
|
||||
else
|
||||
bad "the loss was refused, but not BY THE COMPLETENESS GUARD"
|
||||
fi
|
||||
fi
|
||||
|
||||
# 19. The ticket's own fixture: a copy truncated to half its clauses. This one
|
||||
# ALSO breaks kb_consistent, so said() is what makes it evidence -- the
|
||||
# completeness guard runs first and must be the one that answers.
|
||||
fresh
|
||||
head -n "$(( $(wc -l < "$KB") / 2 ))" "$KB" > "$work/kb.pl"
|
||||
cp "$work/kb.pl" "$work/half.pl"
|
||||
if kb add "$work/new.pl" >"$work/out" 2>&1; then
|
||||
bad "add wrote onto a kb truncated to half"
|
||||
elif ! cmp -s "$work/kb.pl" "$work/half.pl"; then
|
||||
bad "the truncation was refused but the kb was MODIFIED"
|
||||
elif said "$work/out" "no kb rm recorded their removal"; then
|
||||
ok "a kb truncated to half is refused by name, byte-identical"
|
||||
else
|
||||
bad "the truncation was refused, but not by the completeness guard"
|
||||
fi
|
||||
|
||||
# 20. rm is how the count legitimately falls, and the ledger is how a LATER
|
||||
# write knows it: rm a clause HEAD has, then add -- the add must land. A
|
||||
# ledger that is never written, or is ignored, refuses here.
|
||||
fresh
|
||||
printf "location(cli_args,'src/main.rs',_).\n" > "$work/drop-head.pl"
|
||||
if ! kb rm "$work/drop-head.pl" >"$work/out" 2>&1; then
|
||||
bad "rm of a clause HEAD has was refused: $(tail -1 "$work/out")"
|
||||
elif kb add "$work/new.pl" >"$work/out" 2>&1; then
|
||||
ok "an add after a recorded rm is accepted"
|
||||
else
|
||||
bad "an add after a legitimate rm was refused: the removal was not recorded"
|
||||
fi
|
||||
|
||||
# 20b. ...and the record excuses exactly what it names. A second, unrecorded
|
||||
# loss on top of a recorded rm must still refuse; a guard that stands down
|
||||
# whenever a ledger exists passes 20 and fails here.
|
||||
sed -i.bak '/^location(add_command,/d' "$work/kb.pl"; rm -f "$work/kb.pl.bak"
|
||||
cp "$work/kb.pl" "$work/twice.pl"
|
||||
printf "doctrine(another_probe_after_the_rm,'x').\n" > "$work/new2.pl"
|
||||
if kb add "$work/new2.pl" >"$work/out" 2>&1; then
|
||||
bad "a recorded rm excused an unrecorded loss beside it"
|
||||
elif cmp -s "$work/kb.pl" "$work/twice.pl" && said "$work/out" "1 of the baseline's are missing"; then
|
||||
ok "a recorded rm excuses only the clause it removed"
|
||||
else
|
||||
bad "the unrecorded loss was refused, but not by name, or the kb changed"
|
||||
fi
|
||||
|
||||
# 21. A usage error, an unreadable baseline and a verdict are three exit codes.
|
||||
# Sharing one is improvise-b4ks: "could not check" reading as "refused".
|
||||
fresh
|
||||
KB_BASELINE="$work/no-such-file.pl" kb add "$work/new.pl" >/dev/null 2>&1; rc3=$?
|
||||
kb add >/dev/null 2>&1; rc2=$?
|
||||
if [ "$rc3" -eq 3 ] && [ "$rc2" -eq 2 ] && unchanged; then
|
||||
ok "an unreadable baseline exits 3 and usage exits 2, neither a verdict"
|
||||
else
|
||||
bad "exit codes: unreadable baseline $rc3 (want 3), usage $rc2 (want 2)"
|
||||
fi
|
||||
|
||||
# 22. A killed write leaves the old kb. The tool SIGKILLs itself once the
|
||||
# candidate is complete and checked, just before publishing it. Two rivals
|
||||
# this separates: writing into the kb in place (the kb changes), and
|
||||
# building the candidate in $TMPDIR, where mv may cross a device and copy
|
||||
# -- so the candidate must be a sibling of the kb, making mv a rename(2).
|
||||
fresh
|
||||
KB_TEST_KILL="$work/killed" kb add "$work/new.pl" >/dev/null 2>&1; rc=$?
|
||||
cand="$(cat "$work/killed" 2>/dev/null)"
|
||||
if [ "$rc" -ne 137 ] || [ -z "$cand" ]; then
|
||||
bad "the kill seam did not fire (exit $rc) -- case 22 proves nothing"
|
||||
elif ! unchanged; then
|
||||
bad "a write killed before publishing MODIFIED the kb"
|
||||
elif [ "$(dirname "$cand")" != "$work" ]; then
|
||||
bad "the candidate was built in $(dirname "$cand"), not beside the kb: mv may copy"
|
||||
elif ! grep -q '^doctrine(a_name_that_is_certainly_not_taken,' "$cand"; then
|
||||
bad "the candidate was not complete when the write died"
|
||||
else
|
||||
ok "a write killed before its rename leaves the old kb byte-identical"
|
||||
fi
|
||||
|
||||
printf '\nkb-test: %d passed, %d failed\n' "$pass" "$fail"
|
||||
[ "$fail" -eq 0 ]
|
||||
|
||||
Reference in New Issue
Block a user