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
@@ -1,8 +1,9 @@
|
||||
# Nightly snapshot of the kernel images: the acceptance protocol, the board images, Nexus, then
|
||||
# the proofs. Each stage is a step of scripts/nightly.sh (its header says what each does); any
|
||||
# v4 under the sanitizers with the hosted builds (#16), and the proofs. Each stage is a step of scripts/nightly.sh (its header says what each does); any
|
||||
# failure stops the run, and nothing is published unless every stage before it passed. The proofs
|
||||
# come last and run whatever happened before them: they check the theories, not the images, so a
|
||||
# failed proof does not hold back images that passed acceptance -- it turns the run red.
|
||||
# failed proof does not hold back images that passed acceptance -- it turns the run red. The v4
|
||||
# checks (#16; Captain Bob, 2026-11-13: "Nightly") are the same: the engine on the host, not the images.
|
||||
#
|
||||
# org.starship:kernelImage:<LITHOS_VERSION>-SNAPSHOT, starshipos-snapshots
|
||||
# classifier pc StarshipOS.iso amd64, UEFI -- the ISO the amd64 acceptance boot booted
|
||||
@@ -80,6 +81,15 @@ jobs:
|
||||
name: kernel-images-${{ github.run_number }}
|
||||
path: build/nightly/
|
||||
|
||||
- name: v4 under the sanitizers, and the hosted builds alike
|
||||
if: always()
|
||||
run: | # hosted-check runs aarch64 and riscv64 under qemu-user (#16)
|
||||
if ! command -v qemu-aarch64 >/dev/null || ! command -v qemu-riscv64 >/dev/null; then
|
||||
S=$([ "$(id -u)" = 0 ] || echo sudo)
|
||||
$S apt-get update -qq && $S env DEBIAN_FRONTEND=noninteractive apt-get install -y -qq qemu-user
|
||||
fi
|
||||
scripts/nightly.sh v4-checks
|
||||
|
||||
- name: Isabelle/HOL proofs
|
||||
if: always()
|
||||
run: scripts/nightly.sh proofs
|
||||
|
||||
@@ -3,7 +3,7 @@
|
||||
Written by `v4/tools/mkpost.py` from `v4/tools/post79_rules.py`; do not edit.
|
||||
Design: `NUCLEUS.md` section 6. The cases are `v4/system/post_cases.c`.
|
||||
|
||||
POST runs 538 cases. 431 are v3's, with what the hosted v3 binary did as the
|
||||
POST runs 539 cases. 432 are v3's, with what the hosted v3 binary did as the
|
||||
expected result. This file lists every other case, and why.
|
||||
|
||||
## 1. Rewritten for FORTH-79 (59)
|
||||
@@ -60,11 +60,11 @@ standard's and not v3's.
|
||||
| `CMOVE.basic` | `HERE S" Test" DUP >R HERE 10 + SWAP CMOVE CR` | stack `317`, printed `\n` | `65 PAD C! 66 PAD 1+ C! PAD PAD 10 + 2 CMOVE PAD 10 + C@ . PAD 11 + C@ . CR` | stack `empty`, prints `65 66 \n` | v3's address unit is a byte; a v4 address unit is a cell (D-1); and the v3 case leaves a value on the return stack |
|
||||
| `TYPE.basic_string` | `HERE S" Hello" DUP >R HERE SWAP CMOVE HERE R> TYPE CR` | stack `392`, printed `Hello\n` | `72 PAD C! 105 PAD 1+ C! PAD 2 TYPE CR` | stack `empty`, prints `Hi\n` | v3's address unit is a byte; a v4 address unit is a cell (D-1); and FORTH-79: >R R> R@ are for use inside a definition; v4 refuses them at the prompt |
|
||||
| `TYPE.numbers` | `HERE S" 12345" DUP >R HERE SWAP CMOVE HERE R> TYPE CR` | stack `398`, printed `12345\n` | `49 PAD C! 50 PAD 1+ C! PAD 2 TYPE CR` | stack `empty`, prints `12\n` | v3's address unit is a byte; a v4 address unit is a cell (D-1); and FORTH-79: >R R> R@ are for use inside a definition; v4 refuses them at the prompt |
|
||||
| `>IN.initial` | `>IN @ . CR` | stack `empty`, printed `657828592 \n` | unchanged | stack `empty`, prints `6 \n` | FORTH-79: >IN is the offset into the input, 6 here; v3 prints an address |
|
||||
| `>IN.initial` | `>IN @ . CR` | stack `empty`, printed `7884064 \n` | unchanged | stack `empty`, prints `6 \n` | FORTH-79: >IN is the offset into the input, 6 here; v3 prints an address |
|
||||
| `UPDATE.no_block` | `0 SCR ! UPDATE` | error | unchanged | stack `empty`, prints nothing | v3 raises an error FORTH-79 does not ask for |
|
||||
| `SCR.after_load` | `1 LOAD SCR @ . CR` | stack `empty`, printed `` | unchanged | stack `empty`, prints `1 \n` | v3 prints nothing after 1 LOAD; SCR is still 1 from the LIST before |
|
||||
| `FIND.existing` | `FIND DUP . CR` | stack `empty`, printed `657827952 \n` | unchanged | 0 value(s) left; output not compared | FORTH-79: FIND takes the next word, DUP here, and leaves its address, which is printed |
|
||||
| `FIND.user_word` | `: test5 44 ; FIND test5 . CR` | stack `empty`, printed `658154448 \n` | unchanged | 0 value(s) left; output not compared | the address FIND leaves is printed |
|
||||
| `SCR.after_load` | `1 LOAD SCR @ . CR` | stack `empty`, printed `1 \n` | unchanged | stack `empty`, prints `1 \n` | v3 prints nothing after 1 LOAD; SCR is still 1 from the LIST before |
|
||||
| `FIND.existing` | `FIND DUP . CR` | stack `empty`, printed `7883424 \n` | unchanged | 0 value(s) left; output not compared | FORTH-79: FIND takes the next word, DUP here, and leaves its address, which is printed |
|
||||
| `FIND.user_word` | `: test5 44 ; FIND test5 . CR` | stack `empty`, printed `8203888 \n` | unchanged | 0 value(s) left; output not compared | the address FIND leaves is printed |
|
||||
| `FIND.empty` | `FIND` | error | unchanged | stack `0`, prints nothing | FORTH-79: FIND leaves 0 when there is no word; v3 raises an error |
|
||||
| `VOCABULARY.cross_vocab_access` | `VOCABULARY V1 V1 DEFINITIONS : V1WORD 11 ; FORTH V1WORD . CR` | stack `empty`, printed `11 \n` | unchanged | an error | FORTH-79: a word defined in another vocabulary is not found from FORTH; v3 finds it |
|
||||
| `VOCABULARY.duplicate` | `VOCABULARY TESTVOC VOCABULARY TESTVOC` | error | unchanged | stack `empty`, prints nothing | v3 raises an error FORTH-79 does not ask for: defining a name again |
|
||||
|
||||
@@ -0,0 +1,3 @@
|
||||
# Stopped, not a result: started by mistake on 2026-11-13 by a test of v4-checks's refusal
|
||||
# without qemu-user, which found qemu-user after all (/bin is /usr/bin here). Stopped by hand
|
||||
# at once; the stage was then tested with a PATH holding no qemu-*.
|
||||
Binary file not shown.
@@ -0,0 +1,7 @@
|
||||
# #190: make -C v4 post79
|
||||
before-*: the table regenerated with nothing changed, with the committed lfs/amd64/starforth and with v3 built from source: 539 cases, LOAD.rest_of_line added (v3 changed since 2026-10-07); POST79.md's v3 addresses different each run.
|
||||
after-run1/2.log: post79 after the fix (v3 built from source, run with setarch -R): post_cases.c and POST79.md the same both runs; 539 cases; hosted POST 539/539.
|
||||
failed-1-*.log: the first verification after the fix: test_host_unit.c:442 wanted 538 POST cases, typed in the test; POST ran 539 of 539. The test now takes the table's own count.
|
||||
after-test-test32.log: make -C v4 test test-32 after both fixes: 99 programs, 3724162 checks, 0 failures.
|
||||
logs/20261113-024314/v4-checks: scripts/nightly.sh v4-checks (#16), its first real run: 79 programs under the sanitizers, 0 failures; the hosted builds alike.
|
||||
logs/20261113-020030/v4-checks: the same stage on the first verification, which failed at test_host_unit.c:442 (see failed-1-*).
|
||||
Binary file not shown.
Binary file not shown.
Binary file not shown.
@@ -0,0 +1,8 @@
|
||||
# #190, before the fix: POST79.md as mkpost.py wrote it from v3 built from source (<) against the committed one (>):
|
||||
# v3's printed addresses differ. Two runs of that same binary also differed from each other: >IN.initial printed 1076337952, then 241286432.
|
||||
< | `>IN.initial` | `>IN @ . CR` | stack `empty`, printed `1076337952 \n` | unchanged | stack `empty`, prints `6 \n` | FORTH-79: >IN is the offset into the input, 6 here; v3 prints an address |
|
||||
> | `>IN.initial` | `>IN @ . CR` | stack `empty`, printed `657828592 \n` | unchanged | stack `empty`, prints `6 \n` | FORTH-79: >IN is the offset into the input, 6 here; v3 prints an address |
|
||||
< | `FIND.existing` | `FIND DUP . CR` | stack `empty`, printed `1076337312 \n` | unchanged | 0 value(s) left; output not compared | FORTH-79: FIND takes the next word, DUP here, and leaves its address, which is printed |
|
||||
< | `FIND.user_word` | `: test5 44 ; FIND test5 . CR` | stack `empty`, printed `1076657776 \n` | unchanged | 0 value(s) left; output not compared | the address FIND leaves is printed |
|
||||
> | `FIND.existing` | `FIND DUP . CR` | stack `empty`, printed `657827952 \n` | unchanged | 0 value(s) left; output not compared | FORTH-79: FIND takes the next word, DUP here, and leaves its address, which is printed |
|
||||
> | `FIND.user_word` | `: test5 44 ; FIND test5 . CR` | stack `empty`, printed `658154448 \n` | unchanged | 0 value(s) left; output not compared | the address FIND leaves is printed |
|
||||
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
@@ -0,0 +1,2 @@
|
||||
# The first real run of scripts/nightly.sh v4-checks (#16), on the first verification of #190: it
|
||||
# stopped at test_host_unit.c:442 (538 typed in the test; POST ran 539). Kept as evidence.
|
||||
Binary file not shown.
Binary file not shown.
+13
-1
@@ -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)
|
||||
|
||||
+6
-3
@@ -218,13 +218,16 @@ $(foreach i,$(HOSTED_ISAS),$(eval $(call HOSTED_RULE,$(i))))
|
||||
# `make post` boots the amd64 system alone, which is the quick check after a
|
||||
# change to the vocabulary: nucleus, forth79.4th, POST, prompt. `make
|
||||
# post79` writes POST's cases, system/post_cases.c, again from
|
||||
# v3's cases and tools/post79_rules.py (tools/mkpost.py); it needs the
|
||||
# hosted v3 binary.
|
||||
# v3's cases and tools/post79_rules.py (tools/mkpost.py), with the hosted v3
|
||||
# binary built first from this tree's source -- v3/Makefile, in its own build
|
||||
# directory; not the lfs/ copy, which can be older (#190).
|
||||
V3_HOSTED = $(shell $(MAKE) -s -C $(ROOT) -f v3/Makefile --eval 'v3bin: ; @echo $$(BINARY)' v3bin 2>/dev/null)
|
||||
.PHONY: post post79
|
||||
post: $(BINDIR)/starforth4-amd64
|
||||
@$(BINDIR)/starforth4-amd64 < /dev/null
|
||||
post79:
|
||||
python3 $(HERE)/tools/mkpost.py
|
||||
$(MAKE) --no-print-directory -C $(ROOT) -f v3/Makefile $(V3_HOSTED)
|
||||
python3 $(HERE)/tools/mkpost.py --v3 $(ROOT)/$(V3_HOSTED)
|
||||
|
||||
# `make hosted` builds the three. `make hosted-check` boots each with no
|
||||
# input and requires that all three print the same lines, ending in
|
||||
|
||||
@@ -1,3 +1,3 @@
|
||||
538
|
||||
539
|
||||
# v4 POST: the fewest tests an accepted boot may report (#173). Raise it when POST grows;
|
||||
# never lower it without Captain Bob. scripts/nightly.sh post-count reads the first line.
|
||||
|
||||
+307
-305
File diff suppressed because it is too large
Load Diff
@@ -439,8 +439,11 @@ int main(void)
|
||||
uint64_t hash = v4_image_dict_hash(hera, &im);
|
||||
memcpy(before, hera->mem, sizeof before);
|
||||
host.self = 0; host.n = hera; host.line = post_line; host.say = post_say;
|
||||
CHECK(v4_post_run(&host, v4_post_cases, v4_post_case_count, &tally) && tally.tests == 538 && tally.pass == 538 && tally.fail == 0
|
||||
&& strstr(post_said, "PARITY:V4_POST tests=538 pass=538 fail=0\n") != NULL && strstr(post_said, "POST FAIL") == NULL,
|
||||
char want_line[64]; /* the table's own count, not a number typed here: it was 538, POST grew (#190) */
|
||||
snprintf(want_line, sizeof want_line, "PARITY:V4_POST tests=%u pass=%u fail=0\n", v4_post_case_count, v4_post_case_count);
|
||||
CHECK(v4_post_run(&host, v4_post_cases, v4_post_case_count, &tally) && tally.tests == v4_post_case_count
|
||||
&& tally.pass == v4_post_case_count && tally.fail == 0
|
||||
&& strstr(post_said, want_line) != NULL && strstr(post_said, "POST FAIL") == NULL,
|
||||
"and passes POST, which the kernel runs on her: %u of %u, %u failed; \"%s\"", tally.pass, tally.tests, tally.fail, post_said);
|
||||
CHECK(strcmp(tell(10, "RS1"), "42 42 \n") == 0, "while POST runs, what its cases define is on her: \"%s\"", printed);
|
||||
CHECK(strstr(tell(10, "COLD"), "Cold Start") != NULL, "the kernel puts her back to the system as it was sealed");
|
||||
|
||||
+9
-1
@@ -29,7 +29,9 @@ and the same lines.)
|
||||
"""
|
||||
import argparse
|
||||
import os
|
||||
import platform
|
||||
import re
|
||||
import shutil
|
||||
import subprocess
|
||||
import sys
|
||||
|
||||
@@ -252,7 +254,13 @@ def run_v3(v3, cases):
|
||||
script.extend(line[3:] for line in case["lines"])
|
||||
script.append('." [[E%d]]" BASE @ DECIMAL .S BASE ! ." [[S%d]]"' % (n, n))
|
||||
script.append("BYE")
|
||||
done = subprocess.run([v3, "--log-none"], input=("\n".join(script) + "\n").encode("latin-1"),
|
||||
# With the address space randomised, what v3 prints for an address (>IN, FIND) is different on
|
||||
# every run, so the report (POST79.md) could never be written twice the same (#190): v3 is run
|
||||
# with randomisation off (setarch -R), and its addresses are the same each time.
|
||||
cmd = [v3, "--log-none"]
|
||||
if shutil.which("setarch"):
|
||||
cmd = ["setarch", platform.machine(), "-R"] + cmd
|
||||
done = subprocess.run(cmd, input=("\n".join(script) + "\n").encode("latin-1"),
|
||||
capture_output=True, timeout=600)
|
||||
text = ANSI.sub("", done.stdout.decode("latin-1")) # a byte is a character
|
||||
results = []
|
||||
|
||||
Reference in New Issue
Block a user