kb: refusal no longer offers committing the loss; skill and kb-tool.md describe the guard (improvise-za97)
The kb skill (both copies) now describes the HEAD comparison, the ledger, exit code 3 and the recovery. kb-tool.md records the ih3k/yea8 arguments and corrects the residue paragraph: .gitignore hides the leftovers, and there are six, not one. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
This commit is contained in:
Edward Langley
@@ -78,9 +78,41 @@ examples and history belong; prose docs should stay operational.
|
||||
- **Reading through the MCP is fine.** `loadSession` at session start is still
|
||||
how a session gets the model in hand; only writing moved.
|
||||
|
||||
Every write verifies the result reads back as intended and runs `kb_consistent`
|
||||
on the candidate, so a bad delta leaves the file untouched. `count` before and
|
||||
after is still the cheapest evidence a write did what you meant.
|
||||
Every write checks three things before it replaces the file: the result reads
|
||||
back as intended, it still holds every clause **HEAD** has, and `kb_consistent`
|
||||
passes. So a bad delta leaves the file untouched. `count` before and after is
|
||||
still the cheapest evidence a write did what you meant.
|
||||
|
||||
## When a write is refused
|
||||
|
||||
Exit codes: `0` done, `1` refused, `2` usage, `3` HEAD's `kb.pl` could not be
|
||||
read, so nothing was compared, `127` no `tpl`. Only `1` is a verdict.
|
||||
|
||||
**"clauses HEAD has are gone, with no kb rm recorded"** means the working-tree
|
||||
`kb.pl` is short of the committed one. Your delta did not cause it. The file
|
||||
was already damaged, by a killed write, a bad merge resolution or an edit. The
|
||||
refusal lists the clauses that are missing. The check counts clauses **per
|
||||
key**, so losing one of two clauses that share a key is caught too.
|
||||
|
||||
- **Recover:** `git show HEAD:prolog-sessions/kb.pl > prolog-sessions/kb.pl`,
|
||||
then re-run your `add`/`replace`/`rm` deltas.
|
||||
- **Do not commit the short file to get past the refusal.** HEAD is what the
|
||||
check compares against, so a committed loss becomes the new floor and is
|
||||
never reported again.
|
||||
- **To remove a clause on purpose, use `kb rm`.** It records the removal in a
|
||||
per-worktree ledger (`git rev-parse --git-path kb-removed.pl`, never
|
||||
committed), and that record is what lets later writes accept the missing
|
||||
clause. A hand deletion has no record, so it is refused.
|
||||
|
||||
The ledger vouches only for the exact `kb.pl` file the tool last wrote. Any
|
||||
rewrite outside the tool voids it, including a restore, `git checkout`, `cp`
|
||||
or an editor. After an `rm`, a restore therefore also undoes the `rm`, and you
|
||||
must redo it. That is deliberate. Otherwise the abandoned `rm` would go on
|
||||
excusing a later, accidental loss of the same clause.
|
||||
|
||||
A killed write can leave `kb.pl.cand.*` files and a `kb.pl.lock` directory in
|
||||
`prolog-sessions/`. Git ignores them. The lock makes the next write wait 30
|
||||
seconds and then fail, so delete it if nothing else is writing.
|
||||
|
||||
`context/code/kb-tool.md` has the argument. `scripts/kb-test.sh` proves each
|
||||
refusal by injecting the fault it names.
|
||||
|
||||
@@ -78,9 +78,41 @@ examples and history belong; prose docs should stay operational.
|
||||
- **Reading through the MCP is fine.** `loadSession` at session start is still
|
||||
how a session gets the model in hand; only writing moved.
|
||||
|
||||
Every write verifies the result reads back as intended and runs `kb_consistent`
|
||||
on the candidate, so a bad delta leaves the file untouched. `count` before and
|
||||
after is still the cheapest evidence a write did what you meant.
|
||||
Every write checks three things before it replaces the file: the result reads
|
||||
back as intended, it still holds every clause **HEAD** has, and `kb_consistent`
|
||||
passes. So a bad delta leaves the file untouched. `count` before and after is
|
||||
still the cheapest evidence a write did what you meant.
|
||||
|
||||
## When a write is refused
|
||||
|
||||
Exit codes: `0` done, `1` refused, `2` usage, `3` HEAD's `kb.pl` could not be
|
||||
read, so nothing was compared, `127` no `tpl`. Only `1` is a verdict.
|
||||
|
||||
**"clauses HEAD has are gone, with no kb rm recorded"** means the working-tree
|
||||
`kb.pl` is short of the committed one. Your delta did not cause it. The file
|
||||
was already damaged, by a killed write, a bad merge resolution or an edit. The
|
||||
refusal lists the clauses that are missing. The check counts clauses **per
|
||||
key**, so losing one of two clauses that share a key is caught too.
|
||||
|
||||
- **Recover:** `git show HEAD:prolog-sessions/kb.pl > prolog-sessions/kb.pl`,
|
||||
then re-run your `add`/`replace`/`rm` deltas.
|
||||
- **Do not commit the short file to get past the refusal.** HEAD is what the
|
||||
check compares against, so a committed loss becomes the new floor and is
|
||||
never reported again.
|
||||
- **To remove a clause on purpose, use `kb rm`.** It records the removal in a
|
||||
per-worktree ledger (`git rev-parse --git-path kb-removed.pl`, never
|
||||
committed), and that record is what lets later writes accept the missing
|
||||
clause. A hand deletion has no record, so it is refused.
|
||||
|
||||
The ledger vouches only for the exact `kb.pl` file the tool last wrote. Any
|
||||
rewrite outside the tool voids it, including a restore, `git checkout`, `cp`
|
||||
or an editor. After an `rm`, a restore therefore also undoes the `rm`, and you
|
||||
must redo it. That is deliberate. Otherwise the abandoned `rm` would go on
|
||||
excusing a later, accidental loss of the same clause.
|
||||
|
||||
A killed write can leave `kb.pl.cand.*` files and a `kb.pl.lock` directory in
|
||||
`prolog-sessions/`. Git ignores them. The lock makes the next write wait 30
|
||||
seconds and then fail, so delete it if nothing else is writing.
|
||||
|
||||
`context/code/kb-tool.md` has the argument. `scripts/kb-test.sh` proves each
|
||||
refusal by injecting the fault it names.
|
||||
|
||||
+93
-17
@@ -99,34 +99,98 @@ 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
|
||||
It compares keys rather than totals, although the ticket asked for a count,
|
||||
because a total 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.
|
||||
|
||||
**Keys are counted, not collected** (improvise-ih3k). The guard first compared
|
||||
the *set* of keys, and a set cannot see one of two clauses sharing a key.
|
||||
`work_done/3`, `decision/3` and `work_followup/3` key on two arguments and are
|
||||
not `functional/1`, so `kb_consistent` accepts two clauses under one key. `kb
|
||||
add` refuses to *write* such a pair, but a git merge is not a `kb add`: two
|
||||
branches that each record `work_done(T, bug_fix, …)` conflict at the end of the
|
||||
block, and keep-both is the natural resolution. Once HEAD holds a pair, losing
|
||||
either clause left the key present and the write was accepted, with both totals
|
||||
printed equal. So the guard counts clauses per key, and a key is short when the
|
||||
result holds fewer than HEAD does. The refusal names the HEAD clauses the result
|
||||
holds no copy of, which is the one that went.
|
||||
|
||||
Two alternatives were rejected. Comparing whole clauses would refuse every
|
||||
`replace`, whose purpose is to change the text under a key. Making the three
|
||||
predicates functional would refuse the pair itself at `kb_consistent`. That
|
||||
would force a merge to resolve it, and may be worth doing, but it is a change to
|
||||
the gate in `kb.pl`, not to this tool. `functional/1` also keys an arity-3
|
||||
predicate on its first argument, which is wrong for `decision/3`, so it would
|
||||
need a new two-argument form. And the tool must not lose a clause whatever the
|
||||
gate allows, so counting is needed either way.
|
||||
|
||||
A pair also had no way out through the tool. `rm` checked its result against
|
||||
`before - clauses in the delta`, which assumes one clause per key, so removing a
|
||||
paired key was refused as "a clause was dropped". The expected total is now
|
||||
`before - clauses the delta's keys match`, which is still counted separately
|
||||
from the fold that removes them. `replace` of a paired key is still refused by
|
||||
its total. That is the right answer, because it would silently collapse two
|
||||
clauses into one. The route for a pair is `kb rm` the key, then `kb add` the one
|
||||
clause to keep.
|
||||
|
||||
**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
|
||||
writes read: a key the result is short of is excused only if the ledger names
|
||||
it. 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:
|
||||
`KB_FILE` set it sits beside that file. Every write rewrites it, keeping only
|
||||
the keys the result is still short of, so an entry drops once the removal is
|
||||
committed and once the key is back to HEAD's count. 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.
|
||||
is deliberately no override flag.
|
||||
|
||||
The way out of a refusal is to restore `kb.pl` from HEAD and re-apply your
|
||||
deltas. Do **not** commit the short `kb.pl` to get past it. The refusal
|
||||
message used to offer that, and taken on a loss nobody intended it makes the
|
||||
loss permanent: the committed file becomes the floor this guard compares
|
||||
against, and nothing ever reports it again. A removal you intend goes through
|
||||
`kb rm`, onto a restored file.
|
||||
|
||||
**A ledger speaks only for the file its write published** (improvise-yea8).
|
||||
Pruning happens only when the tool writes. A commit, a `git checkout --
|
||||
prolog-sessions/kb.pl`, a `cp`, and a branch switch are not writes. So an
|
||||
entry from an `rm` that was later abandoned would excuse a later loss of that
|
||||
same clause by any path. That is easy to reach, because the recommended
|
||||
recovery is exactly a restore. Pruning against the kb read at the next write
|
||||
cannot close it, because that kb has already lost the clause. So the ledger's
|
||||
first line is a `% kb-stamp` comment naming the kb file the write published,
|
||||
and a later write reads the entries only if the kb it finds is still that file.
|
||||
|
||||
The stamp is the content hash **and** the file's inode and nanosecond mtime.
|
||||
Content alone is not enough, and the test that showed it was the ticket's own
|
||||
reproduction. `kb.pl` is kept in canonical form, so `grep -v` of one clause
|
||||
from HEAD produces output **byte-identical** to what `kb rm` of that clause
|
||||
writes. After `rm X`, a restore, and then the same loss by hand, a content-only
|
||||
stamp still matched. `rename(2)` carries the candidate's inode and mtime onto
|
||||
`kb.pl`. Anything else that rewrites the file, whether a `cp` onto it, a git
|
||||
checkout or an editor, gives a new mtime and usually a new inode. `stat -c` is
|
||||
tried before `stat -f` because GNU `stat -f` means *filesystem* status and
|
||||
would silently stamp the wrong thing. It is not keyed by HEAD commit, because a
|
||||
commit that does not touch `kb.pl` does not make the ledger wrong. And an
|
||||
uncommitted `rm` carried across a branch switch, with `kb.pl` untouched, is
|
||||
still exactly the kb it describes.
|
||||
|
||||
The cost is a false refusal after an intended `rm` followed by anything that
|
||||
rewrites the file without the tool. That refusal is loud, and the recovery is
|
||||
the usual one: restore and redo the `rm`.
|
||||
|
||||
**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.
|
||||
renamed first. A kill between the two renames leaves a ledger stamped for a
|
||||
candidate that was never published. It therefore matches nothing, and the next
|
||||
write ignores it. That can refuse a write an earlier `rm` should have excused.
|
||||
It cannot excuse a loss, which was the hole before the stamp.
|
||||
|
||||
**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"
|
||||
@@ -139,10 +203,22 @@ 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.
|
||||
A `SIGKILL` leaves six files behind, because no trap runs: the candidate
|
||||
`kb.pl.cand.XXXXXX`, its `.base`, `.ledger`, `.removed` and `.stamped`
|
||||
siblings, and the `kb.pl.lock` directory. None of them is ever read again,
|
||||
and **git does not see them**. `.gitignore` ignores `prolog-sessions/*`, so
|
||||
neither `git status --untracked-files=all` nor `git add -A` lists them. That
|
||||
was measured, and an earlier version of this paragraph warned about `git add
|
||||
-A` staging them, which does not happen. The one that matters is the lock: the
|
||||
next write waits 30 seconds for it and then exits 1 with "remove it if stale".
|
||||
Delete it and the candidates by hand.
|
||||
|
||||
The ledger's stamp names a file by inode and nanosecond mtime. A rewrite that
|
||||
preserves both, such as a `touch -r`, a filesystem with coarse timestamps
|
||||
rewriting within one tick, or an inode reused at the same mtime, with the bytes
|
||||
also identical to what the tool published, is indistinguishable from the file
|
||||
the tool wrote. That takes deliberate effort or a filesystem this repository
|
||||
does not run on.
|
||||
|
||||
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
|
||||
|
||||
@@ -486,3 +486,62 @@ 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).
|
||||
|
||||
### The kb completeness guard's follow-ups — `scripts/kb-test.sh` cases 19b, 20b, 23–25
|
||||
|
||||
improvise-ih3k, improvise-yea8 and improvise-za97, filed by the review of PR
|
||||
#166. The argument is in `context/code/kb-tool.md`. This entry covers what each
|
||||
case was watched to catch.
|
||||
|
||||
**Reproduced at `f909cad` before any fix.** The new cases 23, 23c and 24 gave
|
||||
40 passed, 3 failed. 23 failed because an add onto a kb that had lost one of
|
||||
two `work_done('improvise-zzzz',bug_fix,…)` clauses exited 0. 23c failed
|
||||
because `rm` of that paired key was refused as "a clause was dropped": its
|
||||
expected total assumed one clause per key. The tickets did not predict that
|
||||
one, and it meant a pair could not be resolved through the tool at all. 24
|
||||
failed because the stale ledger entry excused the loss.
|
||||
|
||||
**The ticket's own reproduction defeats a content stamp.** The first fix
|
||||
stamped the ledger with the kb's sha256, and case 24 still failed. `kb.pl` is
|
||||
canonical, so `grep -v` of one clause from HEAD is byte-identical to what `kb
|
||||
rm` of that clause writes. The stamp therefore also carries the inode and the
|
||||
nanosecond mtime.
|
||||
|
||||
**Case 20b had to change, and why that is not a weakening.** It made its
|
||||
second loss with `sed -i` on the kb. Under the fix, any edit outside the tool
|
||||
voids the ledger, so 20b then refused two clauses instead of one and failed on
|
||||
its "1 of" assertion. It was testing the new voiding rather than what its
|
||||
comment names. The second loss now comes from giving the *baseline* an extra
|
||||
clause (`KB_BASELINE`). The kb file stays exactly as the tool wrote it, the
|
||||
ledger stays valid, and the case again isolates "excuses only what it names".
|
||||
It also now asserts the unexcused clause is named.
|
||||
|
||||
**Rivals injected, one at a time. Each failed only the cases listed:**
|
||||
|
||||
- keys compared as a set (`min(1, N)` per key) in `complete`: 23 only.
|
||||
- `rm`'s expected total back to `before - |delta|`: 23c's rm step only.
|
||||
- ledger pruned by key presence rather than count: 23c's final write only.
|
||||
- ledger honoured whenever it exists: 24 and 25.
|
||||
- ledger stamped by content alone: 24 only. 25 cannot see it, because its
|
||||
intervening `add` makes the restored-then-lost file differ in content
|
||||
anyway. 24 is the case that carries identity.
|
||||
- ledger re-stamped only by `rm`, keeping the old stamp on other writes: 24b
|
||||
(as named), 20b and 23c. All three write again after an add.
|
||||
- ledger stamped with the kb as read rather than the candidate: 20, 20b, 23c,
|
||||
24b and 25. That is wider than any one case, as expected, since no later
|
||||
write can ever match.
|
||||
- the `gh/main` `scripts/kb` (old refusal text, no stamp): 19b, 24 and 25.
|
||||
|
||||
**Case 25 is the first to run the production paths.** Every other case sets
|
||||
`KB_FILE`, so `ledger_path`'s `git rev-parse --git-path` branch and
|
||||
`baseline_to`'s `git show HEAD` were unexercised. It copies the tool into a
|
||||
throwaway `git init` repo and checks four things. `rm` records to the git-path
|
||||
ledger. `git status` shows only `kb.pl` modified, so the ledger is invisible
|
||||
to git. A later `add` is excused. After `git checkout --` and a hand loss, the
|
||||
`add` is refused.
|
||||
|
||||
**Checked by hand, not in the suite:** a `SIGKILL` at the publish point (the
|
||||
`KB_TEST_KILL` seam) on a copy inside `prolog-sessions/` leaves the candidate,
|
||||
its `.base`, `.ledger`, `.removed` and `.stamped` siblings and `.lock`. `git
|
||||
status --untracked-files=all` and `git add -A --dry-run` both show none of
|
||||
them, and `git check-ignore -v` names `.gitignore:40` (`prolog-sessions/*`).
|
||||
|
||||
@@ -553,6 +553,17 @@ else
|
||||
bad "the truncation was refused, but not by the completeness guard"
|
||||
fi
|
||||
|
||||
# 19b. ...and the refusal must not offer committing the loss as the way out:
|
||||
# a committed loss becomes the floor, and is never reported again
|
||||
# (improvise-za97).
|
||||
if said "$work/out" "commit the removal"; then
|
||||
bad "the refusal still offers committing an unexplained loss"
|
||||
elif said "$work/out" "do NOT commit"; then
|
||||
ok "the refusal warns against committing the loss"
|
||||
else
|
||||
bad "the refusal says nothing about committing the short kb"
|
||||
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.
|
||||
|
||||
Reference in New Issue
Block a user