4ca3a47b41
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
236 lines
13 KiB
Markdown
236 lines
13 KiB
Markdown
# Maintaining the knowledge base
|
|
|
|
`prolog-sessions/kb.pl` is executable knowledge, checked by CI. This is the
|
|
argument for how it is written, and why the Prolog MCP stopped being the way.
|
|
|
|
## Why the MCP was retired
|
|
|
|
`loadProgram` **replaces a whole predicate**, so adding one clause means
|
|
re-sending every existing clause of it through an agent's context window — and a
|
|
short payload silently drops the rest. Three further blockers: `saveSession`
|
|
re-adds the MCP's own `host_rpc` shims and reserializes the whole file, and
|
|
`assertz` raises `permission_error(modify, static_procedure)` against a
|
|
consulted predicate, so there is no incremental route through it at all.
|
|
|
|
## What replaced it
|
|
|
|
`scripts/kb`, a shell entry point over `scripts/kb-merge.pl`.
|
|
|
|
**Clauses are read as DATA, never consulted.** `read_term/3` in a loop yields a
|
|
list of terms; merging is list manipulation; `portray_clause/1` writes them
|
|
back. Nothing is ever asserted, so the static-procedure wall is not reached and
|
|
the cost of adding a clause is the clause.
|
|
|
|
**Canonical form is `read_term` in, `portray_clause` out.** This was not
|
|
designed, it was measured: all 495 facts in the existing file — including every
|
|
escaped quote — round-trip byte-identically, and the form is a fixed point in
|
|
one pass. The only change on first use is that rules move from the MCP's
|
|
two-line layout to one line, which is why the reformat lands with this tool
|
|
rather than before it: the MCP would re-expand them on its next save and the two
|
|
would thrash.
|
|
|
|
**trealla comes from the dev shell.** Reaching it through `nix shell` per
|
|
invocation cost more than the work: the tool's first real use timed out past two
|
|
minutes on a write that takes 0.42 seconds with `tpl` on `PATH`.
|
|
|
|
## The guards, and why each exists
|
|
|
|
Every one of these was added because injecting its fault showed the tool
|
|
accepting something it should refuse. None was found by reading.
|
|
|
|
**The round-trip check.** After writing, the file is read back and required to
|
|
be the clauses intended. A serializer bug is the wipe-the-knowledge-base failure
|
|
with a new owner, and this is the only check that sees it. Note it compares
|
|
*variant* equality via `numbervars` over a copy — reading a term back yields
|
|
fresh variables, so `==` compares variable identity and reports every rule as a
|
|
difference.
|
|
|
|
**`kb_consistent` runs on the CANDIDATE.** The file is replaced only after the
|
|
check passes, so a delta that breaks the knowledge base leaves it untouched
|
|
rather than requiring a revert.
|
|
|
|
**Parse errors are caught explicitly.** An uncaught syntax error drops trealla
|
|
into its REPL, which *hangs* with a terminal and *exits 0* without one — a
|
|
refusal that reads as acceptance. `scripts/kb` also closes stdin on every call
|
|
as a backstop.
|
|
|
|
**Every run reaches a `halt/1`.** `tpl` exits 0 unless a halt is *reached*:
|
|
measured on 3.10.3, `-g "fail"` and `-g "throw(boom)"` both exit 0, and so do
|
|
`fail,halt` and `throw(boom),halt`, because a goal that fails or throws never
|
|
reaches the halt beside it. `halt(2)` alone exits 2, so halt works — the default
|
|
is the hazard. The goal used is therefore
|
|
|
|
```
|
|
(catch(main,E,(write(user_error,E),nl(user_error),halt(2))) -> halt(0) ; halt(1))
|
|
```
|
|
|
|
which gives 0, 2 and 1 for success, throw and failure. Without it, `if ! merge
|
|
...` reads a crashed merge as a clean one and replaces the knowledge base.
|
|
|
|
**Terms must be callable.** `42.` parses, is not a clause, and reached the
|
|
knowledge base as a fact whose head is a number. `kb_consistent` has no opinion
|
|
about stray terms, so nothing objected.
|
|
|
|
**A clause can be retired.** `kb rm` takes keys and refuses if any of them is
|
|
absent, because a typo'd key would otherwise report success and leave the clause
|
|
in place. Without it no correction could ever drop a fact — the first thing it
|
|
was used for was retiring `kb_is_maintained_through_the_mcp`, whose *name* was
|
|
the claim that went false.
|
|
|
|
**Duplicate keys are refused by default.** A key is the functor plus every
|
|
argument but the last, so `doctrine(Name,_)` keys on the name and
|
|
`decision(Id,Key,_)` on the pair. `replace` is the door a correction goes
|
|
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 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 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. 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 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 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"
|
|
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 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
|
|
the merge.
|
|
|
|
A clause name cited *inside another clause's string* is unchecked — dropping or
|
|
renaming a clause silently dangles every clause referring to it
|
|
(`improvise-2f97`).
|
|
|
|
A shebang would let `kb-merge.pl` run directly and collapse the two files into
|
|
one. It does not work on trealla 3.10.3: `#!` is a syntax error that aborts the
|
|
consult, so `main/0` is never defined, and `tpl` wants `-- args` *after* the
|
|
file, which a shebang cannot inject. Worth re-testing if trealla gains script
|
|
support.
|