Edward Langley
87 lines
3.8 KiB
Markdown
87 lines
3.8 KiB
Markdown
---
|
|
name: kb
|
|
description: Read and write the Prolog knowledge base at prolog-sessions/kb.pl. Use when adding a doctrine, invariant, decision or work_done fact, correcting or retiring one, or querying the formal model. Never edit that file by hand and never write it through the Prolog MCP.
|
|
---
|
|
|
|
# Writing the knowledge base
|
|
|
|
`prolog-sessions/kb.pl` is executable knowledge, gated by CI. **`scripts/kb` is
|
|
the only thing that writes it.** `tpl` is assumed on `PATH` from the dev shell.
|
|
|
|
```
|
|
scripts/kb check # kb_consistent, exactly what CI runs
|
|
scripts/kb check --with <d.pl># does the model accept a design you have not built?
|
|
scripts/kb count # clauses per keyed predicate
|
|
scripts/kb query '<goal>' # run a goal; exit 1 if it fails
|
|
scripts/kb add <delta.pl> # add clauses; refuses if a key already exists
|
|
scripts/kb replace <delta.pl> # add, overwriting existing keys
|
|
scripts/kb rm <keys.pl> # remove by key; refuses if a key is absent
|
|
scripts/kb fmt # canonical form (idempotent)
|
|
```
|
|
|
|
A delta is an ordinary Prolog file of clauses. For `rm`, a key is a clause head
|
|
with the last argument left as `_`:
|
|
|
|
```prolog
|
|
doctrine(a_name_that_went_false,_).
|
|
```
|
|
|
|
## Designing against the model
|
|
|
|
Before implementing a ticket, state the design as facts and ask whether the
|
|
model accepts it:
|
|
|
|
```prolog
|
|
crate(improvise_report,'crates/improvise-report','render a View as a report').
|
|
crate_depends_on(improvise_report,improvise_core).
|
|
layer(report,improvise_report).
|
|
```
|
|
|
|
`scripts/kb check --with design.pl` merges those into a throwaway candidate and
|
|
runs `kb_consistent` over the union. Nothing is written either way.
|
|
|
|
It derives consequences you would not enumerate: one wrong dependency edge
|
|
returns six `layering_inverted` violations through the transitive closure. It
|
|
also catches schema mistakes — `layer/2` is `(layer, crate)`, and the wrong
|
|
order comes back as `layer_names_unknown_crate` rather than being accepted.
|
|
|
|
What the model can refuse today: layering and dependency direction
|
|
(`illegal_dependency`, `layering_inverted`, `may_use`), `ViewState` membership
|
|
(`portable`, `snapshot_safe`, `view_state_admits`, `field_misplaced_in_view_state`),
|
|
record obligations, and functional-key conflicts. A design touching those areas
|
|
is worth stating; one that touches none of them will be accepted vacuously, so
|
|
extend the model rather than trusting the green.
|
|
|
|
## Rules
|
|
|
|
**Write a fact when you learn it.** There is no reason to batch.
|
|
|
|
**Verify the claim against the tree before writing it.** A clause stating the
|
|
negation of what the code does is worse than no clause
|
|
(`doctrine(a_stale_gotcha_asserts_the_negation)`).
|
|
|
|
**If the NAME went false, retire it** — `rm` the old key, `add` the new one, and
|
|
say in the new clause that it was renamed. A reader who trusts a name never
|
|
reads the body.
|
|
|
|
**Put the argument in the clause.** Doctrine and decision text is where worked
|
|
examples and history belong; prose docs should stay operational.
|
|
|
|
## Traps
|
|
|
|
- **`assertz` does not work here.** A consulted predicate is static;
|
|
`assertz`/`retract` raise `permission_error(modify, static_procedure)`. This
|
|
is why the tool reads clauses as data.
|
|
- **`kb_consistent` does not check everything.** A clause name cited *inside
|
|
another clause's string* is unchecked, so retiring a clause can dangle every
|
|
clause referring to it (`improvise-2f97`).
|
|
- **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.
|
|
|
|
`context/code/kb-tool.md` has the argument. `scripts/kb-test.sh` proves each
|
|
refusal by injecting the fault it names.
|