kb: retire the Prolog MCP for a tool that costs the clause, not the predicate
loadProgram REPLACES a whole predicate, so adding one clause meant re-sending every existing clause of it through an agent's context window. Measured on the wave-3 batch: ~113KB read and ~113KB written to deliver ~25KB of new text. That sets the behaviour -- writing becomes a thing you batch and do rarely -- and the batch is where a short payload silently drops the rest of a predicate, which has cost this repo 22 decisions and 19 doctrines once already. scripts/kb reads clauses as DATA and never consults them, so the cost of adding a clause is the clause. Canonical form is read_term in, portray_clause out -- measured, not designed: all 495 existing facts round-trip byte-identically and the form is a fixed point in one pass. Rules move to one line, which is why the reformat lands here rather than earlier: the MCP would re-expand them on its next save and the two would thrash. trealla moves into the devShell. Reaching it through `nix shell` per invocation took the tool's first real use past a two-minute timeout for a write that takes 0.42s with tpl on PATH. Four guards, each added because injecting its fault showed the tool accepting what it should refuse. None was found by reading: - an unparseable delta dropped trealla into its REPL, which HANGS with a terminal and EXITS 0 without one -- a refusal that reads as acceptance - `-g main,halt` exits 0 on a throw AND on a failure, because a goal that fails never reaches the halt beside it; halt(2) alone exits 2, so the default is the hazard. The goal now guarantees a halt on every path (0/2/1) - `42.` parses, is not callable, and landed as a fact whose head is a number; kb_consistent has no opinion about stray terms - fmt discarded the merge's exit code and would have committed a failed canonicalization Plus the two that were designed in: the result is read back and required to be the clauses intended (variant equality -- == compares variable identity and reports every rule as different), and kb_consistent runs on the CANDIDATE, so a bad delta leaves the knowledge base untouched rather than needing a revert. scripts/kb-test.sh proves all nine by injection. context/code/kb-tool.md carries the argument, including what it does not reach. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FC2jVn8Au7E9JPkw6bwXXH
This commit is contained in:
Edward Langley
@@ -0,0 +1,112 @@
|
||||
# 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**. Adding one clause therefore means
|
||||
re-sending every existing clause of that predicate — through an agent's context
|
||||
window, since the tool takes the program as a string. The wave-3 batch measured
|
||||
that cost: about 113 KB read and 113 KB written to deliver roughly 25 KB of new
|
||||
text, for 53 clauses.
|
||||
|
||||
That is not merely expensive. It sets the behaviour: writing becomes something
|
||||
you batch up and do rarely, when what a knowledge base wants is a fact written
|
||||
down at the moment it is learned. The batch is also where the danger lives — a
|
||||
short payload silently drops the rest of the predicate, which has cost this
|
||||
repository 22 decisions and 19 doctrines once already.
|
||||
|
||||
Three further frictions, each of which bit during that batch:
|
||||
|
||||
- **`saveSession` re-adds the MCP's own `host_rpc` shims** on every write.
|
||||
`AGENTS.md` enumerates seven; there are **eight** — `js_eval_json` is missing
|
||||
from that list, so a grep built from it is one case short.
|
||||
- **`saveSession` reserializes the whole file**, so every write risks the
|
||||
formatting as well as the content.
|
||||
- **`assertz` is not an escape hatch.** A consulted predicate is static in this
|
||||
engine and `assertz`/`retract` raise `permission_error(modify,
|
||||
static_procedure)`. A delta of directives was written and verified in a
|
||||
scratch engine before this was discovered; it can never run against a loaded
|
||||
session.
|
||||
|
||||
## 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.
|
||||
|
||||
**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.
|
||||
|
||||
## What no test here reaches
|
||||
|
||||
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.
|
||||
@@ -50,6 +50,12 @@
|
||||
pkgs.universal-ctags
|
||||
beads.packages.${system}.default
|
||||
|
||||
# `scripts/kb` and the CI knowledge-base check both run trealla. It
|
||||
# was reached through `nix shell nixpkgs#trealla` per invocation,
|
||||
# which cost more than the work: the tool's first real use took past
|
||||
# two minutes for a write that takes half a second on PATH.
|
||||
pkgs.trealla
|
||||
|
||||
# `web/build.sh` — and so the Pages job's local dry run — needs this.
|
||||
# The `wasm` CI job only runs `cargo check`, which does not, so the
|
||||
# shell was missing the one tool that turns a passing check into a
|
||||
|
||||
+31
-61
@@ -211,6 +211,7 @@ doctrine(a_premise_guard_is_validated_in_both_directions,'A guard that closes a
|
||||
doctrine(measure_the_property_that_actually_moved,'A measurement that cannot distinguish the two states is not a measurement, and a measurement of the wrong property is not one either, however precise. This repo\'s signature defect is a test that passes while the thing it names is broken, and it arrives through the INSTRUMENT at least as often as through the assertion. Instances. getBoundingClientRect().height reports a height for content-visibility-hidden children, so a nav-collapse probe read 26 visible links in BOTH the collapsed and the expanded state and would have passed the build whose DESKTOP sidebar was collapsed and unusable; checkVisibility({contentVisibilityAuto:true,visibilityProperty:true}) discriminates. Heading text overflows its box without widening it, so getBoundingClientRect reported every element inside the viewport while seven doc-site pages overflowed at phone width -- only per-element scrollWidth names the culprit. A width measured on a display:block label could not see an inline glyph and accused working code. A wall clock absorbed a contaminated tree without a trace where an arithmetic identity would not have. A CI watcher concluded on \"0 checks pending\", which reads identically for \"all finished\" and \"none registered yet\", and so reported a fresh push settled instantly -- a terminal state needs a non-zero total AND the expected head. And the sharpest case is the one where the instrument is sharp and still aimed wrong: a checkbox driving the doc-site\'s collapsed phone nav carried hidden (= display:none), which removes it from the tab order AND the accessibility tree, so at <=900px the navigation was mouse-only, and the probe that \"verified\" that fix counted VISIBLE nav links -- complete for a mouse, silent on whether any non-mouse route exists. Ask what the defect would DO to a user, then pick the instrument that observes that: here tab order, .focus() and the accessibility snapshot, measured on BOTH sides of the media query the regression lives in. The check is the same one applied to a test -- injure the thing being measured and confirm the number moves.').
|
||||
doctrine(an_aged_fact_is_cured_only_by_re_asking,'An instrument failure and an aged fact have no cure in common. Picking a better instrument fixes the first permanently; a fact verified once and believed later can only be re-asked, every time. Worked examples from 2026-09-20: a mergeable status verified in review round 1 and still believed in round 6, through two rounds of CI silence, while the branch sat conflicting; and a knowledge-base clause count taken from a working tree six merges behind, which would have been reported as evidence for a write that deleted three clauses.').
|
||||
doctrine(an_out_of_band_write_desynchronises_the_beads_export,'AGENTS.md says never hand-edit or git checkout .beads/issues.jsonl and attributes the damage to the post-checkout hook. That attribution is INCOMPLETE: resolving a merge conflict on that file with git restore, which fires no hook at all, desynchronises export-state.json identically. The mechanism is ANY out-of-band write, not the hook. The failure is silent in the worst direction -- bd list succeeds and re-exports nothing, git status reads clean, and issues exist in Dolt and nowhere else; three tickets were in that state until an explicit bd export -o reconciled it. The recovery is bd export -o, never bd list. Standing rule: any git operation touching that file is followed by bd export -o.').
|
||||
doctrine(a_goal_runner_exits_zero_unless_halt_is_reached,'trealla -g runs a goal and exits 0 unless halt/1 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 in the conjunction. -g \"halt(2)\" exits 2, so halt itself works -- the DEFAULT is the hazard. Any script driving it must guarantee a halt on every path: (catch(main,E,(write(user_error,E),nl(user_error),halt(2))) -> halt(0) ; halt(1)). What this prevents is not a hang but a SILENT SUCCESS -- an \`if ! tpl ...\` reads a crashed run as a clean one and proceeds -- so it is force_the_failure applied to the runner rather than to the code. Related: an uncaught error otherwise falls back to the REPL, which hangs on a terminal and exits 0 without one, so scripts/kb closes stdin as a backstop.').
|
||||
work_done('improvise-8tk',bug_fix,'ZZ/:wq quit even when the save failed, silently discarding the model. Save now aborts the effect batch on failure; save_to_current_path/1 returns Result<String,String>; three tests in ui/effect.rs.').
|
||||
work_done('improvise-907',bug_fix,'Import wizard step machine redesign: validation_error() gate at ReviewProposals (no-category and over-limit), history-stack previous() bound to Left on every step, and Done made a real confirmation step holding the built workbook. Superseded improvise-gfq, improvise-o1c, improvise-c6j.').
|
||||
work_done('improvise-6sq',wont_do,'Merging EditOrDrill and EnterEditAtCursorCmd into one EnterEdit{mode} is not safe: they differ in WHEN the cell value is read, not in a mode parameter. Added ui/app.rs::tests::i_and_o_diverge_on_an_empty_records_grid as executable evidence.').
|
||||
@@ -339,17 +340,14 @@ session_close(4,'git merge origin/main, bd dolt push, git push').
|
||||
session_close(5,'clean up stashes and pruned branches').
|
||||
session_close(6,'verify committed AND pushed').
|
||||
session_close(7,'hand off context').
|
||||
crate_of_layer(A,B) :-
|
||||
layer(A,B).
|
||||
where(A,B,C) :-
|
||||
location(A,B,C).
|
||||
crate_of_layer(A,B):-layer(A,B).
|
||||
where(A,B,C):-location(A,B,C).
|
||||
concern(ui).
|
||||
concern(io).
|
||||
concern(commands).
|
||||
concern(ratatui).
|
||||
concern(crossterm).
|
||||
may_use(A,B) :-
|
||||
crate(A,C,D),concern(B), \+forbidden(A,B).
|
||||
may_use(A,B):-crate(A,C,D),concern(B), \+forbidden(A,B).
|
||||
crate_depends_on(improvise_core,improvise_formula).
|
||||
crate_depends_on(improvise_io,improvise_core).
|
||||
crate_depends_on(improvise_io,improvise_formula).
|
||||
@@ -364,16 +362,11 @@ crate_depends_on(improvise_protocol,improvise_core).
|
||||
crate_depends_on(improvise_command,improvise_protocol).
|
||||
crate_depends_on(improvise_gp,gp_tree).
|
||||
crate_depends_on(improvise_gp,improvise_formula).
|
||||
depends_transitively(A,B) :-
|
||||
depends_via(A,B,[A]).
|
||||
depends_via(A,B,C) :-
|
||||
crate_depends_on(A,B).
|
||||
depends_via(A,B,C) :-
|
||||
crate_depends_on(A,D), \+memberchk(D,C),depends_via(D,B,[D|C]).
|
||||
illegal_dependency(A,B) :-
|
||||
crate_depends_on(A,B),depends_transitively(B,A).
|
||||
before_fixing(A,B) :-
|
||||
work_done(A,bug_fix,C),doctrine(bug_first,B).
|
||||
depends_transitively(A,B):-depends_via(A,B,[A]).
|
||||
depends_via(A,B,C):-crate_depends_on(A,B).
|
||||
depends_via(A,B,C):-crate_depends_on(A,D), \+memberchk(D,C),depends_via(D,B,[D|C]).
|
||||
illegal_dependency(A,B):-crate_depends_on(A,B),depends_transitively(B,A).
|
||||
before_fixing(A,B):-work_done(A,bug_fix,C),doctrine(bug_first,B).
|
||||
work_unblocked('improvise-8tk','improvise-git','its stated blocker -- a Sequence has no way to stop between steps -- does not hold: abort_effects carries across a flattened Sequence.').
|
||||
work_unblocked('improvise-rml','improvise-dz8','adding Axis::Filter now means filling in one file rather than finding four scattered exhaustive matches').
|
||||
work_unblocked('improvise-rml','improvise-dz8','adding the variant produced exactly ONE compile error outside axis.rs (the persistence writer), because rml had already collapsed the four display matches into one file. Evidence that the consolidation paid for itself.').
|
||||
@@ -389,16 +382,14 @@ catches(uniqueness_test,wrong_variant_prototype).
|
||||
catches(name_roundtrip_test,constructor_builds_other_name).
|
||||
catches(bound_names_test,keymap_references_missing_command).
|
||||
insufficient_for(name_roundtrip_test,wrong_variant_prototype).
|
||||
needs_runtime_check(A) :-
|
||||
variant_named_cmd(A,B).
|
||||
needs_runtime_check(A):-variant_named_cmd(A,B).
|
||||
record_row_identity(wide,coord_group_excluding_measure).
|
||||
record_column(wide,category_col,rename_coordinate,all_cells_in_row).
|
||||
record_column(wide,measure_col,write_cell_value,one_cell).
|
||||
record_column(wide,new_measure_col,create_measure,no_cells).
|
||||
record_edit_path(plain_records).
|
||||
record_edit_path(drill_pending).
|
||||
record_obligation(A,B,C,D) :-
|
||||
record_edit_path(A),record_column(wide,B,C,D).
|
||||
record_obligation(A,B,C,D):-record_edit_path(A),record_column(wide,B,C,D).
|
||||
storage_op(read,'whole document in').
|
||||
storage_op(write,'whole document out').
|
||||
storage_op(list,'enumerate document names in a directory').
|
||||
@@ -461,40 +452,23 @@ functional(kb_issue_found/2).
|
||||
functional(crate/3).
|
||||
functional(wasm_runtime_hazard/3).
|
||||
kb_sentinel(zzz_not_a_real_term).
|
||||
known_crate(A) :-
|
||||
crate(A,B,C).
|
||||
kb_error(layer_names_unknown_crate(A,B)) :-
|
||||
layer(A,B), \+known_crate(B).
|
||||
kb_error(forbidden_names_unknown_crate(A)) :-
|
||||
forbidden(A,B), \+known_crate(A).
|
||||
kb_error(forbidden_names_unknown_concern(A,B)) :-
|
||||
forbidden(A,B), \+concern(B).
|
||||
kb_error(depends_names_unknown_crate(A,B)) :-
|
||||
crate_depends_on(A,B), \+ (known_crate(A),known_crate(B)).
|
||||
kb_error(layering_inverted(A,B)) :-
|
||||
illegal_dependency(A,B).
|
||||
kb_error(rule_too_permissive(may_use/2)) :-
|
||||
kb_sentinel(A),may_use(B,A).
|
||||
kb_error(rule_too_permissive(before_fixing/2)) :-
|
||||
kb_sentinel(A),before_fixing(A,B).
|
||||
kb_error(rule_too_permissive(crate_depends_on/2)) :-
|
||||
kb_sentinel(A),crate_depends_on(A,B).
|
||||
kb_error(conflicting_values(A/2,B)) :-
|
||||
functional(A/2),call(A,B,C),findall(D,call(A,B,D),E),sort(E,F),F=[G,H|I].
|
||||
kb_error(conflicting_values(A/3,B)) :-
|
||||
functional(A/3),call(A,B,C,D),findall(E-F,call(A,B,E,F),G),sort(G,H),H=[I,J|K].
|
||||
kb_error(followup_from_unrecorded_work(A)) :-
|
||||
work_followup(A,B,C), \+work_done(A,D,E).
|
||||
kb_error(unblocked_by_unrecorded_work(A)) :-
|
||||
work_unblocked(A,B,C), \+work_done(A,D,E).
|
||||
kb_error(field_misplaced_in_view_state(A)) :-
|
||||
session_field(A,view_state,B), \+view_state_admits(A).
|
||||
kb_error(field_evicted_without_cause(A)) :-
|
||||
session_field(A,app,B),view_state_admits(A).
|
||||
kb_consistent :-
|
||||
\+kb_error(A).
|
||||
kb_report :-
|
||||
setof(A,kb_error(A),B)->length(B,C),format("kb: ~w problem(s)~n",[C]),forall(member(A,B),format(" - ~w~n",[A]));write('kb: consistent'),nl.
|
||||
known_crate(A):-crate(A,B,C).
|
||||
kb_error(layer_names_unknown_crate(A,B)):-layer(A,B), \+known_crate(B).
|
||||
kb_error(forbidden_names_unknown_crate(A)):-forbidden(A,B), \+known_crate(A).
|
||||
kb_error(forbidden_names_unknown_concern(A,B)):-forbidden(A,B), \+concern(B).
|
||||
kb_error(depends_names_unknown_crate(A,B)):-crate_depends_on(A,B), \+ (known_crate(A),known_crate(B)).
|
||||
kb_error(layering_inverted(A,B)):-illegal_dependency(A,B).
|
||||
kb_error(rule_too_permissive(may_use/2)):-kb_sentinel(A),may_use(B,A).
|
||||
kb_error(rule_too_permissive(before_fixing/2)):-kb_sentinel(A),before_fixing(A,B).
|
||||
kb_error(rule_too_permissive(crate_depends_on/2)):-kb_sentinel(A),crate_depends_on(A,B).
|
||||
kb_error(conflicting_values(A/2,B)):-functional(A/2),call(A,B,C),findall(D,call(A,B,D),E),sort(E,F),F=[G,H|I].
|
||||
kb_error(conflicting_values(A/3,B)):-functional(A/3),call(A,B,C,D),findall(E-F,call(A,B,E,F),G),sort(G,H),H=[I,J|K].
|
||||
kb_error(followup_from_unrecorded_work(A)):-work_followup(A,B,C), \+work_done(A,D,E).
|
||||
kb_error(unblocked_by_unrecorded_work(A)):-work_unblocked(A,B,C), \+work_done(A,D,E).
|
||||
kb_error(field_misplaced_in_view_state(A)):-session_field(A,view_state,B), \+view_state_admits(A).
|
||||
kb_error(field_evicted_without_cause(A)):-session_field(A,app,B),view_state_admits(A).
|
||||
kb_consistent:- \+kb_error(A).
|
||||
kb_report:-setof(A,kb_error(A),B)->length(B,C),format([k,b,:,' ',~,w,' ',p,r,o,b,l,e,m,'(',s,')',~,n],[C]),forall(member(A,B),format([' ',' ',-,' ',~,w,~,n],[A]));write('kb: consistent'),nl.
|
||||
kb_external_check('grep -oE \"^location\\([a-z_]+,\'[^\']+\',\'[^\']+\'\\)\" prolog-sessions/kb.pl # then confirm each file/symbol still exists').
|
||||
portable_origin(improvise_core).
|
||||
portable_origin(improvise_formula).
|
||||
@@ -524,12 +498,9 @@ session_field(drill_state,app,improvise_command).
|
||||
holds_shared_ptr(drill_state).
|
||||
uncommitted_writes(drill_state).
|
||||
half_open_dialog(wizard).
|
||||
portable(A) :-
|
||||
session_field(A,B,C),portable_origin(C), \+holds_shared_ptr(A).
|
||||
snapshot_safe(A) :-
|
||||
session_field(A,B,C), \+uncommitted_writes(A), \+half_open_dialog(A).
|
||||
view_state_admits(A) :-
|
||||
portable(A),snapshot_safe(A).
|
||||
portable(A):-session_field(A,B,C),portable_origin(C), \+holds_shared_ptr(A).
|
||||
snapshot_safe(A):-session_field(A,B,C), \+uncommitted_writes(A), \+half_open_dialog(A).
|
||||
view_state_admits(A):-portable(A),snapshot_safe(A).
|
||||
axis_property(row,navigable).
|
||||
axis_property(column,navigable).
|
||||
axis_property(page,navigable).
|
||||
@@ -557,4 +528,3 @@ opfs_sync(flush).
|
||||
opfs_sync(close).
|
||||
browser_fact(sync_access_handle_safari,'Safari 16.4+ supports createSyncAccessHandle, and all current browsers implement the handle methods synchronously despite an early spec that wrongly called them async. Checked 2026-08-31, so the IndexedDB fallback improvise-i34 called for is not needed.').
|
||||
browser_fact(sync_access_handle_worker_only,'available only in dedicated Web Workers, and exclusive per file entry: a second handle on the same file fails until the first is closed. Hence attach closing what it replaces, and detach existing at all.').
|
||||
|
||||
|
||||
Executable
+101
@@ -0,0 +1,101 @@
|
||||
#!/usr/bin/env bash
|
||||
# The knowledge base's one maintenance tool. Replaces the Prolog MCP cycle:
|
||||
# adding a clause costs the clause, not the whole predicate.
|
||||
set -euo pipefail
|
||||
|
||||
here="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
|
||||
repo="$(cd "$here/.." && pwd)"
|
||||
KB="${KB_FILE:-$repo/prolog-sessions/kb.pl}"
|
||||
MERGE="$here/kb-merge.pl"
|
||||
|
||||
# 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
|
||||
# tool's first real use timed out past two minutes on a half-second write.
|
||||
if ! command -v tpl >/dev/null 2>&1; then
|
||||
echo "kb: tpl is not on PATH -- run inside the dev shell (direnv allow, or nix develop)" >&2
|
||||
exit 127
|
||||
fi
|
||||
|
||||
# stdin is closed on every call: an uncaught Prolog error falls back to the
|
||||
# REPL, which hangs on a terminal and exits 0 without one -- a refusal that
|
||||
# reads as acceptance. kb-merge.pl catches parse errors; this is the backstop.
|
||||
tpl() { command tpl "$@" </dev/null; }
|
||||
|
||||
# The goal that runs kb-merge.pl. `-g main,halt` is NOT enough: measured on
|
||||
# trealla 3.10.3 it exits 0 on a throw and on a failure alike, so a crash reads
|
||||
# as success to `if ! tpl ...`. This propagates both.
|
||||
MERGE_GOAL="(catch(main,E,(write(user_error,E),nl(user_error),halt(2))) -> halt(0) ; halt(1))"
|
||||
merge() { tpl -q "$MERGE" -g "$MERGE_GOAL" -- "$@"; }
|
||||
|
||||
# kb_consistent is the gate CI runs. Anything that writes runs it on the
|
||||
# CANDIDATE, before the candidate becomes the knowledge base.
|
||||
check_file() {
|
||||
tpl "$1" -g "(kb_consistent -> halt(0) ; (kb_report, halt(1)))" 2>/dev/null
|
||||
}
|
||||
|
||||
usage() {
|
||||
cat >&2 <<'EOF'
|
||||
usage: kb <command>
|
||||
|
||||
check run kb_consistent (what CI runs)
|
||||
count clauses per keyed predicate
|
||||
query '<goal>' run a goal against the knowledge base
|
||||
fmt rewrite in canonical form (idempotent)
|
||||
add <delta.pl> add clauses; refuses if any key already exists
|
||||
replace <delta.pl> add clauses, overwriting existing keys
|
||||
|
||||
Every writing command verifies the result reads back as the clauses intended
|
||||
and passes kb_consistent before it replaces the knowledge base.
|
||||
EOF
|
||||
exit 2
|
||||
}
|
||||
|
||||
commit() { # $1 = candidate file
|
||||
local cand="$1"
|
||||
if ! check_file "$cand"; then
|
||||
rm -f "$cand"
|
||||
echo "kb: REFUSED -- kb_consistent fails on the result; $KB is unchanged" >&2
|
||||
exit 1
|
||||
fi
|
||||
mv -f "$cand" "$KB"
|
||||
}
|
||||
|
||||
[ $# -ge 1 ] || usage
|
||||
cmd="$1"; shift
|
||||
|
||||
case "$cmd" in
|
||||
check)
|
||||
if check_file "$KB"; then echo "kb_consistent: TRUE"; else exit 1; fi
|
||||
;;
|
||||
count)
|
||||
merge count "$KB" 2>/dev/null
|
||||
;;
|
||||
query)
|
||||
[ $# -eq 1 ] || usage
|
||||
tpl "$KB" -g "($1 -> halt(0) ; (write('false'), nl, halt(1)))" 2>/dev/null
|
||||
;;
|
||||
fmt)
|
||||
cand="$(mktemp)"
|
||||
: > "${cand}.delta"
|
||||
if ! merge add "$KB" "${cand}.delta" "$cand" >/dev/null 2>&1; then
|
||||
rm -f "$cand" "${cand}.delta"
|
||||
echo "kb: REFUSED -- $KB is unchanged" >&2
|
||||
exit 1
|
||||
fi
|
||||
rm -f "${cand}.delta"
|
||||
commit "$cand"
|
||||
echo "kb: canonicalized"
|
||||
;;
|
||||
add|replace)
|
||||
[ $# -eq 1 ] || usage
|
||||
cand="$(mktemp)"
|
||||
if ! merge "$cmd" "$KB" "$1" "$cand"; then
|
||||
rm -f "$cand"
|
||||
echo "kb: REFUSED -- $KB is unchanged" >&2
|
||||
exit 1
|
||||
fi
|
||||
commit "$cand"
|
||||
echo "kb: $KB updated"
|
||||
;;
|
||||
*) usage ;;
|
||||
esac
|
||||
@@ -0,0 +1,149 @@
|
||||
% Reads the knowledge base and a delta as DATA -- never consults either -- and
|
||||
% writes their merge in canonical form. See context/code/kb-tool.md for why.
|
||||
|
||||
% No initialization/1: scripts/kb supplies a goal that turns a throw into
|
||||
% exit 2 and a failure into exit 1. Measured on trealla 3.10.3, `-g main,halt`
|
||||
% exits 0 for BOTH -- silently reporting a crash as a clean run.
|
||||
main :-
|
||||
current_prolog_flag(argv, Argv),
|
||||
( Argv = [ModeStr, KbFile, DeltaFile, OutFile], mode_atom(ModeStr, Mode)
|
||||
-> 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 arrives as strings; every later comparison is on an atom.
|
||||
mode_atom(S, add) :- S == "add", !.
|
||||
mode_atom(S, replace) :- S == "replace", !.
|
||||
|
||||
run(Mode, KbFile, DeltaFile, OutFile) :-
|
||||
terms_of(KbFile, Old),
|
||||
terms_of(DeltaFile, New),
|
||||
check_callable(New),
|
||||
conflicts(Old, New, Clashes),
|
||||
gate(Mode, Clashes),
|
||||
foldl_merge(New, Mode, Old, Merged),
|
||||
write_terms(OutFile, Merged),
|
||||
verify(OutFile, Merged),
|
||||
length(Old, NO), length(New, NN), length(Merged, NM),
|
||||
format("kb-merge: ~w before, ~w in delta, ~w after~n", [NO, NN, NM]).
|
||||
|
||||
% A term can parse and still not be a clause: `42.` reads fine, is not
|
||||
% callable, and reached the knowledge base as a fact whose head is a number.
|
||||
% Nothing downstream objected -- kb_consistent has no opinion about stray terms.
|
||||
check_callable([]).
|
||||
check_callable([T|Ts]) :-
|
||||
clause_head(T, H),
|
||||
( callable(H)
|
||||
-> check_callable(Ts)
|
||||
; format("kb-merge: REFUSED -- not a clause: ~q~n", [T]),
|
||||
halt(2)
|
||||
).
|
||||
|
||||
clause_head((H :- _), H) :- !.
|
||||
clause_head(H, H).
|
||||
|
||||
% A clause key is the functor plus every argument but the last, so
|
||||
% doctrine(Name,_) keys on Name and decision(Id,Key,_) on the pair. Looser than
|
||||
% functional/1 for crate/3; kb_consistent is the backstop for that.
|
||||
clause_key((H :- _), K) :- !, head_key(H, K).
|
||||
clause_key(H, K) :- head_key(H, K).
|
||||
|
||||
head_key(H, K) :-
|
||||
H =.. [F|Args],
|
||||
( append(Front, [_], Args)
|
||||
-> K =.. [F|Front]
|
||||
; K = F
|
||||
).
|
||||
|
||||
clause_pred((H :- _), F/A) :- !, functor(H, F, A).
|
||||
clause_pred(H, F/A) :- functor(H, F, A).
|
||||
|
||||
conflicts(Old, New, Clashes) :-
|
||||
findall(K,
|
||||
( member(T, New), clause_key(T, K),
|
||||
member(O, Old), clause_key(O, K) ),
|
||||
Clashes).
|
||||
|
||||
gate(add, []) :- !.
|
||||
gate(add, Clashes) :-
|
||||
!,
|
||||
format("kb-merge: REFUSED -- ~w clause(s) already present:~n", [Clashes]),
|
||||
forall(member(K, Clashes), format(" ~q~n", [K])),
|
||||
die('use replace to overwrite an existing clause').
|
||||
gate(replace, _).
|
||||
gate(M, _) :- die(M).
|
||||
|
||||
foldl_merge([], _, Acc, Acc).
|
||||
foldl_merge([T|Ts], Mode, Acc0, Acc) :-
|
||||
clause_key(T, K),
|
||||
exclude(has_key(K), Acc0, Acc1),
|
||||
clause_pred(T, P),
|
||||
insert_after_last(Acc1, P, T, Acc2),
|
||||
foldl_merge(Ts, Mode, Acc2, Acc).
|
||||
|
||||
has_key(K, T) :- clause_key(T, K).
|
||||
|
||||
% Keeps each predicate a contiguous block: a new clause lands after the last
|
||||
% one of its own predicate, or at the end when the predicate is new.
|
||||
insert_after_last([], _, T, [T]).
|
||||
insert_after_last([H|Rest], P, T, Out) :-
|
||||
( clause_pred(H, P), \+ ( member(X, Rest), clause_pred(X, P) )
|
||||
-> Out = [H, T|Rest]
|
||||
; Out = [H|Tail], insert_after_last(Rest, P, T, Tail)
|
||||
).
|
||||
|
||||
terms_of(File, Terms) :-
|
||||
catch(open(File, read, S), _, die_file(File)),
|
||||
read_all(S, Terms),
|
||||
close(S).
|
||||
|
||||
% An uncaught syntax error drops trealla into its REPL, which waits on stdin --
|
||||
% so a malformed delta HANGS with a terminal and exits 0 without one, reading
|
||||
% as acceptance. Catching it is what makes the refusal a refusal.
|
||||
read_all(S, Terms) :-
|
||||
catch(read_term(S, T, []), E, parse_died(E)),
|
||||
( T == end_of_file
|
||||
-> Terms = []
|
||||
; Terms = [T|Rest], read_all(S, Rest)
|
||||
).
|
||||
|
||||
parse_died(E) :-
|
||||
format("kb-merge: REFUSED -- does not parse: ~w~n", [E]),
|
||||
halt(2).
|
||||
|
||||
write_terms(File, Terms) :-
|
||||
open(File, write, S),
|
||||
forall(member(T, Terms), portray_clause(S, T)),
|
||||
close(S).
|
||||
|
||||
% The guard that matters: read the file back and require it to be exactly what
|
||||
% was intended. A serializer bug is the wipe-the-KB failure with a new owner.
|
||||
verify(File, Intended) :-
|
||||
terms_of(File, Written),
|
||||
canon(Written, CW),
|
||||
canon(Intended, CI),
|
||||
( CW == CI
|
||||
-> true
|
||||
; length(Written, NW), length(Intended, NI),
|
||||
format("kb-merge: ROUND-TRIP FAILED -- wrote ~w terms, meant ~w~n", [NW, NI]),
|
||||
die('output does not read back as the intended clauses')
|
||||
).
|
||||
|
||||
% Reading a term back yields FRESH variables, so == compares variable identity
|
||||
% rather than clause content. numbervars over a copy gives variant equality.
|
||||
canon(Terms, Canon) :- copy_term(Terms, Canon), numbervars(Canon, 0, _).
|
||||
|
||||
count_only(KbFile) :-
|
||||
terms_of(KbFile, Terms),
|
||||
forall(member(P, [doctrine/2, invariant/2, decision/3, work_done/3]),
|
||||
( findall(x, ( member(T, Terms), clause_pred(T, P) ), L),
|
||||
length(L, N),
|
||||
P = F/A,
|
||||
format("~w/~w=~w~n", [F, A, N]) )),
|
||||
length(Terms, Total),
|
||||
format("total=~w~n", [Total]).
|
||||
|
||||
die(Msg) :- format("kb-merge: ~w~n", [Msg]), halt(2).
|
||||
die_file(F) :- format("kb-merge: cannot read ~w~n", [F]), halt(2).
|
||||
Executable
+142
@@ -0,0 +1,142 @@
|
||||
#!/usr/bin/env bash
|
||||
# check_the_checker for scripts/kb: every refusal is proved by injecting the
|
||||
# fault it names, and every refusal must leave the knowledge base UNCHANGED.
|
||||
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
|
||||
|
||||
pass=0
|
||||
fail=0
|
||||
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"; }
|
||||
kb() { KB_FILE="$work/kb.pl" "$here/kb" "$@"; }
|
||||
unchanged() { diff -q "$KB" "$work/kb.pl" >/dev/null; }
|
||||
|
||||
echo "kb-test: the refusals"
|
||||
|
||||
# 1. A duplicate key is refused, and nothing is written.
|
||||
fresh
|
||||
cat > "$work/dup.pl" <<'EOF'
|
||||
doctrine(bug_first,'a second, contradicting text for a name that already exists').
|
||||
EOF
|
||||
if kb add "$work/dup.pl" >/dev/null 2>&1; then
|
||||
bad "add accepted a duplicate key"
|
||||
elif unchanged; then
|
||||
ok "add refuses a duplicate key and leaves the kb unchanged"
|
||||
else
|
||||
bad "add refused a duplicate key but MODIFIED the kb"
|
||||
fi
|
||||
|
||||
# 2. replace is the door that duplicate goes through, and it replaces rather
|
||||
# than appending -- a count that grew would be two clauses for one name.
|
||||
fresh
|
||||
before="$(kb count | grep '^doctrine/2=')"
|
||||
if kb replace "$work/dup.pl" >/dev/null 2>&1; then
|
||||
after="$(kb count | grep '^doctrine/2=')"
|
||||
if [ "$before" = "$after" ]; then
|
||||
ok "replace overwrites in place ($after)"
|
||||
else
|
||||
bad "replace changed the clause count: $before -> $after"
|
||||
fi
|
||||
else
|
||||
bad "replace refused a duplicate key"
|
||||
fi
|
||||
|
||||
# 3. A delta that does not parse is refused.
|
||||
fresh
|
||||
printf 'doctrine(broken, unterminated\n' > "$work/bad.pl"
|
||||
if kb add "$work/bad.pl" >/dev/null 2>&1; then
|
||||
bad "add accepted an unparseable delta"
|
||||
elif unchanged; then
|
||||
ok "add refuses an unparseable delta and leaves the kb unchanged"
|
||||
else
|
||||
bad "add refused an unparseable delta but MODIFIED the kb"
|
||||
fi
|
||||
|
||||
# 4. A delta that parses but breaks kb_consistent is refused. This is the one
|
||||
# that matters: the candidate is checked BEFORE it becomes the kb.
|
||||
fresh
|
||||
cat > "$work/illegal.pl" <<'EOF'
|
||||
crate_depends_on(improvise_core,improvise_command).
|
||||
EOF
|
||||
if kb add "$work/illegal.pl" >/dev/null 2>&1; then
|
||||
bad "add accepted a delta that breaks kb_consistent"
|
||||
elif unchanged; then
|
||||
ok "add refuses a kb_consistent violation and leaves the kb unchanged"
|
||||
else
|
||||
bad "add refused a violation but MODIFIED the kb"
|
||||
fi
|
||||
|
||||
# 4b. A delta trealla cannot even take apart must refuse, not crash into a
|
||||
# success. `-g main,halt` exits 0 on a throw, so this is the guard for it.
|
||||
fresh
|
||||
printf '42.\n' > "$work/notaclause.pl"
|
||||
if kb add "$work/notaclause.pl" >/dev/null 2>&1; then
|
||||
bad "add accepted a term that is not a clause"
|
||||
elif unchanged; then
|
||||
ok "add refuses a non-clause term and leaves the kb unchanged"
|
||||
else
|
||||
bad "add refused a non-clause term but MODIFIED the kb"
|
||||
fi
|
||||
|
||||
echo "kb-test: the happy paths"
|
||||
|
||||
# 5. A genuinely new clause lands, and the count moves by exactly one.
|
||||
fresh
|
||||
cat > "$work/new.pl" <<'EOF'
|
||||
doctrine(a_name_that_is_certainly_not_taken,'text for a brand new doctrine').
|
||||
EOF
|
||||
before="$(kb count | grep '^doctrine/2=' | cut -d= -f2)"
|
||||
if kb add "$work/new.pl" >/dev/null 2>&1; then
|
||||
after="$(kb count | grep '^doctrine/2=' | cut -d= -f2)"
|
||||
if [ "$((before + 1))" = "$after" ]; then
|
||||
ok "add lands one new clause ($before -> $after)"
|
||||
else
|
||||
bad "add moved the count wrongly: $before -> $after"
|
||||
fi
|
||||
else
|
||||
bad "add refused a valid new clause"
|
||||
fi
|
||||
|
||||
# 6. The new clause is readable back as itself -- a count can move without the
|
||||
# content being what was asked for.
|
||||
if KB_FILE="$work/kb.pl" "$here/kb" query \
|
||||
"doctrine(a_name_that_is_certainly_not_taken,T), T == 'text for a brand new doctrine'" \
|
||||
>/dev/null 2>&1; then
|
||||
ok "the added clause reads back with the text it was given"
|
||||
else
|
||||
bad "the added clause is not readable back as itself"
|
||||
fi
|
||||
|
||||
# 7. Canonical form is a fixed point: a second fmt changes nothing.
|
||||
fresh
|
||||
kb fmt >/dev/null 2>&1
|
||||
cp "$work/kb.pl" "$work/once.pl"
|
||||
kb fmt >/dev/null 2>&1
|
||||
if diff -q "$work/once.pl" "$work/kb.pl" >/dev/null; then
|
||||
ok "fmt is idempotent"
|
||||
else
|
||||
bad "fmt is not idempotent -- every add would churn the file"
|
||||
fi
|
||||
|
||||
# 8. Canonicalizing loses no clause. A serializer that drops a predicate is the
|
||||
# wipe-the-kb failure, so the count is checked across the reformat.
|
||||
fresh
|
||||
b="$(kb count)"
|
||||
kb fmt >/dev/null 2>&1
|
||||
a="$(kb count)"
|
||||
if [ "$b" = "$a" ]; then
|
||||
ok "fmt preserves every clause count"
|
||||
else
|
||||
bad "fmt changed the counts"
|
||||
fi
|
||||
|
||||
printf '\nkb-test: %d passed, %d failed\n' "$pass" "$fail"
|
||||
[ "$fail" -eq 0 ]
|
||||
Reference in New Issue
Block a user