fix(v4): #190 POST regenerates the same; #16 sanitizers and hosted-check nightly

Captain Bob, 2026-11-13: "Create the issues then fix them before the long
acceptance test runs"; #16: "Nightly".

#190 -- make -C v4 post79 did not reproduce POST:
- mkpost.py runs v3 with address randomisation off (setarch -R): its
  printed addresses (>IN, FIND) are the same each run, so POST79.md is.
- v4/Makefile post79 builds hosted v3 from this tree's source first and
  uses it, not the lfs/ copy, which can be older.
- post_cases.c and POST79.md regenerated: 539 cases -- LOAD.rest_of_line,
  which v3 gets through since it changed after 2026-10-07. Two runs the
  same. POST_FLOOR 538 -> 539 (#173).
- test_host_unit.c takes the table's count, not 538 typed in the test.

#16 -- scripts/nightly.sh v4-checks: make -C v4 sanitize hosted-check,
logged under logs/<TS>/v4-checks/, refused without qemu-user; nightly.yml
runs it after publishing, before the proofs, installing qemu-user if the
image lacks it.

Evidence (logs/20261113-014927/post79, -024314): before, regenerated with
nothing changed: 539 cases and addresses differing run to run; after: the
same twice, hosted POST 539/539; test, test-32 99 programs 0 failures;
v4-checks 79 programs under the sanitizers 0 failures, the hosted builds
alike. The first verification failed at test_host_unit.c:442 (kept); a
stray v4-checks run stopped at once is kept, labelled (-014453).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_017RzZgrf7V7Zk2iczBXDRbm
This commit is contained in:
Claude
2026-11-13 03:19:24 +00:00
parent abfb30d0c4
commit be456d44e9
22 changed files with 408 additions and 320 deletions
+13 -1
View File
@@ -19,6 +19,10 @@
# found, and one value (#172 -- it was one distinct value, which two of the three could make).
# scripts/nightly.sh test-32
# make -C v4 test-32: v4 with 32-bit cells, every test (the acceptance's last part).
# scripts/nightly.sh v4-checks
# make -C v4 sanitize hosted-check (#16; Captain Bob, 2026-11-13: in the nightly): every v4
# test under ASan and UBSan at both widths, and the three hosted builds booting alike --
# aarch64 and riscv64 under qemu-user (make init). Its log is logs/<TS>/v4-checks/.
# scripts/nightly.sh proofs
# isabelle build -c -D proof/, capped to fit the server (one thread, small heaps): the StarForth
# session checked afresh every run, whatever is
@@ -76,7 +80,7 @@ DOCS=build/nightly-docs
LITHOS=$(sed -n 's/^LITHOS_VERSION *?= *//p' kernel/Makefile)
VERSION=${NIGHTLY_VERSION:-$LITHOS-SNAPSHOT}
usage() {
echo "Usage: scripts/nightly.sh accept <amd64|aarch64|riscv64|stick-high> | test-32 | proofs | images" >&2
echo "Usage: scripts/nightly.sh accept <amd64|aarch64|riscv64|stick-high> | test-32 | v4-checks | proofs | images" >&2
echo " | publish <URL> | docs | publish-docs <URL> | gitea-release <tag>" >&2
echo " | protocol [<stage>...] | protocol-report | dict-hash | post-count" >&2
echo " protocol stages: $PROTOCOL_STAGES" >&2
@@ -182,6 +186,14 @@ test-32)
make --no-print-directory -C v4 test-32 2>&1 | tee "$OUT/test-32.txt"
echo "=== nightly: test-32: $(grep -cE '[0-9]+ checks, 0 failures' "$OUT/test-32.txt") programs, 0 failures"
;;
v4-checks)
command -v qemu-aarch64 >/dev/null && command -v qemu-riscv64 >/dev/null \
|| { echo "nightly: v4-checks needs qemu-user (qemu-aarch64, qemu-riscv64): make init" >&2; exit 1; }
ts=$(date -u +%Y%m%d-%H%M%S)
mkdir -p "logs/$ts/v4-checks"
make --no-print-directory -C v4 sanitize hosted-check 2>&1 | tee "logs/$ts/v4-checks/v4-checks-$ts.log"
echo "=== nightly: v4-checks: $(grep -cE '[0-9]+ checks, 0 failures' "logs/$ts/v4-checks/v4-checks-$ts.log") programs under the sanitizers, 0 failures; the hosted builds alike"
;;
proofs)
need "$OUT/.started"
ts=$(date -u +%Y%m%d-%H%M%S)