754add31e2
This follows the user's rulings: CI should not care which bash or which standard utilities it runs, and jobs take what the ci dev shell provides. - checkers.sh: remove find_modern_bash, the 5.1 floor (improvise-fd0j) and exit 3. Suites run under $BASH with PATH unchanged. - checkers-test.sh: remove sections 2, 5 and 5b (the fake bashes and utilbin). They existed only to pin the floor. - scripts/kb: drop the BSD `stat -f` fallback. kb needs the dev shell for tpl, and that shell's stat is GNU. - ci.yml: remove every `shell: bash` override, so every step runs in the dev shell. Remove the web-toolchain version probe and the Playwright version/browser probe. The shell's PLAYWRIGHT_BROWSERS_PATH pins the browsers. npm ci stays because @playwright/test is not nix-provided. - flake.nix: update the comments that promised those CI checks. Reasoning: context/code/tooling.md section 5. Evidence: context/test-evidence/tooling.md. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
241 lines
8.9 KiB
Bash
Executable File
241 lines
8.9 KiB
Bash
Executable File
#!/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}"
|
|
# Test seam: kb-test.sh injects a pre-fix kb-merge.pl to prove the arithmetic
|
|
# check catches a merge that drops a clause.
|
|
MERGE="${KB_MERGE:-$here/kb-merge.pl}"
|
|
# Exit codes: 0 done, 1 REFUSED (a verdict on the write), 2 usage, 3 the
|
|
# completeness baseline could not be read, 127 no tpl. Only 1 is a verdict.
|
|
|
|
# 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 'rm -f "${scratch[@]}"; rmdir "$KB.lock" 2>/dev/null || true' EXIT
|
|
}
|
|
|
|
# Every temporary a writing command makes. The candidate lives BESIDE the kb, so
|
|
# publishing it is a rename(2): a mv from $TMPDIR may cross a device and copy.
|
|
scratch=()
|
|
new_cand() {
|
|
cand="$(mktemp "$KB.cand.XXXXXX")"
|
|
scratch+=("$cand" "$cand.delta" "$cand.removed" "$cand.ledger" "$cand.base" "$cand.stamped")
|
|
}
|
|
|
|
# What `kb rm` removed that HEAD still has: the record that tells an intended
|
|
# removal from a lost clause. A fixture's sits beside it; the real one in .git.
|
|
ledger_path() {
|
|
if [ -n "${KB_FILE:-}" ]; then echo "$KB.removed"
|
|
else git -C "$repo" rev-parse --path-format=absolute --git-path kb-removed.pl
|
|
fi
|
|
}
|
|
|
|
# A ledger speaks only for the kb FILE this tool last published, named on its
|
|
# first line; bytes alone are not enough, since a restore can reproduce them.
|
|
file_stamp() {
|
|
printf '%s %s' "$(stamp_of "$1")" \
|
|
"$(stat -c '%i %.9Y' "$1")"
|
|
}
|
|
ledger_holds() { [ -f "$1" ] && [ "$(head -n 1 "$1")" = "% kb-stamp $(file_stamp "$2")" ]; }
|
|
|
|
# The committed knowledge base, which no write may end up short of.
|
|
# KB_BASELINE is the test seam, naming a file.
|
|
baseline_to() {
|
|
if [ -n "${KB_BASELINE:-}" ]; then cp -f "$KB_BASELINE" "$1"
|
|
else git -C "$repo" show HEAD:prolog-sessions/kb.pl > "$1" 2>/dev/null
|
|
fi
|
|
}
|
|
|
|
# Test seam: SIGKILL once the candidate is complete and checked, before it is
|
|
# published -- where a killed write dies. Records the candidate's path first.
|
|
kill_hook() {
|
|
[ -n "${KB_TEST_KILL:-}" ] || return 0
|
|
echo "$1" > "$KB_TEST_KILL"
|
|
kill -9 $$
|
|
}
|
|
|
|
# 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,
|
|
still holds every clause HEAD has that no `kb rm` removed, and passes
|
|
kb_consistent before it replaces the knowledge base.
|
|
|
|
Exit: 0 done, 1 refused, 2 usage, 3 HEAD's kb.pl unreadable, 127 no tpl.
|
|
EOF
|
|
exit 2
|
|
}
|
|
|
|
commit() { # $1 = candidate, $2 = stamp of the kb as read, $3 = keys a rm removes
|
|
local cand="$1" was="${2:-}" removing="${3:-}" ledger
|
|
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
|
|
ledger="$(ledger_path)"
|
|
if ! baseline_to "$cand.base"; then
|
|
echo "kb: cannot read the committed kb.pl to compare against; $KB is unchanged" >&2
|
|
exit 3
|
|
fi
|
|
{ if ledger_holds "$ledger" "$KB"; then cat "$ledger"; fi
|
|
if [ -n "$removing" ]; then cat "$removing"; fi; } > "$cand.removed"
|
|
if ! merge complete "$cand.base" "$cand" "$cand.removed" "$cand.ledger"; then
|
|
echo "kb: REFUSED -- clauses HEAD has are gone, with no kb rm recorded; $KB is unchanged." >&2
|
|
echo "kb: restore it from HEAD (git show HEAD:prolog-sessions/kb.pl) and re-apply your deltas." >&2
|
|
echo "kb: do NOT commit this kb.pl: a committed loss becomes the floor this check compares against." >&2
|
|
echo "kb: to drop a clause on purpose, restore first and then kb rm it." >&2
|
|
exit 1
|
|
fi
|
|
if ! check_file "$cand"; then
|
|
echo "kb: REFUSED -- kb_consistent fails on the result; $KB is unchanged" >&2
|
|
exit 1
|
|
fi
|
|
{ printf '%% kb-stamp %s\n' "$(file_stamp "$cand")"; cat "$cand.ledger"; } > "$cand.stamped"
|
|
kill_hook "$cand"
|
|
mv -f "$cand.stamped" "$ledger"
|
|
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")"
|
|
new_cand
|
|
: > "${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")"
|
|
new_cand
|
|
if ! merge remove "$KB" "$1" "$cand"; then
|
|
rm -f "$cand"
|
|
echo "kb: REFUSED -- $KB is unchanged" >&2
|
|
exit 1
|
|
fi
|
|
commit "$cand" "$was" "$1"
|
|
echo "kb: $KB updated"
|
|
;;
|
|
add|replace)
|
|
[ $# -eq 1 ] || usage
|
|
acquire_lock
|
|
was="$(stamp_of "$KB")"
|
|
new_cand
|
|
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
|