kb: a ledger excuses only the kb file its write published (improvise-yea8)
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
This commit is contained in:
+15
-4
@@ -72,7 +72,7 @@ acquire_lock() {
|
||||
scratch=()
|
||||
new_cand() {
|
||||
cand="$(mktemp "$KB.cand.XXXXXX")"
|
||||
scratch+=("$cand" "$cand.delta" "$cand.removed" "$cand.ledger" "$cand.base")
|
||||
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
|
||||
@@ -83,6 +83,14 @@ ledger_path() {
|
||||
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" 2>/dev/null || stat -f '%i %Fm' "$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() {
|
||||
@@ -140,19 +148,22 @@ commit() { # $1 = candidate, $2 = stamp of the kb as read, $3 = keys a rm remove
|
||||
echo "kb: cannot read the committed kb.pl to compare against; $KB is unchanged" >&2
|
||||
exit 3
|
||||
fi
|
||||
{ if [ -f "$ledger" ]; then cat "$ledger"; 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 and re-apply your deltas, or commit the removal." >&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.ledger" "$ledger"
|
||||
mv -f "$cand.stamped" "$ledger"
|
||||
mv -f "$cand" "$KB"
|
||||
}
|
||||
|
||||
|
||||
+10
-4
@@ -568,13 +568,19 @@ fi
|
||||
|
||||
# 20b. ...and the record excuses exactly what it names. A second, unrecorded
|
||||
# loss on top of a recorded rm must still refuse; a guard that stands down
|
||||
# whenever a ledger exists passes 20 and fails here.
|
||||
sed -i.bak '/^location(add_command,/d' "$work/kb.pl"; rm -f "$work/kb.pl.bak"
|
||||
# whenever a ledger exists passes 20 and fails here. The second loss is
|
||||
# made by giving the BASELINE a clause, not by editing the kb: an edit
|
||||
# voids the ledger (case 24), which would test that instead.
|
||||
awk -v x="location(a_probe_only_head_has,'src/nowhere.rs',probe)." '
|
||||
{ line[NR] = $0 } /^location\(/ { last = NR }
|
||||
END { for (i = 1; i <= NR; i++) { print line[i]; if (i == last) print x } }
|
||||
' "$KB" > "$work/head-plus.pl"
|
||||
cp "$work/kb.pl" "$work/twice.pl"
|
||||
printf "doctrine(another_probe_after_the_rm,'x').\n" > "$work/new2.pl"
|
||||
if kb add "$work/new2.pl" >"$work/out" 2>&1; then
|
||||
if KB_BASELINE="$work/head-plus.pl" kb add "$work/new2.pl" >"$work/out" 2>&1; then
|
||||
bad "a recorded rm excused an unrecorded loss beside it"
|
||||
elif cmp -s "$work/kb.pl" "$work/twice.pl" && said "$work/out" "1 of the baseline's are missing"; then
|
||||
elif cmp -s "$work/kb.pl" "$work/twice.pl" && said "$work/out" "1 of the baseline's are missing" \
|
||||
&& said "$work/out" "a_probe_only_head_has"; then
|
||||
ok "a recorded rm excuses only the clause it removed"
|
||||
else
|
||||
bad "the unrecorded loss was refused, but not by name, or the kb changed"
|
||||
|
||||
Reference in New Issue
Block a user