a55b3c7147
scripts/kb add wrote onto a working-tree kb.pl that had lost 276 of its 801 clauses and reported success, because kb_consistent checks consistency, not completeness (improvise-usus). Every write now runs kb-merge.pl `complete` on the candidate before kb_consistent. It refuses unless every clause HEAD has is still present by key, or its removal was recorded by `kb rm` in a per-worktree ledger in the git dir, which prunes itself on every write. The candidate is now built beside kb.pl, so publishing it is a rename(2) rather than a possible cross-device copy that a kill could truncate. Exit codes: 0 done, 1 refused, 2 usage, 3 HEAD's kb.pl unreadable. kb-test.sh now builds its fixtures from HEAD and adds cases 18-22. Argument in context/code/kb-tool.md, evidence and rivals in context/test-evidence/tooling.md. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
160 lines
8.5 KiB
Markdown
160 lines
8.5 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 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.
|
|
|
|
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.
|