Merge pull request 'ci: the workflows run in the runner image with HOL-Library' (#128) from StarForth-v4.0.0 into master

The image runner-image.yml built from master 4f675c8b (run 193): what init
installs, Maven, and the HOL-Library heap fetched prebuilt (checksum OK, 4.8
s), so the proofs build only the StarForth session. Its acceptance run is
this PR's.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2

.gitea/workflows/acceptance.yml

@@ -18,7 +18,8 @@ on:
   workflow_dispatch:
 
 concurrency:
-  group: qemu                     # one QEMU at a time on the runner: shared with nightly.yml and release.yml
+  group: qemu                     # every workflow shares this one group: one run at a time,
+                                  # a runner-image rebuild included (Captain Bob, 2026-11-07)
   cancel-in-progress: false
 
 jobs:
@@ -26,7 +27,7 @@ jobs:
     name: Acceptance
     runs-on: ubuntu-latest
     container:
-      image: gitea.starshipos-f18.org/rajames/lithosananke-runner:72b6cf370db1   # ci/runner-image (#120)
+      image: gitea.starshipos-f18.org/rajames/lithosananke-runner:4f675c8b75b2   # ci/runner-image (#120)
       credentials:                # the registry refuses anonymous pulls
         username: rajames
         password: ${{ secrets.PACKAGES_TOKEN }}

.gitea/workflows/build.yml

@@ -9,14 +9,20 @@ name: Build
 on:
   push:
     branches: [StarForth-v4.0.0]   # not master: what reaches it has just passed acceptance (#119)
+    paths-ignore: ['site/**']        # the websites (site/) build nothing here; each run is ~17 min on
+                                     # the server the wikis share (Captain Bob, 2026-11-07)
   workflow_dispatch:
 
+concurrency:
+  group: qemu                     # every workflow shares this one group (Captain Bob, 2026-11-07: a
+  cancel-in-progress: false       # runner-image rebuild blocks other jobs, always): one run at a time
+
 jobs:
   image:
     name: Image ${{ matrix.board }}
     runs-on: ubuntu-latest
     container:
-      image: gitea.starshipos-f18.org/rajames/lithosananke-runner:72b6cf370db1   # ci/runner-image (#120)
+      image: gitea.starshipos-f18.org/rajames/lithosananke-runner:4f675c8b75b2   # ci/runner-image (#120)
       credentials:                # the registry refuses anonymous pulls
         username: rajames
         password: ${{ secrets.PACKAGES_TOKEN }}
@@ -64,7 +70,7 @@ jobs:
     name: v4 tests (32- and 64-bit cells)
     runs-on: ubuntu-latest
     container:
-      image: gitea.starshipos-f18.org/rajames/lithosananke-runner:72b6cf370db1   # ci/runner-image (#120)
+      image: gitea.starshipos-f18.org/rajames/lithosananke-runner:4f675c8b75b2   # ci/runner-image (#120)
       credentials:                # the registry refuses anonymous pulls
         username: rajames
         password: ${{ secrets.PACKAGES_TOKEN }}

.gitea/workflows/nightly-docs.yml

@@ -14,12 +14,16 @@ on:
     - cron: '0 4 * * *'        # 04:00 UTC, after the images (nightly.yml, 03:00)
   workflow_dispatch:
 
+concurrency:
+  group: qemu                     # every workflow shares this one group (Captain Bob, 2026-11-07: a
+  cancel-in-progress: false       # runner-image rebuild blocks other jobs, always): one run at a time
+
 jobs:
   docs:
     name: Book, volumes, API reference
     runs-on: ubuntu-latest
     container:
-      image: gitea.starshipos-f18.org/rajames/lithosananke-runner:72b6cf370db1   # ci/runner-image (#120)
+      image: gitea.starshipos-f18.org/rajames/lithosananke-runner:4f675c8b75b2   # ci/runner-image (#120)
       credentials:                # the registry refuses anonymous pulls
         username: rajames
         password: ${{ secrets.PACKAGES_TOKEN }}

.gitea/workflows/nightly.yml

@@ -20,7 +20,8 @@ on:
   workflow_dispatch:
 
 concurrency:
-  group: qemu                     # one QEMU at a time on the runner: shared with acceptance.yml
+  group: qemu                     # every workflow shares this one group: one run at a time,
+                                  # a runner-image rebuild included (Captain Bob, 2026-11-07)
   cancel-in-progress: false
 
 jobs:
@@ -28,7 +29,7 @@ jobs:
     name: Acceptance, images, proofs
     runs-on: ubuntu-latest
     container:
-      image: gitea.starshipos-f18.org/rajames/lithosananke-runner:72b6cf370db1   # ci/runner-image (#120)
+      image: gitea.starshipos-f18.org/rajames/lithosananke-runner:4f675c8b75b2   # ci/runner-image (#120)
       credentials:                # the registry refuses anonymous pulls
         username: rajames
         password: ${{ secrets.PACKAGES_TOKEN }}

.gitea/workflows/release.yml

@@ -14,7 +14,8 @@ on:
     tags: ['v*']
 
 concurrency:
-  group: qemu                     # one QEMU at a time on the runner: shared with acceptance.yml
+  group: qemu                     # every workflow shares this one group: one run at a time,
+                                  # a runner-image rebuild included (Captain Bob, 2026-11-07)
   cancel-in-progress: false
 
 jobs:
@@ -22,7 +23,7 @@ jobs:
     name: Release ${{ github.ref_name }}
     runs-on: ubuntu-latest
     container:
-      image: gitea.starshipos-f18.org/rajames/lithosananke-runner:72b6cf370db1   # ci/runner-image (#120)
+      image: gitea.starshipos-f18.org/rajames/lithosananke-runner:4f675c8b75b2   # ci/runner-image (#120)
       credentials:                # the registry refuses anonymous pulls
         username: rajames
         password: ${{ secrets.PACKAGES_TOKEN }}

.gitea/workflows/runner-image.yml

@@ -17,6 +17,10 @@ on:
     paths: ['ci/runner-image/**', 'Makefile']
   workflow_dispatch:
 
+concurrency:
+  group: qemu                     # every workflow shares this one group (Captain Bob, 2026-11-07: a
+  cancel-in-progress: false       # runner-image rebuild blocks other jobs, always): one run at a time
+
 jobs:
   image:
     name: Build and publish the runner image
@@ -44,7 +48,9 @@ jobs:
           tag=$(git rev-parse --short=12 HEAD)
           ctx=$(mktemp -d)                                  # not the repository: 7 GB of context
           cp -r Makefile boards ci/runner-image/Dockerfile "$ctx/"
-          docker build -t "$img:$tag" "$ctx"
+          tok=$(mktemp); printf '%s' "$TOKEN" > "$tok"          # the HOL-Library heap's download (Dockerfile)
+          docker build --secret id=pkgtoken,src="$tok" -t "$img:$tag" "$ctx"
+          rm -f "$tok"
           echo "$TOKEN" | docker login gitea.starshipos-f18.org -u rajames --password-stdin
           docker push "$img:$tag"
           echo "Published $img:$tag"

CHANGELOG.md

@@ -1,5 +1,18 @@
 # Changelog
 
+## 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
+board boots by default, with v3 a boot argument away. The kernel's version goes from 2.1.0 to the
+4.x working line (Captain Bob, 2026-11-07); the engine stays 3.2.0. Accepted in full before the tag:
+amd64, aarch64 and riscv64 to `[zuse@Hera] ok>` with POST 538/538 and one `dict_hash`
+(`0xfec8c47cfc6f437f`), the PC stick loaded high, `test-32` (39 programs, 0 failures), and the
+Isabelle/HOL proofs. An alpha: the v4.0.0 milestone's own definition -- parity with v3's vocabulary,
+K=1.0 measured on v4, the hosted mesh, Verilator -- is still open, and the capsules are unsigned until
+the StarshipOS CA is made (FABRIC-3.md XLVI). Also today: CI in a prebuilt runner image, the
+nightly's proofs no longer able to hold back its images, and the .com and .org websites. Full record:
+`docs/fabric/FABRIC-3.md` XLVII.
+
 ## 2026-11-07 — CI jobs start ready: the runner image
 
 The CI jobs now run in `lithosananke-runner` (`ci/runner-image`, #120), an image with everything

ci/runner-image/Dockerfile

@@ -12,8 +12,19 @@ WORKDIR /opt/starship-init
 RUN make --no-print-directory ARCH=amd64,aarch64,riscv64 init INIT_DOCS=0 \
  && DEBIAN_FRONTEND=noninteractive apt-get install -y -qq maven default-jre-headless \
  && rm -rf /var/lib/apt/lists/* /opt/starship-init/build/cache/downloads
-# HOL-Library, built once here, into Isabelle's own heaps (system_heaps), so the nightly's proofs
-# build only the StarForth session: ~2.2 GiB and under a minute, where HOL-Library from scratch
-# takes ~5.3 GiB and ~11 minutes -- more than the runner had (nightly 174, killed).
-RUN isabelle build -b -o system_heaps -o threads=1 HOL-Library
+# HOL-Library, prebuilt, into Isabelle's own heaps, so the proofs build only the StarForth session
+# (~2.2 GiB, under a minute). Built from scratch it takes ~5.3 GiB (nightly 174 was killed doing it),
+# and capped it still needs ~2.6-3.3 GiB: more than the server has. So it is built once, elsewhere,
+# by the same Isabelle2025-2, and fetched from this repository's package registry, its checksum
+# pinned here (FABRIC-3.md XLVII). Isabelle ships its own HOL heap the same way. The token is a
+# build secret (runner-image.yml): it is in neither the image nor its history.
+ARG HOL_LIBRARY_URL=https://gitea.starshipos-f18.org/api/packages/rajames/generic/isabelle-hol-library/Isabelle2025-2/hol-library-Isabelle2025-2.tar.xz
+ARG HOL_LIBRARY_SHA256=bb24784664def9379e5db27f88802e3679b8e1c628177f6fbe7084e999cb339e
+RUN --mount=type=secret,id=pkgtoken \
+    curl -fsSL -H "Authorization: token $(cat /run/secrets/pkgtoken)" -o /tmp/hol-library.tar.xz "$HOL_LIBRARY_URL" \
+ && echo "$HOL_LIBRARY_SHA256  /tmp/hol-library.tar.xz" | sha256sum -c - \
+ && heaps=$(isabelle getenv -b ISABELLE_HEAPS_SYSTEM) && mkdir -p "$heaps" \
+ && xz -dc /tmp/hol-library.tar.xz | tar -C "$heaps" -xf - \
+ && rm /tmp/hol-library.tar.xz \
+ && test -s "$heaps/polyml-5.9.2_x86_64_32-linux/HOL-Library"
 WORKDIR /

docs/fabric/FABRIC-3.md

@@ -6105,3 +6105,63 @@ With a CA made by `make-ca.sh` in a scratch directory (not the real one): `opens
 chain OK; `make-ca.sh` refuses a second run; `mkcapsule` with the signing key -- "signing key
 matches"; with the root's key -- refused; with a key and no certificate -- refused; with no key --
 unsigned, as before. The acceptance with the real certificate is the PR's.
+
+## XLVII. LithosAnanke v4.0.0-alpha.1: the first alpha release (2026-11-07)
+
+### 1. Ruled
+
+Captain Bob, 2026-11-07: "next on the list is do a tag/release of v4.0.0" -- then, on what the number
+names: "StarForth version stays the same ... Kernel is 4.0.0. This is our first alpha release." The
+tag names the kernel (`release.yml`: `v<LITHOS_VERSION>`), so:
+
+- `LITHOS_VERSION` 2.1.0 -> **4.0.0-alpha.1**; the tag is `v4.0.0-alpha.1`; Nexus takes
+  `org.starship:kernelImage:4.0.0-alpha.1` and `org.starship:documentation:4.0.0-alpha.1`.
+- The engine's `VERSION` stays **3.2.0**.
+- The versioning policy (`kernel/Makefile`, FABRIC-3.5.md XXX): 4.x is a working line (even major).
+  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. Alphas are numbered: a release repository takes each version once.
+- The v4.0.0 milestone is unchanged: its definition (v4 equivalent to v3, K=1.0 on all three host
+  ISAs, a hosted mesh, Verilator co-simulation) is what 4.0.0 itself will be; nine of its issues
+  are open. This is an alpha of it.
+- The release is built and proved here first (this session, 15 GiB), its logs committed; the
+  server's release run follows once it can pass -- the proofs need HOL-Library in the runner image.
+  The capsules are unsigned for this release.
+
+### 2. Verified (this session, `b7534107`, before the tag)
+
+- amd64 (`logs/20261107-150809`), aarch64 (`-151023`), riscv64 (`-151359`): `LithosAnanke
+  v4.0.0-alpha.1 <arch>`, `[zuse@Hera] ok>`, `PARITY:V4_POST tests=538 pass=538 fail=0`,
+  `POST: PASSED`, Zuse identity confirmed, `PARITY:V4_SYSTEM word_count=317
+  dict_hash=0xfec8c47cfc6f437f` on all three.
+- The PC stick loaded high (`logs/20261107-151539`): the same, from the stick, no fault.
+- `make -C v4 test-32`: 39 programs, 0 failures.
+- The Isabelle/HOL proofs (`logs/20261107-152312/isabelle`).
+- Each v4 capsule logs `signature: no root key (cert not found/parseable)`: the kernel looks for the
+  StarshipOS Capsule Signing certificate (XLVI), which is not in the tree until `ci/pki/make-ca.sh`
+  has run. A warning, as "missing (unsigned)" was before; nothing is refused.
+
+### 3. The StarshipOS CA, and acceptance again (`4ca935d8`)
+
+`ci/pki/make-ca.sh` ran on the CI box (2026-11-07 16:50 UTC): the StarshipOS Root CA there, the
+signing key in the secret `CAPSULE_SIGN_KEY`, and the certificate -- O=StarshipOS, CN=StarshipOS
+Capsule Signing, issued by the root, 2026-11-07 to 2036-11-06, `CA:TRUE, pathlen:0`, SHA-256 of the
+DER `13a28dda...029b9a6c` -- in the tree as `capsules/pki/starshipos-intermediate.der`, the snakeoil
+intermediate out of it. The tree changed, so the protocol ran again here: amd64
+(`logs/20261107-165611`), aarch64 (`-165817`), riscv64 (`-170149`) -- POST 538/538,
+`dict_hash=0xfec8c47cfc6f437f` on all three; the stick loaded high (`-170326`); `test-32`, 39
+programs, 0 failures; the proofs (`-171020`). Each capsule now logs `signature: missing (unsigned)`:
+the kernel found and read the StarshipOS certificate (it said "no root key" without it), and this
+session has no key to sign with. CI signs with the secret: the PR's acceptance and the release are
+where every capsule first verifies.
+
+### 4. HOL-Library, prebuilt
+
+The runner image was to build HOL-Library itself (XLVI's companion change, `4ae1f759`); the server
+cannot: from scratch it peaks at ~5.3 GiB, and with Poly/ML capped at 1.6 GiB the build still needs
+Isabelle's Java side at ~1 GiB (at 384 MiB it ran out and hung) -- 2.6-3.3 GiB against the server's
+3.8 GiB in all, ~2.3 GiB free with both wikis stopped. So the heap built here by the same
+Isabelle2025-2 (HOL-Library and its build database) is a package in this repository's registry,
+`generic/isabelle-hol-library/Isabelle2025-2/hol-library-Isabelle2025-2.tar.xz` (45 MB, SHA-256
+`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).

kernel/Makefile

@@ -89,6 +89,12 @@ endif
 #   v2.2.0  — amd64 bare-metal bring-up (Beelink SER5)
 #   v2.x    — further working releases; riscv64 / aarch64 board bring-up
 #   v3.0.0  — FIRST LTS, when and only when FABRIC-3.5.md §XXX.5's 5 criteria are met
+#   v4.0.0-alpha.1 — the first alpha release (Captain Bob, 2026-11-07: "Kernel is 4.0.0. This is
+#             our first alpha release"): v4, the F18 engine, the default system. The kernel goes
+#             from v2.1.0 straight to the 4.x working line (even: breaking changes land here);
+#             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.
 # 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
@@ -97,7 +103,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 ?= 2.1.0
+LITHOS_VERSION ?= 4.0.0-alpha.1
 
 # ==============================================================================
 # BUILD PATHS