Merge pull request #179 from fiddlerwoaroof/fix/kb-guard-followups
CI / Build all bundles (push) Has been cancelled
CI / Test and lint (host) (push) Has been cancelled
CI / wasm32 check (browser bundle crates) (push) Has been cancelled
CI / Browser JS unit tests (node --test) (push) Has been cancelled
CI / Knowledge base consistency (push) Has been cancelled
CI / Lint the harness crate (push) Has been cancelled
CI / Browser harness (OPFS contract + shell) (push) Has been cancelled
CI / Deploy to GitHub Pages (push) Has been cancelled
CI / Build all bundles (push) Has been cancelled
CI / Test and lint (host) (push) Has been cancelled
CI / wasm32 check (browser bundle crates) (push) Has been cancelled
CI / Browser JS unit tests (node --test) (push) Has been cancelled
CI / Knowledge base consistency (push) Has been cancelled
CI / Lint the harness crate (push) Has been cancelled
CI / Browser harness (OPFS contract + shell) (push) Has been cancelled
CI / Deploy to GitHub Pages (push) Has been cancelled
kb: count keys, tie the rm ledger to the file it describes, fix the guard's docs (ih3k, yea8, za97)
This commit is contained in:
@@ -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
|
||||
|
||||
@@ -551,3 +551,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(<fixture id>,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/*`).
|
||||
|
||||
+15
-4
@@ -72,7 +72,7 @@ acquire_lock() {
|
||||
scratch=()
|
||||
new_cand() {
|
||||
cand="$(mktemp "$KB.cand.XXXXXX")"
|
||||
scratch+=("$cand" "$cand.delta" "$cand.removed" "$cand.ledger" "$cand.base")
|
||||
scratch+=("$cand" "$cand.delta" "$cand.removed" "$cand.ledger" "$cand.base" "$cand.stamped")
|
||||
}
|
||||
|
||||
# What `kb rm` removed that HEAD still has: the record that tells an intended
|
||||
@@ -83,6 +83,14 @@ ledger_path() {
|
||||
fi
|
||||
}
|
||||
|
||||
# A ledger speaks only for the kb FILE this tool last published, named on its
|
||||
# first line; bytes alone are not enough, since a restore can reproduce them.
|
||||
file_stamp() {
|
||||
printf '%s %s' "$(stamp_of "$1")" \
|
||||
"$(stat -c '%i %.9Y' "$1" 2>/dev/null || stat -f '%i %Fm' "$1")"
|
||||
}
|
||||
ledger_holds() { [ -f "$1" ] && [ "$(head -n 1 "$1")" = "% kb-stamp $(file_stamp "$2")" ]; }
|
||||
|
||||
# The committed knowledge base, which no write may end up short of.
|
||||
# KB_BASELINE is the test seam, naming a file.
|
||||
baseline_to() {
|
||||
@@ -140,19 +148,22 @@ commit() { # $1 = candidate, $2 = stamp of the kb as read, $3 = keys a rm remove
|
||||
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 ledger_holds "$ledger" "$KB"; 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
|
||||
echo "kb: restore it from HEAD (git show HEAD:prolog-sessions/kb.pl) and re-apply your deltas." >&2
|
||||
echo "kb: do NOT commit this kb.pl: a committed loss becomes the floor this check compares against." >&2
|
||||
echo "kb: to drop a clause on purpose, restore first and then kb rm it." >&2
|
||||
exit 1
|
||||
fi
|
||||
if ! check_file "$cand"; then
|
||||
echo "kb: REFUSED -- kb_consistent fails on the result; $KB is unchanged" >&2
|
||||
exit 1
|
||||
fi
|
||||
{ printf '%% kb-stamp %s\n' "$(file_stamp "$cand")"; cat "$cand.ledger"; } > "$cand.stamped"
|
||||
kill_hook "$cand"
|
||||
mv -f "$cand.ledger" "$ledger"
|
||||
mv -f "$cand.stamped" "$ledger"
|
||||
mv -f "$cand" "$KB"
|
||||
}
|
||||
|
||||
|
||||
+40
-10
@@ -35,8 +35,11 @@ run(remove, KbFile, DeltaFile, OutFile) :-
|
||||
halt(2)
|
||||
),
|
||||
foldl_remove(Funcs, Doomed, Old, Kept),
|
||||
length(Old, NOld), length(Doomed, NDoomed),
|
||||
ExpectK is NOld - NDoomed,
|
||||
length(Old, NOld),
|
||||
findall(x, ( member(O, Old), clause_key(Funcs, O, KO),
|
||||
member(T, Doomed), clause_key(Funcs, T, KT), same_key(KO, KT) ), Hits),
|
||||
length(Hits, NHits),
|
||||
ExpectK is NOld - NHits,
|
||||
check_total(Kept, ExpectK),
|
||||
write_terms(OutFile, Kept),
|
||||
verify(OutFile, Kept),
|
||||
@@ -325,24 +328,27 @@ count_only(KbFile) :-
|
||||
|
||||
% 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.
|
||||
% Keys are counted, not collected: a merge can commit two clauses under one
|
||||
% key, and a set of keys cannot see one of them go (improvise-ih3k).
|
||||
complete(BaseFile, CandFile, ExcFile, LedgerOut) :-
|
||||
terms_of(BaseFile, Base),
|
||||
terms_of(CandFile, Cand),
|
||||
terms_of(ExcFile, Exc),
|
||||
ground_keys(Cand, CandKeys),
|
||||
key_counts(Base, BaseCounts),
|
||||
key_counts(Cand, CandCounts),
|
||||
ground_keys(Exc, ExcKeys),
|
||||
findall(T, ( member(T, Base), ground_key(T, K),
|
||||
\+ memberchk(K, CandKeys), \+ memberchk(K, ExcKeys) ), Missing),
|
||||
findall(K-D, ( member(K-NBK, BaseCounts), count_of(K, CandCounts, NCK),
|
||||
D is NBK - NCK, D > 0 ), Short),
|
||||
findall(K-D, ( member(K-D, Short), \+ memberchk(K, ExcKeys) ), Unexcused),
|
||||
findall(T, ( member(K-_, Unexcused), lost_under(K, Base, Cand, T) ), 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),
|
||||
( Unexcused == []
|
||||
-> findall(E, ( member(E, Exc), ground_key(E, K), memberchk(K-_, Short) ), 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),
|
||||
; foldl(add_deficit, Unexcused, 0, 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])),
|
||||
@@ -356,5 +362,29 @@ ground_keys(Terms, Sorted) :-
|
||||
findall(C, ( member(T, Terms), ground_key(T, C) ), Cs),
|
||||
sort(Cs, Sorted).
|
||||
|
||||
key_counts(Terms, Counts) :-
|
||||
findall(C, ( member(T, Terms), ground_key(T, C) ), Cs),
|
||||
msort(Cs, Sorted),
|
||||
run_lengths(Sorted, Counts).
|
||||
|
||||
run_lengths([], []).
|
||||
run_lengths([K|T], [K-N|Rest]) :-
|
||||
same_run(K, T, 1, N, After),
|
||||
run_lengths(After, Rest).
|
||||
|
||||
same_run(K, [X|T], N0, N, After) :- X == K, !, N1 is N0 + 1, same_run(K, T, N1, N, After).
|
||||
same_run(_, After, N, N, After).
|
||||
|
||||
count_of(K, Counts, N) :- ( memberchk(K-N0, Counts) -> N = N0 ; N = 0 ).
|
||||
|
||||
add_deficit(_-D, N0, N) :- N is N0 + D.
|
||||
|
||||
% What to name for a short key: the baseline's clauses under it that the
|
||||
% result holds no variant of, or the first one when every text survives.
|
||||
lost_under(K, Base, Cand, T) :-
|
||||
findall(B, ( member(B, Base), ground_key(B, KB), KB == K ), Under),
|
||||
findall(B, ( member(B, Under), \+ ( member(C, Cand), same_key(B, C) ) ), Gone),
|
||||
( Gone == [] -> Under = [T|_] ; member(T, Gone) ).
|
||||
|
||||
die(Msg) :- format("kb-merge: ~w~n", [Msg]), halt(2).
|
||||
die_file(F) :- format("kb-merge: cannot read ~w~n", [F]), halt(2).
|
||||
|
||||
+147
-4
@@ -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.
|
||||
@@ -568,13 +579,19 @@ 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"
|
||||
# whenever a ledger exists passes 20 and fails here. The second loss is
|
||||
# made by giving the BASELINE a clause, not by editing the kb: an edit
|
||||
# voids the ledger (case 24), which would test that instead.
|
||||
awk -v x="location(a_probe_only_head_has,'src/nowhere.rs',probe)." '
|
||||
{ line[NR] = $0 } /^location\(/ { last = NR }
|
||||
END { for (i = 1; i <= NR; i++) { print line[i]; if (i == last) print x } }
|
||||
' "$KB" > "$work/head-plus.pl"
|
||||
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
|
||||
if KB_BASELINE="$work/head-plus.pl" 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
|
||||
elif cmp -s "$work/kb.pl" "$work/twice.pl" && said "$work/out" "1 of the baseline's are missing" \
|
||||
&& said "$work/out" "a_probe_only_head_has"; 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"
|
||||
@@ -611,5 +628,131 @@ else
|
||||
ok "a write killed before its rename leaves the old kb byte-identical"
|
||||
fi
|
||||
|
||||
echo "kb-test: what the ledger and the key comparison can be fooled by"
|
||||
|
||||
# 23. Keys compared as a SET cannot see one of two clauses sharing a key
|
||||
# (improvise-ih3k). work_done/3 keys on (id, kind) and is not functional/1,
|
||||
# so a git merge can commit two clauses under one key. Dropping one then
|
||||
# leaves the key present and the loss unseen. The baseline carries the pair.
|
||||
awk -v a="work_done('improvise-zzzz',bug_fix,'first fix, merged from branch A')." \
|
||||
-v b="work_done('improvise-zzzz',bug_fix,'review fix, merged from branch B')." '
|
||||
{ line[NR] = $0 } /^work_done\(/ { last = NR }
|
||||
END { for (i = 1; i <= NR; i++) { print line[i]; if (i == last) { print a; print b } } }
|
||||
' "$KB" > "$work/pair-base.pl"
|
||||
grep -v "^work_done('improvise-zzzz',bug_fix,'review fix" "$work/pair-base.pl" > "$work/pair-lost.pl"
|
||||
pkb() { KB_FILE="$work/kb.pl" KB_BASELINE="$work/pair-base.pl" "$here/kb" "$@"; }
|
||||
fresh
|
||||
if ! KB_FILE="$work/pair-base.pl" "$here/kb" check >/dev/null 2>&1; then
|
||||
bad "the paired baseline fails kb_consistent -- case 23 proves nothing"
|
||||
elif [ "$(grep -c "^work_done('improvise-zzzz'" "$work/pair-lost.pl")" -ne 1 ]; then
|
||||
bad "the lossy fixture does not hold exactly one of the pair -- case 23 proves nothing"
|
||||
else
|
||||
cp "$work/pair-lost.pl" "$work/kb.pl"
|
||||
if pkb add "$work/new.pl" >"$work/out" 2>&1; then
|
||||
bad "add wrote onto a kb that lost one of two clauses sharing a key"
|
||||
elif ! cmp -s "$work/kb.pl" "$work/pair-lost.pl"; then
|
||||
bad "the lost twin was refused but the kb was MODIFIED"
|
||||
elif said "$work/out" "review fix, merged from branch B"; then
|
||||
ok "losing one of two clauses under one key is refused, naming the one lost"
|
||||
else
|
||||
bad "the lost twin was refused, but the refusal does not name it"
|
||||
fi
|
||||
# The pair itself is not a loss: an add onto the intact pair must land, or
|
||||
# the guard has turned "HEAD holds a duplicate" into "nothing may be written".
|
||||
cp "$work/pair-base.pl" "$work/kb.pl"
|
||||
if pkb add "$work/new.pl" >"$work/out" 2>&1; then
|
||||
ok "an add onto a kb that still holds both clauses of a pair is accepted"
|
||||
else
|
||||
bad "the intact pair was refused: $(tail -1 "$work/out")"
|
||||
fi
|
||||
# And the pair has a way out through the tool: rm the key (both go, recorded),
|
||||
# add back the survivor, and a later write must still land.
|
||||
printf "work_done('improvise-zzzz',bug_fix,_).\n" > "$work/pair-key.pl"
|
||||
printf "work_done('improvise-zzzz',bug_fix,'the fix, both halves').\n" > "$work/pair-one.pl"
|
||||
printf "doctrine(a_probe_after_the_pair_is_resolved,'x').\n" > "$work/after-pair.pl"
|
||||
if ! pkb rm "$work/pair-key.pl" >"$work/out" 2>&1; then
|
||||
bad "rm of a key HEAD holds twice was refused: $(tail -1 "$work/out")"
|
||||
elif ! pkb add "$work/pair-one.pl" >"$work/out" 2>&1; then
|
||||
bad "re-adding one clause for a removed pair was refused: $(tail -1 "$work/out")"
|
||||
elif ! pkb add "$work/after-pair.pl" >"$work/out" 2>&1; then
|
||||
bad "a write after resolving the pair was refused: $(tail -1 "$work/out")"
|
||||
else
|
||||
ok "a pair is resolved by rm then add, and later writes still land"
|
||||
fi
|
||||
fi
|
||||
|
||||
# 24. A ledger entry excuses only the kb it was recorded against
|
||||
# (improvise-yea8). rm X, then restore kb.pl the way the refusal message
|
||||
# recommends -- not a write, so nothing prunes -- then lose X some other
|
||||
# way. The ledger entry from the abandoned rm must not excuse that loss.
|
||||
fresh
|
||||
printf "location(cli_args,'src/main.rs',_).\n" > "$work/drop-x.pl"
|
||||
grep -v "^location(cli_args," "$KB" > "$work/lost-x.pl"
|
||||
if ! kb rm "$work/drop-x.pl" >"$work/out" 2>&1; then
|
||||
bad "rm of a clause HEAD has was refused -- case 24 proves nothing"
|
||||
elif [ ! -s "$work/kb.pl.removed" ]; then
|
||||
bad "rm left no ledger -- case 24 proves nothing"
|
||||
else
|
||||
cp "$work/lost-x.pl" "$work/kb.pl"
|
||||
if kb add "$work/new.pl" >"$work/out" 2>&1; then
|
||||
bad "a ledger entry from an abandoned rm excused a later loss of that clause"
|
||||
elif ! cmp -s "$work/kb.pl" "$work/lost-x.pl"; then
|
||||
bad "the stale excuse was refused but the kb was MODIFIED"
|
||||
elif said "$work/out" "location(cli_args,'src/main.rs',clap)"; then
|
||||
ok "a ledger entry does not outlive the kb its rm produced"
|
||||
else
|
||||
bad "the loss was refused, but not by naming the lost clause"
|
||||
fi
|
||||
fi
|
||||
|
||||
# 24b. ...and still excuses it across the tool's own writes: the stamp moves
|
||||
# with each write, so rm then add then add must all land. A ledger stamped
|
||||
# only by rm passes 24 and refuses the second add here.
|
||||
fresh
|
||||
printf "doctrine(a_second_probe_after_the_rm,'x').\n" > "$work/new3.pl"
|
||||
if ! kb rm "$work/drop-x.pl" >"$work/out" 2>&1; then
|
||||
bad "rm refused -- case 24b proves nothing"
|
||||
elif ! kb add "$work/new.pl" >"$work/out" 2>&1; then
|
||||
bad "the first add after an rm was refused: $(tail -1 "$work/out")"
|
||||
elif ! kb add "$work/new3.pl" >"$work/out" 2>&1; then
|
||||
bad "the second add after an rm was refused: the ledger did not follow the write"
|
||||
else
|
||||
ok "a recorded rm stays excused across the tool's later writes"
|
||||
fi
|
||||
|
||||
# 25. The production paths, which every case above bypasses by setting KB_FILE:
|
||||
# the baseline is `git show HEAD` and the ledger is `git rev-parse
|
||||
# --git-path`. Run in a throwaway repo holding a copy of the tool.
|
||||
r="$work/repo"
|
||||
mkdir -p "$r/scripts" "$r/prolog-sessions"
|
||||
cp "$here/kb" "$here/kb-merge.pl" "$r/scripts/"
|
||||
cp "$KB" "$r/prolog-sessions/kb.pl"
|
||||
g() { git -C "$r" -c user.name=kb-test -c user.email=kb-test@invalid "$@"; }
|
||||
rkb() { (unset KB_FILE KB_BASELINE; "$r/scripts/kb" "$@"); }
|
||||
if ! { g init -q && g add -A && g commit -qm base; } >/dev/null 2>&1; then
|
||||
bad "could not build the throwaway repo -- case 25 proves nothing"
|
||||
elif ! rkb rm "$work/drop-x.pl" >"$work/out" 2>&1; then
|
||||
bad "rm in a real repo was refused: $(tail -1 "$work/out")"
|
||||
else
|
||||
ledger="$(g rev-parse --path-format=absolute --git-path kb-removed.pl)"
|
||||
if ! grep -q "^location(cli_args," "$ledger" 2>/dev/null; then
|
||||
bad "rm in a real repo did not record its removal at the git-path ledger"
|
||||
elif [ "$(g status --porcelain --untracked-files=all)" != " M prolog-sessions/kb.pl" ]; then
|
||||
bad "the real-repo write left something git sees: $(g status --porcelain --untracked-files=all | tr '\n' ' ')"
|
||||
elif ! rkb add "$work/new.pl" >"$work/out" 2>&1; then
|
||||
bad "the git-path ledger did not excuse its own rm: $(tail -1 "$work/out")"
|
||||
else
|
||||
g checkout -q -- prolog-sessions/kb.pl
|
||||
cp "$work/lost-x.pl" "$r/prolog-sessions/kb.pl"
|
||||
if rkb add "$work/new.pl" >"$work/out" 2>&1; then
|
||||
bad "after git checkout restored the kb, the git-path ledger excused a new loss"
|
||||
elif said "$work/out" "location(cli_args,'src/main.rs',clap)"; then
|
||||
ok "the git-path ledger and HEAD baseline work, and a loss after a restore is refused"
|
||||
else
|
||||
bad "the real-repo loss was refused, but not by naming it"
|
||||
fi
|
||||
fi
|
||||
fi
|
||||
|
||||
printf '\nkb-test: %d passed, %d failed\n' "$pass" "$fail"
|
||||
[ "$fail" -eq 0 ]
|
||||
|
||||
Reference in New Issue
Block a user