Merge pull request #68 from fiddlerwoaroof/kb/tool
kb: a knowledge base you can write to cheaply, and design against
This commit is contained in:
Ed Langley
GitHub
@@ -38,6 +38,7 @@
|
||||
{"_type":"issue","id":"improvise-km8","title":"1.2 Fix Cargo.toml metadata","description":"Add missing package fields: description, repository, homepage, documentation, readme, keywords, categories, license. Description: 'Terminal pivot-table modeling in the spirit of Lotus Improv'. Keywords: tui, pivot, spreadsheet, data, improv. Categories: command-line-utilities, visualization.","status":"closed","priority":1,"issue_type":"task","assignee":"Edward Langley","owner":"el-github@elangley.org","created_at":"2026-04-09T04:06:48Z","created_by":"Edward Langley","updated_at":"2026-07-30T23:06:31Z","closed_at":"2026-04-09T07:20:17Z","close_reason":"Metadata already present: description, license, repository, homepage, readme, keywords, categories all populated.","dependency_count":0,"dependent_count":2,"comment_count":0}
|
||||
{"_type":"issue","id":"improvise-902","title":"1.1 Audit and remove or update context/SPEC.md","description":"Compare context/SPEC.md against actual code. If spec contradicts code significantly, delete it. Optionally move salvageable conceptual content to docs/design-notes.md with a staleness disclaimer. Do not try to bring spec into sync.","status":"closed","priority":1,"issue_type":"task","assignee":"Edward Langley","owner":"el-github@elangley.org","created_at":"2026-04-09T04:06:46Z","created_by":"Edward Langley","updated_at":"2026-07-30T23:06:31Z","closed_at":"2026-04-09T07:10:05Z","close_reason":"Audited SPEC.md against code. Found minor inaccuracies (storage internals, wizard step count, search mode representation) but no major architectural contradictions. Deleted SPEC.md since it was largely redundant with repo-map.md and design-principles.md. Salvaged product vision and non-goals into docs/design-notes.md with staleness disclaimer.","dependency_count":0,"dependent_count":1,"comment_count":0}
|
||||
{"_type":"issue","id":"improvise-tik","title":"Phase 1: Repository hygiene","description":"Raise the quality floor of what a stranger sees when they land on the repo. Subtasks cover spec audit, Cargo.toml metadata, publish-readiness, CSV audit, and example files.","status":"closed","priority":1,"issue_type":"feature","owner":"el-github@elangley.org","created_at":"2026-04-09T04:05:45Z","created_by":"Edward Langley","updated_at":"2026-04-09T07:22:34Z","closed_at":"2026-04-09T07:22:34Z","close_reason":"All 5 subtasks complete: SPEC.md audited, Cargo.toml metadata fixed, publish dry-run clean, CSV audit done, example files created.","dependencies":[{"issue_id":"improvise-tik","depends_on_id":"improvise-2fr","type":"blocks","created_at":"2026-04-08T23:37:31Z","created_by":"Edward Langley","metadata":"{}"},{"issue_id":"improvise-tik","depends_on_id":"improvise-902","type":"blocks","created_at":"2026-04-08T23:37:30Z","created_by":"Edward Langley","metadata":"{}"},{"issue_id":"improvise-tik","depends_on_id":"improvise-bv1","type":"blocks","created_at":"2026-04-08T23:37:32Z","created_by":"Edward Langley","metadata":"{}"},{"issue_id":"improvise-tik","depends_on_id":"improvise-km8","type":"blocks","created_at":"2026-04-08T23:37:30Z","created_by":"Edward Langley","metadata":"{}"},{"issue_id":"improvise-tik","depends_on_id":"improvise-n1h","type":"blocks","created_at":"2026-04-08T23:37:32Z","created_by":"Edward Langley","metadata":"{}"}],"dependency_count":5,"dependent_count":0,"comment_count":0}
|
||||
{"_type":"issue","id":"improvise-xfsb","title":"Agents should post to GitHub under their own identity, not the owner's","description":"Today every agent comment, review and PR goes out as @fiddlerwoaroof, because gh uses his credentials. The interim is a convention -- open each comment with a line saying a model wrote it (doctrine(an_agent_posting_to_github_says_so), AGENTS.md) -- and a convention is something an agent can forget. A separate identity makes attribution structural instead.\n\nTwo routes:\n\n1. GitHub App installed on the repo. Agents mint an installation token and export GH_TOKEN. Comments render as \u003cname\u003e[bot], the same shape as copilot-pull-request-reviewer[bot]. Scoped permissions, no seat consumed, revocable independently of the owner's account, and the bot suffix is not spoofable by a human account.\n\n2. Machine user with its own PAT as GH_TOKEN. Simpler to set up, consumes a seat on some plans, and is indistinguishable from a person at a glance -- which is most of what we are trying to fix.\n\nPrefer 1. Needs the user: create the App, grant contents+pull_requests+issues write, install it, and put the app id and private key where agents can reach them.\n\nWorth checking while doing it: whether the bot can be requested as a PR reviewer, which would let review agents post as reviews rather than as comments.\n\nOnce it lands, the attribution line becomes belt-and-braces rather than the mechanism, and the doctrine should be amended to say so rather than deleted -- a reader seeing an unattributed comment from the owner's account still needs to know it might be an agent.","status":"open","priority":2,"issue_type":"task","owner":"el-github@elangley.org","created_at":"2026-09-20T23:04:19Z","created_by":"orchestrator","updated_at":"2026-09-20T23:04:19Z","dependency_count":0,"dependent_count":0,"comment_count":0}
|
||||
{"_type":"issue","id":"improvise-84wp","title":"Doctrine: a check that looks like the answer, answering a neighbouring question","description":"Ready-to-apply prose for `context/design-principles.md` §7. Filed rather than committed because PR #60 head `ec03f95` is byte-identical (tree `ec5d531...`) to a tree the reviewer fully tested, and a further commit would destroy that property and require a fresh harness run while `main` was moving several times an hour. The artefact is worth more preserved than rushed.\n\n---\n\n### A check that looks like the answer, answering a neighbouring question\n\nThe characteristic defect in this repo is not a wrong line; it is a check that is *adjacent* to the thing it names. Three instances landed in one campaign (PRs #59/#60), in three different layers, which is why it is worth stating as a shape rather than three gotchas:\n\n- **A vacuous assertion.** `set_panel_open_and_cursor` asserted `category_panel_open` was true after an effect set it true -- once the launch default supplied `true`, the effect could be replaced by a **no-op** and 1391 tests passed. It answered *is the flag true* where it meant *did the effect set it*.\n- **A vacuous repair of it.** The first fix folded `[open:false, open:true]` and asserted the final state -- which a reducer that folds nothing also satisfies. It answered *does the text mention the other direction* where it meant *does the writer move the flag both ways*. **Reading the diff is what failed**, and it failed because the vacuous version contained `open: false`.\n- **A clean auto-merge.** `git merge-tree` reporting no conflict answers *can git combine these texts*, where the question is *does the combination do what both sides meant*. Two PRs edited the same four files with no conflict and neither side CI-tested together.\n\nEach has the same remedy shape: **name the question you actually mean, then find an input that separates it from its neighbour.**\n\n- For an assertion: **assert the direction the default cannot supply.** Closing the panel discriminates; opening it proves nothing.\n- For a repair: inject a **one-directional** fault (`if open { set true }` -- can raise, never lower). A vacuous repair cannot see it, because a test that only asserts the `true` direction is satisfied by a writer that only ever writes `true`.\n- For a merge: **materialise it and run the gates**, and check that a count which should MOVE actually moved. Playwright going 16 -\u003e 17 is what showed the other side survived; \"no conflict\" and an unchanged total would both have been consistent with losing it.\n\nThis generalises the existing `doctrine(fold_tests_must_test_order_not_the_axiom)` (asserting `fold(prefix)+fold(rest) == fold(whole)` is the definition of a left fold, so it answers a neighbouring question too). What the campaign adds is that the pattern recurs in **test repairs** and in **merge hygiene**, not only in production code and not only in fold tests.\n\n---\n\nAcceptance: the section is in §7; `doctrine(fold_tests_must_test_order_not_the_axiom)` cross-references it or is subsumed by it. Worth considering a `kb.pl` doctrine clause, which is orchestrator-only.\n","status":"open","priority":2,"issue_type":"task","owner":"el-github@elangley.org","created_at":"2026-09-20T21:38:23Z","created_by":"wave3-webui","updated_at":"2026-09-20T21:38:23Z","dependency_count":0,"dependent_count":0,"comment_count":0}
|
||||
{"_type":"issue","id":"improvise-qsmp","title":"App::cmd_context's panel-open propagator is untested: C cannot open a closed panel and nothing fails","description":"`App::cmd_context` (crates/improvise-command/src/ui/app.rs) propagates `self.view_state.category_panel_open` into the `CmdContext`. **Hardcode it to `true` and the entire workspace passes** — 1394 tests, nothing fails.\n\nThat matters because `registry.rs` reads it in three places for `toggle-panel-and-focus`s open-vs-close decision and the panel focus/cycle commands. With it stuck true, pressing `C` on a CLOSED category panel decides to *close* it rather than open it — the panel becomes unopenable by its own key — and no test notices.\n\n**Why it is invisible:** `cmd/mod.rs`s `test_helpers` sets `category_panel_open` explicitly on the context it builds, so no command test ever exercises the real propagator. The tests construct the value they then assert on.\n\n**This is PRE-EXISTING and was not caused by the launch-default ruling (PR #60).** That distinction was established by control rather than assumed: with the default inverted, this mutation fails *exactly the same two tests as inverting the default alone* and nothing more. So it was unguarded before the ruling too. The remedy is therefore \"a test at all\", not the precondition-stating fixture that fixed the two genuinely-disarmed tests (`set_panel_open_and_cursor`, `panel_commands_address_the_named_panel_only`).\n\n**The method that found it is worth more than the finding** and is written up in `context/test-evidence/clients.md` under \"How to know a launch default has stopped disarming things\": mutate every site that writes, propagates or reads the value; sites where nothing fails are suspects; then re-run each suspect with the default inverted to separate *vacuous* (fix the fixture) from *unguarded* (file it). Grep cannot do this — it finds sites that NAME the flag, not tests that merely start from a default-built state.\n\nAcceptance: a command-layer test that drives the real `App::cmd_context` rather than a hand-built context, such that `toggle-panel-and-focus` on a closed panel opens it; proved by hardcoding the propagator and watching it fail.\n\nSibling note: `improvise-wasm-client/src/render.rs` has the same propagator shape for `RenderModel`. Hardcoding THAT one true is improvise-wsaw reintroduced one layer up, and Rust sees nothing — only the Chromium harness catches it, at `contract.spec.js`s `toBeHidden`. Consequence worth keeping: a Rust-only run of the `test` CI job cannot see a reintroduced wsaw, which is the sharpest argument on file for the browser job being able to fail the build.\n","status":"open","priority":2,"issue_type":"bug","owner":"el-github@elangley.org","created_at":"2026-09-20T21:23:53Z","created_by":"wave3-webui","updated_at":"2026-09-20T21:23:53Z","dependency_count":0,"dependent_count":0,"comment_count":0}
|
||||
{"_type":"issue","id":"improvise-5ray","title":"check-evidence ignores #### headings and every browser-test entry uses them","description":"Found by review of PR #65, 2026-09-20 (finding 4). Sibling of improvise-lyyc\nand improvise-r0qa, and the sharpest of the three because this one has already\nlet a false claim stand for a release.\n\nscripts/check-comment-runs.py --check-evidence collects headings with\n`s.startswith(\"### \")` and builds its `defined` set from rust_files(roots) only.\nTwo consequences compound:\n\n 1. A `####` heading is invisible to it — `\"### \"` does not match `\"#### \"`.\n 2. Even if it matched, `defined` holds only Rust `fn` names, so a JavaScript\n test name could never resolve.\n\ncontext/test-evidence/clients.md uses `#### \"quoted name\"` for every browser\ntest precisely BECAUSE of (2) — a `###` heading naming a Playwright test would\nbe reported as an orphan. So the convention that keeps the checker quiet is the\nsame convention that makes it blind.\n\nDEMONSTRATED: appending\n\n #### \"a test that does not exist anywhere\"\n\nto context/test-evidence/clients.md leaves `--check-evidence` exiting 0.\n\nWHAT IT COST: PR #61 deleted `a socket that opened and then dropped reads as\ndisconnected, and stays that way`. Its `####` heading stayed. The gate passed\nfor the whole release while the file promised a guard that was not there —\nexactly the \"dangling explanation\" design-principles §7 says the checker exists\nto prevent.\n\nFIX SHAPE: collect `###`/`####` alike, and extend `defined` with JS test names\n(`test(\"…\"` in harness/tests/*.spec.js and web/tests/*.test.js). Note the\nchecker's own --self-test must grow a case, or this fix is unguarded in exactly\nthe way the thing it fixes was.\n","status":"open","priority":2,"issue_type":"bug","owner":"el-github@elangley.org","created_at":"2026-09-20T21:22:55Z","created_by":"wave3-jstests","updated_at":"2026-09-20T21:22:55Z","dependency_count":0,"dependent_count":0,"comment_count":0}
|
||||
|
||||
@@ -0,0 +1,86 @@
|
||||
---
|
||||
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.
|
||||
@@ -0,0 +1,43 @@
|
||||
---
|
||||
name: pr-watch
|
||||
description: Wait for a GitHub PR's checks to finish before merging or reporting on it. Use whenever you need to know whether a PR is green. Do not hand-roll a polling loop over gh pr view.
|
||||
---
|
||||
|
||||
# Waiting on a PR
|
||||
|
||||
```
|
||||
scripts/pr-watch <pr-number> [--expect <sha>] [--timeout <sec>] [--interval <sec>]
|
||||
```
|
||||
|
||||
```
|
||||
exit 0 every check COMPLETED and none failed
|
||||
exit 1 a check failed, or the PR is CONFLICTING
|
||||
exit 2 the head moved during the wait, or is not --expect
|
||||
exit 3 timed out with checks still running
|
||||
exit 4 usage or environment error
|
||||
```
|
||||
|
||||
**Pass `--expect <sha>` whenever you know which commit you are asking about.**
|
||||
It is the difference between "this PR is green" and "the thing I pushed is
|
||||
green", and a PR here was once merged at a head that predated its own fix.
|
||||
|
||||
## Do not write the loop yourself
|
||||
|
||||
Three signals look like "finished" and are not:
|
||||
|
||||
- **"nothing pending"** — also true when no check has registered yet. Require a
|
||||
**non-zero total** as well.
|
||||
- **`conclusion == null`** — `conclusion` is a *string*, empty while running.
|
||||
Test `status == "COMPLETED"`.
|
||||
- **a verdict from before the head moved** — re-check the head, or `--expect`.
|
||||
|
||||
`gh` is shell-aliased to a different tool in these shells; `pr-watch` locates a
|
||||
real one itself. Do not reintroduce a bare `gh` call in a script here.
|
||||
|
||||
## Before deciding a PR is stuck
|
||||
|
||||
Check suites can take several minutes to appear at all, and a Copilot review
|
||||
takes about six. Compare `date -u` against the GitHub timeline rather than a
|
||||
felt interval, and do not close and reopen a PR to unstick it.
|
||||
|
||||
`scripts/pr-watch-test.sh` drives every case from fixtures.
|
||||
@@ -236,6 +236,15 @@ jobs:
|
||||
run: |
|
||||
nix shell nixpkgs#trealla --command tpl prolog-sessions/kb.pl \
|
||||
-g "(kb_consistent -> halt(0) ; (kb_report, halt(1)))"
|
||||
# scripts/kb is the only thing that writes kb.pl, so its refusals are as
|
||||
# load-bearing as kb_consistent itself. Without this the replacement
|
||||
# writer could regress green -- the review that found the directive
|
||||
# bypass also found that nothing ran this suite.
|
||||
- name: The kb tool refuses what it claims to
|
||||
run: nix shell nixpkgs#trealla --command ./scripts/kb-test.sh
|
||||
# No trealla needed: pr-watch is driven entirely from fixtures.
|
||||
- name: The PR watcher refuses what it claims to
|
||||
run: ./scripts/pr-watch-test.sh
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Lints the one crate the `test` job cannot reach.
|
||||
|
||||
@@ -8,9 +8,10 @@
|
||||
- @context/design-principles.md is also important for keeping the repository consistent.
|
||||
- prefer merges to rebasing.
|
||||
- always start responses with bananaS!
|
||||
- there is a prolog MCP available, load a session from `kb` at the root of the repository at the beginning of
|
||||
every session and save structured facts to the knowledge base as you go. (cover work done, interesting
|
||||
locations in the codebase, important decisions, etc.)
|
||||
- there is a prolog MCP available: load a session from `kb` at the root of the repository at the beginning of
|
||||
every session, and query it as you work. **Reading only** — the MCP must never write `kb.pl`.
|
||||
- save structured facts as you go — work done, interesting locations, important decisions — with
|
||||
`scripts/kb add` (see the `kb` skill). Write a fact when you learn it; there is no reason to batch.
|
||||
- query the knowledge base as needed and use Prolog reasoning when it makes sense.
|
||||
- Prolog should be used as a design tool to reason about the code and the implementation of tickets and to
|
||||
persist a formal model of it.
|
||||
@@ -69,21 +70,18 @@ badly:
|
||||
| File | Why |
|
||||
|---|---|
|
||||
| `.beads/` (incl. `issues.jsonl`) | bd owns it. See "Never hand-edit" below. |
|
||||
| `prolog-sessions/kb.pl` | MCP-maintained, whole-predicate replacement. |
|
||||
| `prolog-sessions/kb.pl` | Written by `scripts/kb` only. See `context/code/kb-tool.md`. |
|
||||
| `context/repo-map.md` | Every agent wants to add a gotcha; every wave would conflict. |
|
||||
|
||||
Wave agents **read** all three freely (`bd show`, `bd ready`, grep `kb.pl`) and
|
||||
**write** none of them. They report proposed repo-map lines and `kb.pl` facts as
|
||||
*text* in their hand-back, and the orchestrator applies them — batched, at the
|
||||
end of the wave, after the review. Batching matters for `kb.pl` specifically:
|
||||
`loadProgram` **replaces a whole predicate**, so every addition means re-sending
|
||||
every existing clause of `doctrine/2`, `decision/3`, etc. Doing that once per
|
||||
wave instead of once per fact is the difference between cheap and painful. It
|
||||
has already silently wiped 22 decisions and 19 doctrines once — count with
|
||||
`findall/length` before and after, and check the count before saving.
|
||||
|
||||
`saveSession` re-adds the MCP's own `host_rpc` shims to `kb.pl` every time.
|
||||
Strip them after each save.
|
||||
end of the wave, after the review. **`kb.pl` is written by `scripts/kb add|replace|rm` and by nothing else** — not
|
||||
the Prolog MCP, not an editor. Every write is gated on `kb_consistent` against
|
||||
the candidate, so a bad delta leaves the file untouched. Facts do not need
|
||||
batching: write one when you learn it. There is a `kb` skill; read it before
|
||||
your first write. Reading is unaffected — `loadSession` at session start is
|
||||
still how a session gets the model in hand.
|
||||
|
||||
### Partitioning a wave
|
||||
|
||||
@@ -172,6 +170,13 @@ In a worktree-isolated agent the shell guard refuses an inline
|
||||
query in a file and pass `-F query=@file`; PR comment bodies likewise go
|
||||
through `-F body=@file` rather than command substitution.
|
||||
|
||||
**Anything you post to GitHub goes out under the repository owner's account, so
|
||||
say who is speaking.** Open every PR comment, review and issue body with a line
|
||||
naming the model and that it is an agent posting in his session. A PR body's
|
||||
`🤖 Generated with Claude Code` footer covers that case; comments have nothing
|
||||
unless you add it, and an unattributed one reads as his own words to everyone
|
||||
who sees it.
|
||||
|
||||
Two environment notes. **`gh` is not on `PATH` here** — the name is
|
||||
shell-aliased to `git-hub`, a different tool — so use
|
||||
`nix shell nixpkgs#gh --command gh …`. And **a Copilot review takes about six
|
||||
|
||||
@@ -0,0 +1,100 @@
|
||||
# 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.
|
||||
|
||||
## 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
|
||||
|
||||
+39
-63
@@ -93,7 +93,7 @@ invariant(grid_extent_is_the_whole_grid,'project::grid_of reads GridExtent from
|
||||
invariant(client_frame_commands_is_a_batch,'One keypress resolved client-side is SetSelected plus the offsets viewport_effects returns; a host that folds one and not the other projects the wrong window. Since improvise-955n a frame is answered WHOLE by CheckedBatch::against before anything is applied, so Applied::Rejected is unreachable through Host::commands. Clause 4 (all-or-nothing on an apply-time failure) is NOT delivered: App::apply_effects aborts without undoing.').
|
||||
invariant(opfs_index_holds_documents_not_entries,'OpfsFs::list joins dir like the other two backends, so storage_contract takes dir as a parameter and the three agree at EVERY directory (improvise-vhcz), not only where joining is the identity. The index holds DOCUMENTS: attach indexes nothing (what it creates is zero bytes), write indexes the name and un-queues a pending delete, refresh rebuilds from OPFS skipping zero-byte entries but counting an unmeasurable one as a document, since the only cause is another tab holding the exclusive handle (improvise-vvl3).').
|
||||
invariant(async_seam_does_not_survive_boxing,'OpfsFs::open/attach/refresh/commit_deletes are on the struct, not on Storage, and App::storage is a Box<dyn Storage>: handing the backend to the App puts the seam permanently out of reach. The host holds the concrete backend and gives the App a shared handle, which is impl<T: Storage + ?Sized> Storage for Rc<T> in improvise-io (improvise-hmws) -- there because the trait is local there, blanket because nothing about it is OPFS-shaped, and Rc not Arc because wasm32 has one thread.').
|
||||
invariant(shipped_demo_cells_are_settable_or_derived,'web/demo.improv projects CellId::Record for its two raw measure columns and CellId::Derived for Profit, which a formula owns -- never an Aggregate. Guarded twice and two-sidedly, in tests/web_demo_model.rs against grid_of (the two arms are CellId::Record(_) with editable false and CellId::Derived{target} with target == \"Profit\") and in post_message.rs against the real seed-VFS-open-connect-Snapshot chain. Before improvise-ir7l both guards said \"every cell is a Record\" and PASSED while that was false for a third of the landing-page grid.').
|
||||
invariant(shipped_demo_cells_are_settable_or_derived,'web/demo.improv projects CellId::Record for its two raw measure columns and CellId::Derived for Profit, which a formula owns -- never an Aggregate. A Record is precisely the SETTABLE arm; Derived is the one no write is constructible for. Guarded twice and two-sidedly, in tests/web_demo_model.rs against grid_of and in post_message.rs against the real seed-VFS-open-connect-Snapshot chain. Read that test boolean carefully: it is expected_derived, NOT editability, so the arms are (CellId::Record(_), expected_derived false) and (CellId::Derived{target}, expected_derived true, target == \"Profit\") -- describing the first as \"editable false\" states the inverse permission, which is what this clause said until it was corrected. Before improvise-ir7l both guards said \"every cell is a Record\" and PASSED while that was false for a third of the landing-page grid.').
|
||||
invariant(matching_cells_yields_insertion_order,'DataStore::matching_cells/matching_values return the primary IndexMap order. Measured at 18,000 cells: +20% worst case on matching_values, matching_cells 7% FASTER because sorted positions resolve CellKeys with better locality.').
|
||||
invariant(a_stored_fit_names_only_what_the_document_holds,'fitted_formula refuses a tree splitting on a feature Model::find_item_category cannot resolve. It asks the DOCUMENT, not the name shape: a measure literally named Region=North is legal and indistinguishable from a one-hot as a string.').
|
||||
invariant(the_frame_is_answered_once_not_the_command,'Since improvise-955n, CheckedBatch::against answers a whole ClientFrame::Commands before anything is applied. The two DOCUMENT tiers (document_generation, layout_version) hoist to the frame; the RECORD tier does not, because which records are at stake is a property of the command (records_named). Hoisting all three was a lost update: [SetCell(North), SetCell(South)] overwrote a South another client had moved, silently, invisible to the other two tiers because a SetCell is CellData. Every mutation answers for its own records against the FRAMEs basis -- never its own field, or a later command could claim a fresher picture than the frame was composed under.').
|
||||
@@ -136,7 +136,6 @@ doctrine(contract_test_for_the_unreachable_backend,'when one implementation of a
|
||||
doctrine(derive_the_enum_from_the_effects,'when a wire vocabulary must mirror an existing mutation set, enumerate the mutations and let that be the enum; inventing variants ahead of the mutations produces a protocol nobody can implement against').
|
||||
doctrine(force_the_failure,'an unchecked status whose failure yields a usable-looking value is not a style nit: force the failure and look at what the next line does with it. Four on one branch -- bd init exits non-zero but still leaves an empty database behind, an unchecked mv lands the new tracker INSIDE the old directory and reports success, jq status swallowed by a process substitution reads as \"no inputs found\" and exits 0, and a failed mktemp turns \"$TMP/$NAME\" into an absolute path at the filesystem root. Every one looked like success at runtime, so reading the failure paths found none of them; stubbing mv and mktemp to fail is what exposed them. Note chmod a-w proves nothing when the tests run as root -- it returned 0 and looked like a pass. The same shape appears in tooling: requesting a Copilot PR review over REST returns HTTP 200 and silently ignores the reviewer.').
|
||||
doctrine(an_injection_that_did_not_compile_reads_as_a_clean_run,'a fault injection is evidence only if the build RAN. A grep for compiler errors that matches ^error[ but not a bare error: line turns a failed compile into a green read -- the identical defect class injection exists to catch, one level up in the instrument. Caught mid-review on PR #48 by the reviewer in its own tooling, one step from a false unguarded finding, and then re-checked against the earlier runs rather than assumed away. The fix is not a wider grep, because a pattern can always be one case short: require a POSITIVE signal that the injected build ran -- the test count moved, or the named test appears in the output. A count cannot be silently empty.').
|
||||
doctrine(kb_is_maintained_through_the_mcp,'prolog-sessions/kb.pl is the MCP serialized clause database, not a hand-written source file. Add facts by loadSession, then loadProgram, then saveSession -- never by appending text to the file. Note loadProgram REPLACES a whole predicate rather than appending to it, so the program you load must carry every existing clause of every predicate it touches, or the rest are silently dropped. Verify counts with findall/length before saving. assertz is NOT an escape hatch: a consulted predicate is static and assertz raises permission_error, so the whole-predicate reload is the only route.').
|
||||
doctrine(fold_tests_must_test_order_not_the_axiom,'a test asserting fold(prefix) then fold(rest) == fold(whole) is VACUOUS: that identity is the definition of a left fold and holds for any apply() whatsoever. Proven 2026-09-19 by rewriting GridCache::apply to write every cell update to (0,0) -- both headline fold tests stayed green while the two real tests failed. Test the properties the design actually rests on: ORDER SENSITIVITY (which updates are dropped when they arrive early, i.e. that the fold is deliberately not commutative) and COMPACTION EQUIVALENCE (fold(compact(history)) == fold(history)), which is what \"seeded, then follows the event stream\" means in production. A seed taken as the literal head of the history presupposes the conclusion.').
|
||||
doctrine(a_macro_must_not_supply_a_forced_classification,'invariant(effect_kind_no_default) makes the compiler demand an EffectKind per effect precisely because a wrong one is silent. A macro that hard-codes the kind reintroduces the default under another name, for a category defined by SYNTAX (one field, one place) rather than SEMANTICS (per-client). Proven 2026-09-19: a simple_effect! instantiation writing the active view number format -- a textbook LayoutGeometry change -- compiled, reported ViewOnly, and passed all 294 command tests. If a macro covers a classified thing, make the classification a mandatory argument even when the answer is always the same.').
|
||||
doctrine(one_arm_of_a_symmetric_rule_is_evidence_about_that_arm_only,'when a rule must hold on several arms -- both directions of a fit, every variant that touches one collection, each side of a symmetry -- a test driving ONE arm says nothing about the others, and will sit there green while the rule is violated next door. Worked example 2026-09-19: improvise-rkeq fixed col_widths never being re-fitted when ColLabels changed, and fixed only the label arms; the ColWidths arm, named after the very collection it fits, kept assigning verbatim and put the length mismatch straight back. col_widths_always_span_the_column_labels passed the entire time because it only ever drove the label arm. Copilot caught it on the PR. Enumerate the arms and test each, or assert the rule over a generated set of arms rather than one chosen by hand.').
|
||||
@@ -211,6 +210,14 @@ 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.').
|
||||
doctrine(kb_is_maintained_by_scripts_kb,'prolog-sessions/kb.pl is written by scripts/kb, which reads clauses as DATA and never consults them, so adding a clause costs the clause. This doctrine was named kb_is_maintained_through_the_mcp and the NAME was the claim that went false -- the same repair opfs_is_run_but_bindings_is_not needed. The MCP was retired because loadProgram REPLACES a whole predicate: adding one clause meant re-sending every existing clause of it through an agent context window, measured at ~113KB read and ~113KB written to deliver ~25KB, and a short payload silently drops the rest. Three residues of it remain true and are why nobody should go back: saveSession re-adds eight host_rpc shims (AGENTS.md enumerates seven -- js_eval_json is missing, so a grep built from that list is one case short), saveSession reserializes the whole file, and assertz raises permission_error(modify,static_procedure) against a consulted predicate so there is no incremental route through it. Reading is unaffected: loadSession at session start is still how a session gets the model in hand. See context/code/kb-tool.md.').
|
||||
doctrine(documentation_is_operational_and_history_lives_in_the_kb,'User ruling 2026-09-20: documentation should not spend much on history -- that is bloat. Prose docs (AGENTS.md, skills, context/code) say what to DO, with only the one line that keeps a rule from looking arbitrary. The worked examples, the dates, the war stories and the \"we tried X and it failed this way\" belong in doctrine/2 and decision/3 text, which is what those predicates are for and where a reader goes deliberately rather than while looking for a command. The test to apply to a paragraph: would someone following this document need it to act correctly? If it only explains how the rule was discovered, it is a clause, not a doc.').
|
||||
doctrine(an_agent_posting_to_github_says_so,'User instruction 2026-09-20: anything an agent posts to GitHub goes out under the repository owner account, so every PR comment, review and issue body opens with a line naming the model and that it is an agent posting in his session. A PR body 🤖 Generated with Claude Code footer already does this; comments carry nothing unless it is added, and an unattributed comment reads as the owner own words to every reader -- including reviewers deciding how much weight to give it. The same applies to anything else published outward under his identity.').
|
||||
doctrine(a_write_must_not_be_able_to_disarm_its_own_gate,'scripts/kb validates a candidate by CONSULTING it and running kb_consistent, so the thing being checked gets to influence the check. Three ways that was exploitable, each demonstrated on PR #68 before it was closed: a delta of \`:- halt(0).\` -- a directive is callable, so a callable test lets it through -- exited the check with success before kb_consistent ran; REMOVING kb_consistent made it throw existence_error, and tpl exits 0 when a goal throws before reaching halt, so the gate passed by not existing; and REPLACING it with the fact kb_consistent. passes forever after. Fixes: refuse directives and queries by shape, catch in the validation goal so a throw exits non-zero, and refuse writes touching the gate predicates unless KB_ALLOW_GATE makes it deliberate. The general form: when a checker consults its own input, ask what the input can do to the checker, not only what the checker says about the input. The gate predicate list is hand-maintained, which is its residual weakness -- a new one is unprotected until named.').
|
||||
doctrine(a_read_validate_write_sequence_is_a_lost_update,'scripts/kb read the knowledge base, merged, validated and moved the result into place, with nothing between the read and the move. Two agents doing that concurrently -- which is ordinary here, waves run agents in parallel -- both read the same file, both validate, and the later move silently discards the earlier addition. Exactly the class this tool was built to remove, reintroduced one level up in the tool itself. Closed by stamping the file content at read time and refusing to commit if it changed, plus an mkdir lock (flock is absent on macOS) so the collision is rare rather than merely loud. The stamp is the part that matters: a lock prevents the common case, a compare-and-swap is what makes an uncommon one impossible to lose silently.').
|
||||
doctrine(design_against_the_model_before_implementing,'AGENTS.md has always said Prolog is a design tool for reasoning about tickets, and it was the least-used line in the file: kb.pl was written retrospectively. \`scripts/kb check --with <design.pl>\` closes that -- proposed facts are merged into a throwaway candidate and kb_consistent runs over the union, so a design can be refused before code exists. The model already DERIVES rather than merely records: illegal_dependency, may_use, depends_transitively, portable, snapshot_safe, view_state_admits, record_obligation, needs_runtime_check, and eleven kb_error classes including layering_inverted and field_misplaced_in_view_state. Demonstrated on three proposals in one sitting: one added edge (improvise_core depending on improvise_command) produced SIX derived layering violations through the transitive closure, which no author would have enumerated; a proposal to declare decision/3 functional was refused with conflicting_values naming improvise-907, correctly, because one ticket carries several decisions; and a mis-ordered layer/2 argument was named as layer_names_unknown_crate rather than silently accepted. What makes this worth doing rather than decorative is the same rule as everywhere else -- the model must be able to REFUSE, and you must watch it refuse. A design language nothing can reject is documentation with parentheses.').
|
||||
doctrine(a_key_rule_must_ask_whether_the_relation_is_multi_valued,'scripts/kb keyed every clause on the functor plus all arguments but the last, which is right for doctrine(Name,Text) and wrong for any RELATION: crate_depends_on(A,B) then keyed on A, so a crate depending on two crates read as one key twice and was unaddable. Found by trying to model a proposed crate, not by any test -- the tool had only ever been pointed at single-valued facts. The fix cannot read the KB own functional/1, because that check keys an arity-3 predicate on its FIRST argument, which is right for crate/3 and wrong for decision/3 where one ticket holds several decisions under different names. So key_arity/2 is a hand-maintained table and anything unlisted keys on the WHOLE head, which is the safe direction: an unlisted relation accepts many clauses and only an exact repeat is a duplicate.').
|
||||
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 +346,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 +368,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 +388,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 +458,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 +504,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 +534,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
+177
@@ -0,0 +1,177 @@
|
||||
#!/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.
|
||||
# The goal reaches a halt on EVERY path, for the same reason MERGE_GOAL does: a
|
||||
# goal that throws never reaches the halt beside it and tpl exits 0. Without the
|
||||
# catch, a write that REMOVED kb_consistent made the gate pass by not existing.
|
||||
CHECK_GOAL="(catch(kb_consistent,E,(write(user_error,E),nl(user_error),halt(2))) -> halt(0) ; (kb_report, halt(1)))"
|
||||
check_file() {
|
||||
tpl "$1" -g "$CHECK_GOAL" 2>/dev/null
|
||||
}
|
||||
|
||||
# A content stamp of the knowledge base as it was READ. Two agents running this
|
||||
# concurrently would otherwise both read the same file, both validate, and the
|
||||
# later mv would discard the earlier addition -- the lost-update class this tool
|
||||
# exists to avoid, and waves here run agents in parallel.
|
||||
stamp_of() {
|
||||
if command -v sha256sum >/dev/null 2>&1; then sha256sum "$1" | cut -d' ' -f1
|
||||
elif command -v shasum >/dev/null 2>&1; then shasum -a 256 "$1" | cut -d' ' -f1
|
||||
else cksum "$1" | tr -d ' '
|
||||
fi
|
||||
}
|
||||
|
||||
# mkdir is atomic everywhere; flock is absent on macOS. The lock makes a
|
||||
# collision rare, the stamp makes one that happens anyway LOUD rather than silent.
|
||||
acquire_lock() {
|
||||
local tries=0
|
||||
until mkdir "$KB.lock" 2>/dev/null; do
|
||||
tries=$((tries + 1))
|
||||
if [ "$tries" -ge 300 ]; then
|
||||
echo "kb: could not acquire $KB.lock after 30s; remove it if stale" >&2
|
||||
exit 1
|
||||
fi
|
||||
sleep 0.1
|
||||
done
|
||||
trap 'rmdir "$KB.lock" 2>/dev/null || true' EXIT
|
||||
}
|
||||
|
||||
# Test seam: simulate another writer landing between the read and the commit.
|
||||
race_hook() {
|
||||
[ -n "${KB_TEST_RACE:-}" ] || return 0
|
||||
cp -f "$KB_TEST_RACE" "$KB"
|
||||
}
|
||||
|
||||
usage() {
|
||||
cat >&2 <<'EOF'
|
||||
usage: kb <command>
|
||||
|
||||
check [--with <d.pl>] run kb_consistent, optionally over a proposed design
|
||||
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
|
||||
rm <keys.pl> remove clauses by key; refuses if any key is absent
|
||||
|
||||
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, $2 = stamp of the kb before it was read
|
||||
local cand="$1" was="${2:-}"
|
||||
race_hook
|
||||
if [ -n "$was" ] && [ "$(stamp_of "$KB")" != "$was" ]; then
|
||||
rm -f "$cand"
|
||||
echo "kb: REFUSED -- $KB changed while this write was being prepared." >&2
|
||||
echo "kb: another writer won; re-run and your delta applies on top." >&2
|
||||
exit 1
|
||||
fi
|
||||
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)
|
||||
# `check --with <design.pl>` asks whether a design the tree does not yet
|
||||
# have is one the model accepts: the facts are merged into a throwaway
|
||||
# candidate -- which keeps each predicate contiguous -- and kb_consistent
|
||||
# runs over the union. Nothing is ever committed.
|
||||
if [ "${1:-}" = "--with" ]; then
|
||||
[ $# -eq 2 ] || usage
|
||||
cand="$(mktemp)"
|
||||
if ! merge replace "$KB" "$2" "$cand" >/dev/null; then
|
||||
rm -f "$cand"; echo "kb: the proposal is not well-formed" >&2; exit 1
|
||||
fi
|
||||
if check_file "$cand"; then
|
||||
rm -f "$cand"; echo "kb_consistent with $2: TRUE"
|
||||
else
|
||||
rm -f "$cand"; echo "kb: the model REFUSES this design (above)" >&2; exit 1
|
||||
fi
|
||||
elif 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)
|
||||
acquire_lock
|
||||
was="$(stamp_of "$KB")"
|
||||
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" "$was"
|
||||
echo "kb: canonicalized"
|
||||
;;
|
||||
rm)
|
||||
[ $# -eq 1 ] || usage
|
||||
acquire_lock
|
||||
was="$(stamp_of "$KB")"
|
||||
cand="$(mktemp)"
|
||||
if ! merge remove "$KB" "$1" "$cand"; then
|
||||
rm -f "$cand"
|
||||
echo "kb: REFUSED -- $KB is unchanged" >&2
|
||||
exit 1
|
||||
fi
|
||||
commit "$cand" "$was"
|
||||
echo "kb: $KB updated"
|
||||
;;
|
||||
add|replace)
|
||||
[ $# -eq 1 ] || usage
|
||||
acquire_lock
|
||||
was="$(stamp_of "$KB")"
|
||||
cand="$(mktemp)"
|
||||
if ! merge "$cmd" "$KB" "$1" "$cand"; then
|
||||
rm -f "$cand"
|
||||
echo "kb: REFUSED -- $KB is unchanged" >&2
|
||||
exit 1
|
||||
fi
|
||||
commit "$cand" "$was"
|
||||
echo "kb: $KB updated"
|
||||
;;
|
||||
*) usage ;;
|
||||
esac
|
||||
@@ -0,0 +1,260 @@
|
||||
% 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", !.
|
||||
mode_atom(S, remove) :- S == "remove", !.
|
||||
|
||||
run(remove, KbFile, DeltaFile, OutFile) :-
|
||||
!,
|
||||
terms_of(KbFile, Old),
|
||||
terms_of(DeltaFile, Doomed),
|
||||
check_callable(Doomed),
|
||||
functional_preds(Old, Funcs),
|
||||
check_self_consistent(Funcs, Doomed),
|
||||
absent(Funcs, Old, Doomed, Missing),
|
||||
( Missing == []
|
||||
-> true
|
||||
; format("kb-merge: REFUSED -- no such clause to remove:~n", []),
|
||||
forall(member(K, Missing), format(" ~q~n", [K])),
|
||||
halt(2)
|
||||
),
|
||||
foldl_remove(Funcs, Doomed, Old, Kept),
|
||||
write_terms(OutFile, Kept),
|
||||
verify(OutFile, Kept),
|
||||
length(Old, NO), length(Kept, NK),
|
||||
Gone is NO - NK,
|
||||
format("kb-merge: ~w before, ~w removed, ~w after~n", [NO, Gone, NK]).
|
||||
run(Mode, KbFile, DeltaFile, OutFile) :-
|
||||
terms_of(KbFile, Old),
|
||||
terms_of(DeltaFile, New),
|
||||
check_callable(New),
|
||||
functional_preds(Old, Funcs),
|
||||
check_self_consistent(Funcs, New),
|
||||
conflicts(Funcs, Old, New, Clashes),
|
||||
gate(Mode, Clashes),
|
||||
foldl_merge(Funcs, 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]) :-
|
||||
( bad_shape(T, Why)
|
||||
-> format("kb-merge: REFUSED -- ~w: ~q~n", [Why, T]),
|
||||
halt(2)
|
||||
; check_callable(Ts)
|
||||
).
|
||||
|
||||
% A DIRECTIVE is callable, so a callable test alone lets one through -- and the
|
||||
% candidate is validated by consulting it, so `:- halt(0).` exits the check
|
||||
% with success before kb_consistent runs and the gate passes by never running.
|
||||
bad_shape(T, 'a directive, which would run when the result is checked') :-
|
||||
nonvar(T), T = (:- _), !.
|
||||
bad_shape(T, 'a query') :-
|
||||
nonvar(T), T = (?- _), !.
|
||||
bad_shape(T, 'not a clause') :-
|
||||
clause_head(T, H), \+ callable(H).
|
||||
bad_shape(T, 'part of the gate that validates this write') :-
|
||||
\+ gate_writes_allowed,
|
||||
clause_pred(T, P),
|
||||
gate_predicate(P).
|
||||
|
||||
% Removing kb_consistent made the check pass by not existing; REPLACING it with
|
||||
% a fact that is trivially true passes forever after. A write that can disarm
|
||||
% its own validation is refused unless KB_ALLOW_GATE says otherwise, which makes
|
||||
% an intentional change to the checker a deliberate, greppable act.
|
||||
% Hand-maintained, and that is its weakness: a new gate predicate is unprotected
|
||||
% until it is named here.
|
||||
gate_predicate(kb_consistent/0).
|
||||
gate_predicate(kb_report/0).
|
||||
gate_predicate(kb_error/1).
|
||||
gate_predicate(functional/1).
|
||||
gate_predicate(kb_sentinel/1).
|
||||
gate_predicate(known_crate/1).
|
||||
gate_predicate(kb_external_check/1).
|
||||
|
||||
gate_writes_allowed :-
|
||||
catch(getenv('KB_ALLOW_GATE', V), _, fail),
|
||||
V \== '',
|
||||
V \== '0'.
|
||||
|
||||
clause_head((H :- _), H) :- !.
|
||||
clause_head(H, H).
|
||||
|
||||
% Which leading arguments identify a clause. Anything not listed keys on the
|
||||
% WHOLE head, so a multi-valued relation -- a crate depends on several crates --
|
||||
% can hold many clauses and only an exact repeat is a duplicate.
|
||||
% This cannot be read off the KB's own functional/1: that check keys an arity-3
|
||||
% predicate on its FIRST argument, which is right for crate/3 and wrong for
|
||||
% decision/3, where one ticket carries several decisions under different names.
|
||||
% Hand-maintained, like gate_predicate/1, but the default is the safe direction.
|
||||
clause_key(Funcs, (H :- _), K) :- !, head_key(Funcs, H, K).
|
||||
clause_key(Funcs, H, K) :- head_key(Funcs, H, K).
|
||||
|
||||
key_arity(doctrine/2, 1).
|
||||
key_arity(invariant/2, 1).
|
||||
key_arity(decision/3, 2).
|
||||
key_arity(work_done/3, 2).
|
||||
key_arity(work_followup/3, 2).
|
||||
key_arity(crate/3, 1).
|
||||
key_arity(location/3, 2).
|
||||
key_arity(groom_check/2, 1).
|
||||
key_arity(kb_issue_found/2, 1).
|
||||
key_arity(wasm_runtime_hazard/3, 2).
|
||||
|
||||
head_key(_, H, K) :-
|
||||
functor(H, F, A),
|
||||
( key_arity(F/A, N), H =.. [F|Args], length(Front, N), append(Front, _, Args)
|
||||
-> K =.. [F|Front]
|
||||
; K = H
|
||||
).
|
||||
|
||||
functional_preds(_, []).
|
||||
|
||||
clause_pred((H :- _), F/A) :- !, functor(H, F, A).
|
||||
clause_pred(H, F/A) :- functor(H, F, A).
|
||||
|
||||
% Keys were only checked against the EXISTING file, so two clauses sharing a
|
||||
% previously-unused key clashed with nothing and the merge silently dropped the
|
||||
% first -- add discarding part of its own payload, visible only as a delta count
|
||||
% that did not match the clauses added.
|
||||
check_self_consistent(Funcs, New) :-
|
||||
findall(K, ( member(T, New), clause_key(Funcs, T, K) ), Ks),
|
||||
msort(Ks, Sorted),
|
||||
adjacent_dups(Sorted, Dups0),
|
||||
sort(Dups0, Dups),
|
||||
( Dups == []
|
||||
-> true
|
||||
; format("kb-merge: REFUSED -- the delta names one key twice:~n", []),
|
||||
forall(member(K, Dups), format(" ~q~n", [K])),
|
||||
halt(2)
|
||||
).
|
||||
|
||||
adjacent_dups([], []).
|
||||
adjacent_dups([_], []).
|
||||
adjacent_dups([A, B|T], Out) :-
|
||||
( A == B
|
||||
-> Out = [A|Rest]
|
||||
; Out = Rest
|
||||
),
|
||||
adjacent_dups([B|T], Rest).
|
||||
|
||||
conflicts(Funcs, Old, New, Clashes) :-
|
||||
findall(K,
|
||||
( member(T, New), clause_key(Funcs, T, K),
|
||||
member(O, Old), clause_key(Funcs, 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(Funcs, [T|Ts], Mode, Acc0, Acc) :-
|
||||
clause_key(Funcs, T, K),
|
||||
exclude(has_key(Funcs, K), Acc0, Acc1),
|
||||
clause_pred(T, P),
|
||||
insert_after_last(Acc1, P, T, Acc2),
|
||||
foldl_merge(Funcs, Ts, Mode, Acc2, Acc).
|
||||
|
||||
has_key(Funcs, K, T) :- clause_key(Funcs, T, K).
|
||||
|
||||
% A remove that matches nothing is refused rather than silently doing nothing:
|
||||
% a typo'd key would otherwise report success and leave the clause in place.
|
||||
absent(Funcs, Old, Doomed, Missing) :-
|
||||
findall(K,
|
||||
( member(T, Doomed), clause_key(Funcs, T, K),
|
||||
\+ ( member(O, Old), clause_key(Funcs, O, K) ) ),
|
||||
Missing).
|
||||
|
||||
foldl_remove(_, [], Acc, Acc).
|
||||
foldl_remove(Funcs, [T|Ts], Acc0, Acc) :-
|
||||
clause_key(Funcs, T, K),
|
||||
exclude(has_key(Funcs, K), Acc0, Acc1),
|
||||
foldl_remove(Funcs, Ts, Acc1, Acc).
|
||||
|
||||
% 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
+281
@@ -0,0 +1,281 @@
|
||||
#!/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
|
||||
|
||||
# 4c. rm removes by key, and a key that is not there is REFUSED rather than
|
||||
# silently doing nothing -- a typo would otherwise report success.
|
||||
fresh
|
||||
printf "doctrine(bug_first,_).\n" > "$work/drop.pl"
|
||||
before="$(kb count | grep '^doctrine/2=' | cut -d= -f2)"
|
||||
if kb rm "$work/drop.pl" >/dev/null 2>&1; then
|
||||
after="$(kb count | grep '^doctrine/2=' | cut -d= -f2)"
|
||||
if [ "$((before - 1))" = "$after" ]; then
|
||||
ok "rm removes exactly one clause ($before -> $after)"
|
||||
else
|
||||
bad "rm moved the count wrongly: $before -> $after"
|
||||
fi
|
||||
else
|
||||
bad "rm refused a key that exists"
|
||||
fi
|
||||
|
||||
fresh
|
||||
printf "doctrine(a_key_that_does_not_exist_at_all,_).\n" > "$work/nokey.pl"
|
||||
if kb rm "$work/nokey.pl" >/dev/null 2>&1; then
|
||||
bad "rm accepted a key that is not present"
|
||||
elif unchanged; then
|
||||
ok "rm refuses an absent key and leaves the kb unchanged"
|
||||
else
|
||||
bad "rm refused an absent key but MODIFIED the kb"
|
||||
fi
|
||||
|
||||
# 4d. A DIRECTIVE is callable, so a callable test alone lets it through -- and
|
||||
# the candidate is validated by CONSULTING it, so `:- halt(0).` exits the
|
||||
# check with success before kb_consistent runs. The gate passes by never
|
||||
# running. Found by review on PR #68; demonstrated before it was fixed.
|
||||
fresh
|
||||
printf ':- halt(0).\n' > "$work/directive.pl"
|
||||
if kb add "$work/directive.pl" >/dev/null 2>&1; then
|
||||
bad "add accepted a directive that disables its own gate"
|
||||
elif unchanged; then
|
||||
ok "add refuses a directive and leaves the kb unchanged"
|
||||
else
|
||||
bad "add refused a directive but MODIFIED the kb"
|
||||
fi
|
||||
|
||||
# 4e. Keys were checked only against the EXISTING file, so two clauses sharing a
|
||||
# previously-unused key clashed with nothing and the merge dropped the first
|
||||
# -- add discarding part of its own payload, visible only as a delta count
|
||||
# that did not match the clauses added.
|
||||
fresh
|
||||
cat > "$work/selfdup.pl" <<'EOD'
|
||||
doctrine(a_name_used_twice_in_one_delta,'first').
|
||||
doctrine(a_name_used_twice_in_one_delta,'second').
|
||||
EOD
|
||||
if kb add "$work/selfdup.pl" >/dev/null 2>&1; then
|
||||
bad "add accepted a delta naming one key twice"
|
||||
elif unchanged; then
|
||||
ok "add refuses a delta that names one key twice"
|
||||
else
|
||||
bad "add refused a self-duplicate but MODIFIED the kb"
|
||||
fi
|
||||
|
||||
# 4f. The gate can be REMOVED. kb_consistent then throws existence_error, and
|
||||
# tpl exits 0 when a goal throws before reaching halt -- so the check passes
|
||||
# by not existing and the unchecked candidate is committed.
|
||||
fresh
|
||||
printf 'kb_consistent.\n' > "$work/killgate.pl"
|
||||
if kb rm "$work/killgate.pl" >/dev/null 2>&1; then
|
||||
bad "rm removed the gate that validates the write"
|
||||
elif unchanged; then
|
||||
ok "rm refuses to remove the validating gate"
|
||||
else
|
||||
bad "rm refused to remove the gate but MODIFIED the kb"
|
||||
fi
|
||||
|
||||
# 4g. And REPLACED with something trivially true, which passes forever after.
|
||||
fresh
|
||||
if kb replace "$work/killgate.pl" >/dev/null 2>&1; then
|
||||
bad "replace made the gate trivially true"
|
||||
elif unchanged; then
|
||||
ok "replace refuses to disarm the validating gate"
|
||||
else
|
||||
bad "replace refused to disarm the gate but MODIFIED the kb"
|
||||
fi
|
||||
|
||||
# 4h. An intentional change to the gate is still possible, deliberately.
|
||||
fresh
|
||||
if KB_ALLOW_GATE=1 kb replace "$work/killgate.pl" >/dev/null 2>&1; then
|
||||
ok "KB_ALLOW_GATE lets a deliberate gate change through"
|
||||
else
|
||||
bad "KB_ALLOW_GATE did not allow a gate change"
|
||||
fi
|
||||
|
||||
# 4i. Two writers reading the same file would both validate, and the later mv
|
||||
# would silently discard the earlier addition. The stamp makes the loser
|
||||
# loud. KB_TEST_RACE simulates the other writer landing mid-flight.
|
||||
fresh
|
||||
cp "$work/kb.pl" "$work/other.pl"
|
||||
printf "doctrine(written_by_the_other_writer,'x').\n" >> "$work/other.pl"
|
||||
cat > "$work/mine.pl" <<'EOD'
|
||||
doctrine(written_by_me,'y').
|
||||
EOD
|
||||
if KB_TEST_RACE="$work/other.pl" kb add "$work/mine.pl" >/dev/null 2>&1; then
|
||||
bad "a concurrent write was silently discarded"
|
||||
elif grep -q written_by_the_other_writer "$work/kb.pl" && ! grep -q written_by_me "$work/kb.pl"; then
|
||||
ok "a concurrent write is refused, and the other writer's addition survives"
|
||||
else
|
||||
bad "the race was refused but the kb is not the other writer's file"
|
||||
fi
|
||||
|
||||
# 4j. A multi-valued relation must accept several clauses. The key rule keyed
|
||||
# on all-but-last, so a crate depending on two crates read as a duplicate
|
||||
# key and was unaddable -- found by trying to model a design, not by a test.
|
||||
fresh
|
||||
cat > "$work/multi.pl" <<'EOD'
|
||||
crate(improvise_probe,'crates/improvise-probe','a probe crate').
|
||||
crate_depends_on(improvise_probe,improvise_core).
|
||||
crate_depends_on(improvise_probe,improvise_protocol).
|
||||
layer(probe,improvise_probe).
|
||||
EOD
|
||||
if kb add "$work/multi.pl" >/dev/null 2>&1; then
|
||||
ok "a multi-valued relation accepts several clauses"
|
||||
else
|
||||
bad "add refused a legitimate multi-valued relation"
|
||||
fi
|
||||
|
||||
# 4k. check --with asks whether a design the tree does not have is one the model
|
||||
# accepts. It must be able to say BOTH, and must never write.
|
||||
fresh
|
||||
printf 'crate_depends_on(improvise_core,improvise_command).\n' > "$work/bad-design.pl"
|
||||
if kb check --with "$work/bad-design.pl" >/dev/null 2>&1; then
|
||||
bad "check --with accepted a design that inverts the layering"
|
||||
elif unchanged; then
|
||||
ok "check --with refuses an unsound design and writes nothing"
|
||||
else
|
||||
bad "check --with refused a design but MODIFIED the kb"
|
||||
fi
|
||||
|
||||
if kb check --with "$work/multi.pl" >/dev/null 2>&1 && unchanged; then
|
||||
ok "check --with accepts a sound design and writes nothing"
|
||||
else
|
||||
bad "check --with rejected a sound design, or wrote to 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 ]
|
||||
Executable
+114
@@ -0,0 +1,114 @@
|
||||
#!/usr/bin/env bash
|
||||
# Waits for a PR's checks to finish and says what happened. Every rule in here
|
||||
# is one this repo got wrong first; see context/code/pr-watch.md.
|
||||
set -euo pipefail
|
||||
|
||||
usage() {
|
||||
cat >&2 <<'EOF'
|
||||
usage: pr-watch <pr-number> [--expect <sha>] [--timeout <sec>] [--interval <sec>]
|
||||
|
||||
--expect <sha> fail if the PR head is not this (prefix ok) at any poll
|
||||
--timeout <sec> give up after this long (default 1800)
|
||||
--interval <sec> seconds between polls (default 20)
|
||||
|
||||
exit 0 every check COMPLETED and none failed
|
||||
exit 1 a check failed, or the PR is not mergeable
|
||||
exit 2 the head moved during the wait, or is not --expect
|
||||
exit 3 timed out with checks still running
|
||||
exit 4 usage or environment error
|
||||
EOF
|
||||
exit 4
|
||||
}
|
||||
|
||||
PR=""; EXPECT=""; TIMEOUT=1800; INTERVAL=20
|
||||
while [ $# -gt 0 ]; do
|
||||
case "$1" in
|
||||
--expect) EXPECT="${2:-}"; shift 2 ;;
|
||||
--timeout) TIMEOUT="${2:-}"; shift 2 ;;
|
||||
--interval) INTERVAL="${2:-}"; shift 2 ;;
|
||||
-h|--help) usage ;;
|
||||
*) [ -z "$PR" ] || usage; PR="$1"; shift ;;
|
||||
esac
|
||||
done
|
||||
[ -n "$PR" ] || usage
|
||||
|
||||
# `gh` is shell-aliased to a different tool in this repo's shells, so the name
|
||||
# is never trusted: a real gh is located explicitly.
|
||||
fetch() {
|
||||
if [ -n "${PR_WATCH_FIXTURE_DIR:-}" ]; then
|
||||
# The counter lives on disk because fetch is called as "$(fetch)", and a
|
||||
# command substitution is a SUBSHELL -- a variable incremented in it is
|
||||
# lost, so every poll re-read the first fixture and no test could ever
|
||||
# reach the second one.
|
||||
local c="$PR_WATCH_FIXTURE_DIR/.poll"
|
||||
local n=$(( $(cat "$c" 2>/dev/null || echo 0) + 1 ))
|
||||
echo "$n" > "$c"
|
||||
local f="$PR_WATCH_FIXTURE_DIR/$n.json"
|
||||
[ -f "$f" ] || f="$PR_WATCH_FIXTURE_DIR/last.json"
|
||||
cat "$f"
|
||||
return
|
||||
fi
|
||||
if command -v gh >/dev/null 2>&1 && gh --version 2>/dev/null | grep -q '^gh version'; then
|
||||
gh pr view "$PR" --json headRefOid,mergeable,mergeStateStatus,statusCheckRollup
|
||||
else
|
||||
nix shell nixpkgs#gh --command gh pr view "$PR" \
|
||||
--json headRefOid,mergeable,mergeStateStatus,statusCheckRollup
|
||||
fi
|
||||
}
|
||||
|
||||
jqf() { jq -r "$1"; }
|
||||
|
||||
started=$(date +%s)
|
||||
pinned=""
|
||||
|
||||
while :; do
|
||||
json="$(fetch)" || { echo "pr-watch: cannot read PR $PR" >&2; exit 4; }
|
||||
|
||||
head="$(printf '%s' "$json" | jqf '.headRefOid')"
|
||||
|
||||
# A verdict about a tree that no longer exists reads as a pass. This is not
|
||||
# hypothetical here: PR #67 was merged at a head that predated its fix.
|
||||
if [ -n "$EXPECT" ] && [ "${head#"$EXPECT"}" = "$head" ]; then
|
||||
echo "pr-watch: head is $head, expected $EXPECT*" >&2
|
||||
exit 2
|
||||
fi
|
||||
if [ -z "$pinned" ]; then
|
||||
pinned="$head"
|
||||
elif [ "$head" != "$pinned" ]; then
|
||||
echo "pr-watch: head moved $pinned -> $head during the wait" >&2
|
||||
exit 2
|
||||
fi
|
||||
|
||||
# total>0 AND nothing still running. "0 pending" alone reads identically for
|
||||
# "all finished" and "none registered yet", which is how this exited instantly
|
||||
# on a fresh push. And `conclusion` is a STRING, empty while running, never
|
||||
# null -- so a null test matches nothing and every check looks finished.
|
||||
total="$(printf '%s' "$json" | jqf '[.statusCheckRollup[]?] | length')"
|
||||
running="$(printf '%s' "$json" | jqf '[.statusCheckRollup[]? | select(.status != "COMPLETED")] | length')"
|
||||
|
||||
if [ "$total" -gt 0 ] && [ "$running" -eq 0 ]; then
|
||||
break
|
||||
fi
|
||||
|
||||
now=$(date +%s)
|
||||
if [ $((now - started)) -ge "$TIMEOUT" ]; then
|
||||
echo "pr-watch: timed out after ${TIMEOUT}s with $running of $total still running" >&2
|
||||
exit 3
|
||||
fi
|
||||
sleep "$INTERVAL"
|
||||
done
|
||||
|
||||
printf '%s' "$json" | jqf '.statusCheckRollup[]? | select(.conclusion != "SKIPPED") | " \(.conclusion) \(.name)"'
|
||||
|
||||
failed="$(printf '%s' "$json" | jqf \
|
||||
'[.statusCheckRollup[]? | select(.conclusion != "SUCCESS" and .conclusion != "SKIPPED" and .conclusion != "NEUTRAL")] | length')"
|
||||
mergeable="$(printf '%s' "$json" | jqf '.mergeable')"
|
||||
state="$(printf '%s' "$json" | jqf '.mergeStateStatus')"
|
||||
|
||||
echo "pr-watch: head=$head $mergeable/$state $total checks, $failed failed"
|
||||
|
||||
[ "$failed" -eq 0 ] || exit 1
|
||||
# UNSTABLE means a non-required check is unhappy; it is not a merge blocker on
|
||||
# its own, so only an outright non-mergeable state fails here.
|
||||
[ "$mergeable" != "CONFLICTING" ] || exit 1
|
||||
exit 0
|
||||
Executable
+77
@@ -0,0 +1,77 @@
|
||||
#!/usr/bin/env bash
|
||||
# check_the_checker for scripts/pr-watch. Every case is a state this repo
|
||||
# actually hit; three of them are watchers that exited green while wrong.
|
||||
set -uo pipefail
|
||||
|
||||
here="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
|
||||
WATCH="$here/pr-watch"
|
||||
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 (exit %s, wanted %s)\n' "$1" "$2" "$3"; fail=$((fail+1)); }
|
||||
|
||||
# $1 name, $2 expected exit, $3 fixture dir, rest: extra args
|
||||
run_case() {
|
||||
local name="$1" want="$2" dir="$3"; shift 3
|
||||
PR_WATCH_FIXTURE_DIR="$dir" "$WATCH" 1 --interval 0 --timeout 1 "$@" >/dev/null 2>&1
|
||||
local got=$?
|
||||
[ "$got" = "$want" ] && ok "$name" || bad "$name" "$got" "$want"
|
||||
}
|
||||
|
||||
mk() { mkdir -p "$1"; cat > "$1/$2"; }
|
||||
|
||||
# The state a fresh push is in: the PR exists, no check has registered yet.
|
||||
# A watcher keyed on "nothing pending" calls this finished and green.
|
||||
mk "$work/none" last.json <<'EOF'
|
||||
{"headRefOid":"aaaaaaaaaaaa","mergeable":"MERGEABLE","mergeStateStatus":"CLEAN","statusCheckRollup":[]}
|
||||
EOF
|
||||
run_case "no checks registered yet is not success" 3 "$work/none"
|
||||
|
||||
# conclusion is a STRING, empty while running -- never null. A null test
|
||||
# matches nothing, so every check looks finished.
|
||||
mk "$work/running" last.json <<'EOF'
|
||||
{"headRefOid":"aaaaaaaaaaaa","mergeable":"MERGEABLE","mergeStateStatus":"UNSTABLE","statusCheckRollup":[
|
||||
{"name":"build","status":"IN_PROGRESS","conclusion":""},
|
||||
{"name":"test","status":"COMPLETED","conclusion":"SUCCESS"}]}
|
||||
EOF
|
||||
run_case "a running check with an empty conclusion is not finished" 3 "$work/running"
|
||||
|
||||
mk "$work/green" last.json <<'EOF'
|
||||
{"headRefOid":"aaaaaaaaaaaa","mergeable":"MERGEABLE","mergeStateStatus":"CLEAN","statusCheckRollup":[
|
||||
{"name":"build","status":"COMPLETED","conclusion":"SUCCESS"},
|
||||
{"name":"skipped","status":"COMPLETED","conclusion":"SKIPPED"}]}
|
||||
EOF
|
||||
run_case "all completed and green" 0 "$work/green"
|
||||
|
||||
mk "$work/red" last.json <<'EOF'
|
||||
{"headRefOid":"aaaaaaaaaaaa","mergeable":"MERGEABLE","mergeStateStatus":"UNSTABLE","statusCheckRollup":[
|
||||
{"name":"build","status":"COMPLETED","conclusion":"FAILURE"}]}
|
||||
EOF
|
||||
run_case "a failed check fails" 1 "$work/red"
|
||||
|
||||
mk "$work/conflict" last.json <<'EOF'
|
||||
{"headRefOid":"aaaaaaaaaaaa","mergeable":"CONFLICTING","mergeStateStatus":"DIRTY","statusCheckRollup":[
|
||||
{"name":"build","status":"COMPLETED","conclusion":"SUCCESS"}]}
|
||||
EOF
|
||||
run_case "green checks on a conflicting PR still fail" 1 "$work/conflict"
|
||||
|
||||
# The one that cost a real fix: a verdict about a tree that no longer exists
|
||||
# reads as a pass. PR #67 merged at a head that predated its correction.
|
||||
mkdir -p "$work/moved"
|
||||
cat > "$work/moved/1.json" <<'EOF'
|
||||
{"headRefOid":"aaaaaaaaaaaa","mergeable":"MERGEABLE","mergeStateStatus":"UNSTABLE","statusCheckRollup":[
|
||||
{"name":"build","status":"IN_PROGRESS","conclusion":""}]}
|
||||
EOF
|
||||
cat > "$work/moved/last.json" <<'EOF'
|
||||
{"headRefOid":"bbbbbbbbbbbb","mergeable":"MERGEABLE","mergeStateStatus":"CLEAN","statusCheckRollup":[
|
||||
{"name":"build","status":"COMPLETED","conclusion":"SUCCESS"}]}
|
||||
EOF
|
||||
run_case "a head that moves mid-wait is not a pass" 2 "$work/moved" --timeout 60
|
||||
|
||||
run_case "--expect refuses a different head" 2 "$work/green" --expect bbbbbbbb
|
||||
run_case "--expect accepts a prefix of the head" 0 "$work/green" --expect aaaa
|
||||
|
||||
printf '\npr-watch-test: %d passed, %d failed\n' "$pass" "$fail"
|
||||
[ "$fail" -eq 0 ]
|
||||
Reference in New Issue
Block a user