From 04006bff1267ede28e9c253d75b252b3353b08a7 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 7 Nov 2026 18:40:00 +0000 Subject: [PATCH 1/5] release: v4.0.0-alpha.2; release.yml keeps the image's Isabelle [skip ci] v4.0.0-alpha.1's release run (196) was killed in the proofs: release.yml's full `make init` fetched Isabelle into the workspace and pointed isabelle at it, without the image's prebuilt HOL-Library, so the proofs built it from scratch. Nothing was published. Ruled: the tag stays; release.yml runs `init INIT_PROOFS=0`; LITHOS_VERSION 4.0.0-alpha.2, the first published alpha. FABRIC-3.md XLVII.5, CHANGELOG. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2 --- .gitea/workflows/release.yml | 5 ++++- CHANGELOG.md | 8 ++++++++ docs/fabric/FABRIC-3.md | 13 +++++++++++++ kernel/Makefile | 5 ++++- 4 files changed, 29 insertions(+), 2 deletions(-) diff --git a/.gitea/workflows/release.yml b/.gitea/workflows/release.yml index 89469431..e58d82bd 100644 --- a/.gitea/workflows/release.yml +++ b/.gitea/workflows/release.yml @@ -54,7 +54,10 @@ jobs: echo "NIGHTLY_VERSION=${tree#v}" >> "$GITHUB_ENV" - name: Install the dependencies - run: make ARCH=amd64,aarch64,riscv64 init # the image has all but the documents' packages + # INIT_PROOFS=0: the image's Isabelle has HOL-Library prebuilt; a full init would fetch a fresh + # Isabelle into the workspace and point isabelle at it, and the proofs would build HOL-Library + # from scratch -- killed (release run 196, v4.0.0-alpha.1) + run: make ARCH=amd64,aarch64,riscv64 init INIT_PROOFS=0 # the image has all but the documents' packages - name: Acceptance amd64 run: scripts/nightly.sh accept amd64 diff --git a/CHANGELOG.md b/CHANGELOG.md index a8ad0b7a..409d7df9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,13 @@ # Changelog +## 2026-11-07 — LithosAnanke v4.0.0-alpha.2: the first published alpha + +`v4.0.0-alpha.1` (`233025da`) was accepted and tagged, but its release run (196) built HOL-Library +from scratch in the proofs step and was killed: `release.yml`'s full `make init` replaced the +image's Isabelle, the one with HOL-Library prebuilt. Nothing was published; the tag stays where it is +(Captain Bob, 2026-11-07). `release.yml` now runs `init INIT_PROOFS=0`, and `v4.0.0-alpha.2` is the +first alpha published -- the same system as below. `docs/fabric/FABRIC-3.md` XLVII.5. + ## 2026-11-07 — LithosAnanke v4.0.0-alpha.1: the first alpha release The first alpha of the kernel, `v4.0.0-alpha.1`: v4, StarForth's F18 engine, is the system every diff --git a/docs/fabric/FABRIC-3.md b/docs/fabric/FABRIC-3.md index 82ca875d..755bc19a 100644 --- a/docs/fabric/FABRIC-3.md +++ b/docs/fabric/FABRIC-3.md @@ -6165,3 +6165,16 @@ Isabelle2025-2 (HOL-Library and its build database) is a package in this reposit `bb247846...e999cb339e`), and the image fetches it into Isabelle's system heaps, checksum pinned, its token a Docker build secret. Shown portable first: a fresh Isabelle home holding only that heap checks the StarForth session without rebuilding HOL-Library (24 s). + +### 5. v4.0.0-alpha.1 not published; v4.0.0-alpha.2 + +PR #127 merged (`4f675c8b`, acceptance run 192 with the capsules signed); `runner-image.yml` built +`lithosananke-runner:4f675c8b75b2` with HOL-Library fetched (checksum OK, 4.8 s); PR #128 moved the +workflows onto it (`233025da`, acceptance run 195 in the new image). `v4.0.0-alpha.1` was tagged on +`233025da`. Its release run (196) passed acceptance in full, then the proofs step built HOL-Library +from scratch and was killed (exit 137): `release.yml` ran a full `make init` for the documents' +packages, which also fetched Isabelle into the workspace and pointed `/usr/local/bin/isabelle` at it +-- an Isabelle without the image's HOL-Library. Nothing was published. Ruled (Captain Bob, +2026-11-07): the tag stays where it is; `release.yml` runs `init INIT_PROOFS=0` (as +`nightly-docs.yml` does), `LITHOS_VERSION` becomes `4.0.0-alpha.2`, and `v4.0.0-alpha.2` is the +first published alpha. diff --git a/kernel/Makefile b/kernel/Makefile index 81bcbd7b..a7c86bb5 100644 --- a/kernel/Makefile +++ b/kernel/Makefile @@ -95,6 +95,9 @@ endif # v3.0.0, the first LTS, is no longer the next number -- an LTS line takes the next # odd major when §XXX.5's criteria are met. The engine stays 3.2.0. Alphas are # numbered (-alpha.N); a release repository takes each version once. +# v4.0.0-alpha.2 — the first published alpha: v4.0.0-alpha.1 (233025da) was accepted and tagged, +# but its release run's proofs step built HOL-Library from scratch and was killed, so +# nothing was published; the tag stays where it is (Captain Bob, 2026-11-07). # LITHOS_VERSION (kernel) and VERSION (embedded StarForth engine) are independent # and do not auto-sync (§XXX.4) — do not infer a relationship if they ever coincide. # Engine VERSION bumps at tag time by what actually changed (§XXX.6): major = any @@ -103,7 +106,7 @@ endif # the messaging layer was replaced by kernel-Hermes, PLOT/FB-* relocated to Hestia — # all dictionary-visible, no FORTH-79 word semantics changed. VERSION ?= 3.2.0 -LITHOS_VERSION ?= 4.0.0-alpha.1 +LITHOS_VERSION ?= 4.0.0-alpha.2 # ============================================================================== # BUILD PATHS From d8bf2e11213b88034031a9322f7015aea46ac783 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 7 Nov 2026 18:55:30 +0000 Subject: [PATCH 2/5] release v4.0.0-alpha.2: accepted in full, logs [skip ci] The protocol on 04006bff (LithosAnanke v4.0.0-alpha.2), in this session, one QEMU at a time in the foreground: amd64 logs/20261107-184040, aarch64 -184241, riscv64 -184616 (POST 538/538, dict_hash=0xfec8c47cfc6f437f on all three), the stick loaded high -184753, test-32 (39 programs, 0 failures), the Isabelle/HOL proofs (logs/20261107-185450/). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2 --- experiments/bare_metal/runs/doe-aarch64-20261107-184241.csv | 0 experiments/bare_metal/runs/doe-amd64-20261107-184040.csv | 0 experiments/bare_metal/runs/doe-amd64-20261107-184753.csv | 0 experiments/bare_metal/runs/doe-riscv64-20261107-184616.csv | 0 logs/20261107-184040/amd64/qemu-amd64-20261107-184040.log | 3 +++ logs/20261107-184241/aarch64/qemu-aarch64-20261107-184241.log | 3 +++ logs/20261107-184616/riscv64/qemu-riscv64-20261107-184616.log | 3 +++ logs/20261107-184753/amd64/qemu-amd64-20261107-184753.log | 3 +++ logs/20261107-185450/isabelle/isabelle-20261107-185450.log | 3 +++ 9 files changed, 15 insertions(+) create mode 100644 experiments/bare_metal/runs/doe-aarch64-20261107-184241.csv create mode 100644 experiments/bare_metal/runs/doe-amd64-20261107-184040.csv create mode 100644 experiments/bare_metal/runs/doe-amd64-20261107-184753.csv create mode 100644 experiments/bare_metal/runs/doe-riscv64-20261107-184616.csv create mode 100644 logs/20261107-184040/amd64/qemu-amd64-20261107-184040.log create mode 100644 logs/20261107-184241/aarch64/qemu-aarch64-20261107-184241.log create mode 100644 logs/20261107-184616/riscv64/qemu-riscv64-20261107-184616.log create mode 100644 logs/20261107-184753/amd64/qemu-amd64-20261107-184753.log create mode 100644 logs/20261107-185450/isabelle/isabelle-20261107-185450.log diff --git a/experiments/bare_metal/runs/doe-aarch64-20261107-184241.csv b/experiments/bare_metal/runs/doe-aarch64-20261107-184241.csv new file mode 100644 index 00000000..e69de29b diff --git a/experiments/bare_metal/runs/doe-amd64-20261107-184040.csv b/experiments/bare_metal/runs/doe-amd64-20261107-184040.csv new file mode 100644 index 00000000..e69de29b diff --git a/experiments/bare_metal/runs/doe-amd64-20261107-184753.csv b/experiments/bare_metal/runs/doe-amd64-20261107-184753.csv new file mode 100644 index 00000000..e69de29b diff --git a/experiments/bare_metal/runs/doe-riscv64-20261107-184616.csv b/experiments/bare_metal/runs/doe-riscv64-20261107-184616.csv new file mode 100644 index 00000000..e69de29b diff --git a/logs/20261107-184040/amd64/qemu-amd64-20261107-184040.log b/logs/20261107-184040/amd64/qemu-amd64-20261107-184040.log new file mode 100644 index 00000000..6bc54f35 --- /dev/null +++ b/logs/20261107-184040/amd64/qemu-amd64-20261107-184040.log @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:16ff21b314d76f58304fefba58921194b848b2a7521a91b6a9bf6ac72b01a368 +size 6637 diff --git a/logs/20261107-184241/aarch64/qemu-aarch64-20261107-184241.log b/logs/20261107-184241/aarch64/qemu-aarch64-20261107-184241.log new file mode 100644 index 00000000..c24e88d0 --- /dev/null +++ b/logs/20261107-184241/aarch64/qemu-aarch64-20261107-184241.log @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:72acbac8e5db7027b26c1b9689116d434368421961330f6199cbdd6116c449e1 +size 5602 diff --git a/logs/20261107-184616/riscv64/qemu-riscv64-20261107-184616.log b/logs/20261107-184616/riscv64/qemu-riscv64-20261107-184616.log new file mode 100644 index 00000000..20ab5c94 --- /dev/null +++ b/logs/20261107-184616/riscv64/qemu-riscv64-20261107-184616.log @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:a52383c54ba6f2e57dbbdc6115a66d21a877661ae8b053da2748d1dc6f297c07 +size 7993 diff --git a/logs/20261107-184753/amd64/qemu-amd64-20261107-184753.log b/logs/20261107-184753/amd64/qemu-amd64-20261107-184753.log new file mode 100644 index 00000000..28491434 --- /dev/null +++ b/logs/20261107-184753/amd64/qemu-amd64-20261107-184753.log @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:6632ed60fecd61ebdb02cced5f7dc99b821046108ebce0b32e6bf2e94a8fc82d +size 6708 diff --git a/logs/20261107-185450/isabelle/isabelle-20261107-185450.log b/logs/20261107-185450/isabelle/isabelle-20261107-185450.log new file mode 100644 index 00000000..86e1a00e --- /dev/null +++ b/logs/20261107-185450/isabelle/isabelle-20261107-185450.log @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:ea0e788b3fc07f4dd6688a54f4409002ae96f2e1f48d8833f7abf243264a61a2 +size 7783 From 4a125cdd217102fd96e85d4c132f62212f33342e Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 7 Nov 2026 18:56:16 +0000 Subject: [PATCH 3/5] release v4.0.0-alpha.2: run the acceptance check on #130 The commits before this one carry [skip ci], which Gitea also applies to the pull request's checks. No change to the tree. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2 From cabe974872f9988d66f51cfa903dc483f4c492d2 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 7 Nov 2026 18:59:34 +0000 Subject: [PATCH 4/5] release v4.0.0-alpha.2: start #130's acceptance check The commit before this one quoted the skip marker in its message, so Gitea skipped its checks too. No change to the tree. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2 From 37f62d688b99db395df296278428a8f62259dc2f Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 7 Nov 2026 19:15:04 +0000 Subject: [PATCH 5/5] logs: three riscv64 boots of v4.0.0-alpha.2, looking for run 197's failure Acceptance run 197 (#130) failed one riscv64 check: no 'Boot disk: not a StarshipOS stick' line, with POST, the identity and the prompt all passing. Booted three more times here on the same tree: each printed the line and passed (4 of 4 with logs/20261107-184616). The Zuse stick has no ESP (--esp-mib 0), so the firmware cannot have booted from it; the serial capture losing or garbling the line is what is left to check, against run 197's own log. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2 --- experiments/bare_metal/runs/doe-riscv64-20261107-190906.csv | 0 experiments/bare_metal/runs/doe-riscv64-20261107-191105.csv | 0 experiments/bare_metal/runs/doe-riscv64-20261107-191304.csv | 0 logs/20261107-190906/riscv64/qemu-riscv64-20261107-190906.log | 3 +++ logs/20261107-191105/riscv64/qemu-riscv64-20261107-191105.log | 3 +++ logs/20261107-191304/riscv64/qemu-riscv64-20261107-191304.log | 3 +++ 6 files changed, 9 insertions(+) create mode 100644 experiments/bare_metal/runs/doe-riscv64-20261107-190906.csv create mode 100644 experiments/bare_metal/runs/doe-riscv64-20261107-191105.csv create mode 100644 experiments/bare_metal/runs/doe-riscv64-20261107-191304.csv create mode 100644 logs/20261107-190906/riscv64/qemu-riscv64-20261107-190906.log create mode 100644 logs/20261107-191105/riscv64/qemu-riscv64-20261107-191105.log create mode 100644 logs/20261107-191304/riscv64/qemu-riscv64-20261107-191304.log diff --git a/experiments/bare_metal/runs/doe-riscv64-20261107-190906.csv b/experiments/bare_metal/runs/doe-riscv64-20261107-190906.csv new file mode 100644 index 00000000..e69de29b diff --git a/experiments/bare_metal/runs/doe-riscv64-20261107-191105.csv b/experiments/bare_metal/runs/doe-riscv64-20261107-191105.csv new file mode 100644 index 00000000..e69de29b diff --git a/experiments/bare_metal/runs/doe-riscv64-20261107-191304.csv b/experiments/bare_metal/runs/doe-riscv64-20261107-191304.csv new file mode 100644 index 00000000..e69de29b diff --git a/logs/20261107-190906/riscv64/qemu-riscv64-20261107-190906.log b/logs/20261107-190906/riscv64/qemu-riscv64-20261107-190906.log new file mode 100644 index 00000000..4d1bf87c --- /dev/null +++ b/logs/20261107-190906/riscv64/qemu-riscv64-20261107-190906.log @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:ce8ff0557f7784c52621ceda6bb14d1cc95e2482aea02876a7fc17605f64e9eb +size 7993 diff --git a/logs/20261107-191105/riscv64/qemu-riscv64-20261107-191105.log b/logs/20261107-191105/riscv64/qemu-riscv64-20261107-191105.log new file mode 100644 index 00000000..8684f46a --- /dev/null +++ b/logs/20261107-191105/riscv64/qemu-riscv64-20261107-191105.log @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:d160ab458d8f4a422051dc13cc707f7c1b8fc97ba73c285316b7315cbe827237 +size 7993 diff --git a/logs/20261107-191304/riscv64/qemu-riscv64-20261107-191304.log b/logs/20261107-191304/riscv64/qemu-riscv64-20261107-191304.log new file mode 100644 index 00000000..67b56259 --- /dev/null +++ b/logs/20261107-191304/riscv64/qemu-riscv64-20261107-191304.log @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:3074fcf7f8b8a8dd33fee887877dc51965eb461e49f1bf2c134d2ecc402342bf +size 7993