From dd580e071778f12b5d8ad140601fbd63562348d5 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 12 Nov 2026 00:12:55 +0000 Subject: [PATCH] ci: the developer protocol -- nightly.sh protocol, PROTOCOL.md, and the gate checks it (#135) scripts/nightly.sh protocol: every stage a PR, the nightly and a release run -- accept amd64, aarch64, riscv64, stick-high, test-32, proofs, images, docs -- in order, never publish; the first failure ends it. protocol ... runs those only, so each can be its own foreground command (the QEMU rule); accept-amd64 begins a protocol, recording the commit and whether the tree is clean. protocol-report writes logs//PROTOCOL.md (the commit, the tree, each stage's result and output, POST and dict_hash per architecture compared, test-32's totals, the proofs' log, the images' and documents' SHA-256) and keeps every stage's output in logs//protocol/ -- nothing is left only in build/nightly. PASS only if every stage passed on the commit it began on and the tree is unchanged but for the evidence. acceptance.yml: scripts/check_protocol.sh on the PR's head, first, before the boots. The PR template asks for PROTOCOL.md; .claude/CLAUDE.md names the protocol as the acceptance a developer runs. Captain Bob, 2026-11-07 (#135); 2026-11-12: "Keep working on alpha.5". Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_017RzZgrf7V7Zk2iczBXDRbm --- .claude/CLAUDE.md | 19 +++++ .gitea/pull_request_template.md | 5 +- .gitea/workflows/acceptance.yml | 6 ++ scripts/nightly.sh | 142 ++++++++++++++++++++++++++++++++ 4 files changed, 171 insertions(+), 1 deletion(-) diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index 95be1ee8..4a0d2c32 100644 --- a/.claude/CLAUDE.md +++ b/.claude/CLAUDE.md @@ -300,6 +300,25 @@ make -f kernel/Makefile ARCH=amd64 clean qemu-stick-high make -C v4 test-32 ``` +**The developer protocol (#135, 2026-11-12) is the acceptance a developer runs, and its evidence +goes in the PR** (Captain Bob, 2026-11-07: "We can simply run nightly as developers ... Just no +Nexus push ... Then the protocol evidence can be submitted in the PR."): + +```bash +scripts/nightly.sh protocol # every stage above, then the proofs, the images, the documents; never publish +``` + +It writes `logs//PROTOCOL.md` (the commit, its tree clean or not, each stage's result, POST and +`dict_hash` per architecture, test-32, the proofs, the images' and documents' SHA-256) and each +stage's output in `logs//protocol/`. Commit `logs/` and `experiments/bare_metal/runs/`; the +PR's Acceptance check (`scripts/check_protocol.sh`) refuses a head without a passing PROTOCOL.md +for its tree -- any change outside the evidence after the run is stale, and the protocol is run +again. **One stage per foreground command is also a protocol**, and is how an agent runs it (the +QEMU rule: never in the background): `scripts/nightly.sh protocol accept-amd64`, then +`accept-aarch64`, `accept-riscv64`, `accept-stick-high`, `test-32`, `proofs`, `images`, `docs`, +each its own command, then `scripts/nightly.sh protocol-report`. The tools: `make +ARCH=amd64,aarch64,riscv64 init`, plus the HOL-Library heap the CI image has (`ci/runner-image`). + **v4 is the default build (Captain Bob, 2026-10-14: "v4 is the default build ... no, qemu to v4 too ... we are effectively trying to retire v3").** Every kernel build carries v4 and v3 and boots v4; `system=v3` in the boot arguments (`KERNEL_ARGS` for QEMU, `starforth.cfg` / diff --git a/.gitea/pull_request_template.md b/.gitea/pull_request_template.md index 6e1c8148..75a6edd8 100644 --- a/.gitea/pull_request_template.md +++ b/.gitea/pull_request_template.md @@ -10,7 +10,10 @@ The **Acceptance** check runs on this pull request by itself -- amd64, aarch64, stick loaded high, test-32 -- and `master` takes nothing that has not passed it. Note here anything it does not cover: -- [ ] Logs from runs made by hand are committed in `logs/`, if any +- [ ] `logs//PROTOCOL.md` for the head commit: `scripts/nightly.sh protocol`, run by hand, + its `logs/` and `experiments/bare_metal/runs/` committed (#135). The check refuses a head + without one, or with one for another tree. +- [ ] Logs from other runs made by hand are committed in `logs/`, if any - [ ] Hardware this was tried on, if any: ## The record diff --git a/.gitea/workflows/acceptance.yml b/.gitea/workflows/acceptance.yml index 8ace6863..ae8e8e46 100644 --- a/.gitea/workflows/acceptance.yml +++ b/.gitea/workflows/acceptance.yml @@ -38,6 +38,12 @@ jobs: fetch-depth: 0 # the SBOM's version is git describe lfs: false # only the logs and DoE CSVs are in LFS; the build needs neither + # The developer protocol's evidence first (#135): the PR's head carries a passing + # logs//PROTOCOL.md for its own tree (scripts/nightly.sh protocol, run by hand), or it is + # refused here, before the boots. The head, not the merge commit the checkout made. + - name: The developer protocol's evidence + run: scripts/check_protocol.sh "${{ github.event.pull_request.head.sha || 'HEAD' }}" + - name: The capsule-signing key env: KEY: ${{ secrets.CAPSULE_SIGN_KEY }} diff --git a/scripts/nightly.sh b/scripts/nightly.sh index 14e66cb6..64719261 100755 --- a/scripts/nightly.sh +++ b/scripts/nightly.sh @@ -46,6 +46,22 @@ # dictionary (The Dictionary of v4, #157 -- it fails the stage if a live word has no entry), # vol1, vol2, vol3, api (pdf). # +# The developer protocol (#135; Captain Bob, 2026-11-07: "We can simply run nightly as developers +# to further make sure nothing sneaks in. Just no Nexus push."): +# +# scripts/nightly.sh protocol +# Every stage, in order -- accept amd64, aarch64, riscv64, stick-high, test-32, proofs, +# images, docs -- never publish; the first that fails ends it. Then protocol-report. +# scripts/nightly.sh protocol ... +# Those stages only (accept-amd64 begins a protocol), each recorded; one per call runs each +# in a foreground command of its own. Then protocol-report, by hand. +# scripts/nightly.sh protocol-report +# logs//PROTOCOL.md: the commit and whether its tree was clean; each stage's result and +# logs; POST and dict_hash per architecture, compared; test-32's totals; the proofs'; the +# images' and documents' SHA-256 -- and each stage's own output, in logs//protocol/. The +# developer commits logs/ and experiments/bare_metal/runs/; the PR's Acceptance check +# (scripts/check_protocol.sh) refuses a head without a passing PROTOCOL.md for its tree. +# # VERSION is -SNAPSHOT, or NIGHTLY_VERSION when set (a release sets it from its # tag). NEXUS_USER (default ci-publisher) and NEXUS_PASSWORD; publishing needs mvn and a JRE. # Needs what make ARCH=amd64,aarch64,riscv64 init installs (INIT_DOCS=0 for the images, @@ -60,8 +76,15 @@ VERSION=${NIGHTLY_VERSION:-$LITHOS-SNAPSHOT} usage() { echo "Usage: scripts/nightly.sh accept | test-32 | proofs | images" >&2 echo " | publish | docs | publish-docs | gitea-release " >&2 + echo " | protocol [...] | protocol-report" >&2 + echo " protocol stages: $PROTOCOL_STAGES" >&2 exit 2 } +PROTO=build/protocol +PROTOCOL_STAGES="accept-amd64 accept-aarch64 accept-riscv64 accept-stick-high test-32 proofs images docs" +# The tree, but for the evidence the run writes (logs/, the DoE CSVs) and what builds leave behind +# untracked: what scripts/check_protocol.sh compares. +tree_dirt() { git status --porcelain -- . ':(exclude)logs' ':(exclude)experiments/bare_metal/runs'; } need() { for f in "$@"; do [ -f "$f" ] || { echo "nightly: no $f -- run the stages before this one" >&2; exit 1; }; done; } # deploy
[file ext classifier]... @@ -239,5 +262,124 @@ publish-docs) "$DOCS/vol1.pdf" pdf vol1 "$DOCS/vol2.pdf" pdf vol2 "$DOCS/vol3.pdf" pdf vol3 \ "$DOCS/api.pdf" pdf api ;; +protocol) + # The developer protocol (#135): the stages a PR, the nightly and a release run, never publish. + shift + all=0; [ $# -gt 0 ] || { set -- $PROTOCOL_STAGES; all=1; } + for s in "$@"; do case " $PROTOCOL_STAGES " in *" $s "*) ;; *) usage ;; esac; done + self="$(pwd)/scripts/nightly.sh" + for s in "$@"; do + if [ "$s" = accept-amd64 ]; then # a protocol begins: the commit, and its tree + rm -rf "$PROTO"; mkdir -p "$PROTO" + git rev-parse HEAD > "$PROTO/commit" + date -u +%Y%m%d-%H%M%S > "$PROTO/ts" + if [ -z "$(git status --porcelain)" ]; then echo clean > "$PROTO/tree"; else echo dirty > "$PROTO/tree"; fi + echo "=== nightly: protocol for $(git rev-parse --short HEAD), tree $(cat "$PROTO/tree")" + fi + need "$PROTO/commit" + [ "$(git rev-parse HEAD)" = "$(cat "$PROTO/commit")" ] \ + || { echo "nightly: HEAD is not the commit this protocol began on -- begin again with accept-amd64" >&2; exit 1; } + echo "=== nightly: protocol stage $s" + set +e + case $s in + accept-*) "$self" accept "${s#accept-}" ;; + *) "$self" "$s" ;; + esac 2>&1 | tee "$PROTO/$s.txt" + rc=${PIPESTATUS[0]} + set -e + echo "$rc" > "$PROTO/$s.rc" + if [ "$rc" != 0 ]; then + echo "nightly: protocol stage $s failed (exit $rc)" >&2 + [ $all = 0 ] || "$self" protocol-report || true + exit "$rc" + fi + done + [ $all = 0 ] || "$self" protocol-report + ;; +protocol-report) + # logs//PROTOCOL.md: what scripts/check_protocol.sh reads (- Commit:, - Tree:, - Result:) + # and what a reviewer reads. PASS only when every stage of this protocol passed, on the commit + # it began on, and the tree is still that commit's but for the evidence. + need "$PROTO/commit" "$PROTO/ts" "$PROTO/tree" + commit=$(cat "$PROTO/commit"); ts=$(cat "$PROTO/ts"); tree=$(cat "$PROTO/tree") + dir=logs/$ts; mkdir -p "$dir/protocol" + result=PASS; why=() + [ "$tree" = clean ] || { result=FAIL; why+=("the tree was not clean when the protocol began"); } + [ "$(git rev-parse HEAD)" = "$commit" ] || { result=FAIL; why+=("HEAD moved during the protocol"); } + [ -z "$(tree_dirt)" ] || { result=FAIL; why+=("the stages left the tree changed: $(tree_dirt | head -3 | tr '\n' ' ')"); } + rows=() + for s in $PROTOCOL_STAGES; do + if [ -f "$PROTO/$s.rc" ]; then + rc=$(cat "$PROTO/$s.rc"); cp "$PROTO/$s.txt" "$dir/protocol/$s.log" + if [ "$rc" = 0 ]; then st=PASS; else st="FAIL (exit $rc)"; result=FAIL; why+=("$s failed"); fi + else + st="not run"; result=FAIL; why+=("$s was not run") + fi + rows+=("| \`$s\` | $st | \`$dir/protocol/$s.log\` |") + done + boots=() + for a in amd64 aarch64 riscv64 stick-high; do + log=$(sed -n 's/^LOG: //p' "$OUT/accept-$a.txt" 2>/dev/null | head -1) + post=$( [ -n "$log" ] && grep -aoE "PARITY:V4_POST [^[:cntrl:]]*" "$log" | head -1) + sys=$( [ -n "$log" ] && grep -aoE "PARITY:V4_SYSTEM [^[:cntrl:]]*" "$log" | head -1) + boots+=("| $a | \`${log:-none}\` | \`${post:-none}\` | \`${sys:-none}\` |") + done + hashes=$(for a in amd64 aarch64 riscv64; do + log=$(sed -n 's/^LOG: //p' "$OUT/accept-$a.txt" 2>/dev/null | head -1) + [ -n "$log" ] && grep -aoE "PARITY:V4_SYSTEM [^[:cntrl:]]*" "$log" | sed -n 's/.*dict_hash=//p' | head -1 + done) + nh=$(grep -c . <<<"$hashes" || true); nu=$(sort -u <<<"$hashes" | grep -c . || true) + if [ "$nh" = 3 ] && [ "$nu" = 1 ]; then same="the same on all three: \`$(head -1 <<<"$hashes")\`" + else same="**not** one value on three architectures ($nh found, $nu distinct)"; result=FAIL; why+=("dict_hash"); fi + t32=$(grep -E '[0-9]+ checks, [0-9]+ failures' "$OUT/test-32.txt" 2>/dev/null | + awk '{c+=$(NF-3); f+=$(NF-1)} END {printf "%d programs, %d checks, %d failures", NR, c, f}') + isalog=$(find logs -path '*/isabelle/*.log' -newer "$PROTO/commit" 2>/dev/null | sort | tail -1) + { + echo "# Protocol for ${commit:0:8}" + echo + echo "- Commit: $commit" + echo "- Tree: $tree" + echo "- Result: $result" + echo + echo "\`scripts/nightly.sh protocol\` (#135), begun $ts UTC; \`$(git log -1 --format=%s "$commit")\`." + [ ${#why[@]} = 0 ] || { echo; echo "Not passed: $(IFS=';'; echo "${why[*]}")."; } + echo + echo "## Stages" + echo + echo "| Stage | Result | Output |" + echo "|---|---|---|" + printf '%s\n' "${rows[@]}" + echo + echo "## The boots" + echo + echo "| Boot | Serial log | POST | System |" + echo "|---|---|---|---|" + printf '%s\n' "${boots[@]}" + echo + echo "dict_hash: $same." + echo + echo "## test-32" + echo + echo "${t32:-not run}" + echo + echo "## The proofs" + echo + echo "\`${isalog:-none}\`" + echo + echo "## The images (SHA-256)" + echo + echo '```' + cat "$OUT/SHA256SUMS" 2>/dev/null || echo "not built" + echo '```' + echo + echo "## The documents (SHA-256)" + echo + echo '```' + cat "$DOCS/SHA256SUMS" 2>/dev/null || echo "not built" + echo '```' + } > "$dir/PROTOCOL.md" + echo "=== nightly: $dir/PROTOCOL.md: $result" + [ "$result" = PASS ] + ;; *) usage ;; esac