Merge pull request 'release: v4.0.0-alpha.3; the proofs run capped to fit the server' (#132) from StarForth-v4.0.0 into master

On 50d2bc98 (LithosAnanke v4.0.0-alpha.3), in this session, one QEMU at a
time in the foreground: amd64 logs/20261107-195526, aarch64 -195725,
riscv64 -200055 (POST 538/538, dict_hash=0xfec8c47cfc6f437f on all three),
the stick loaded high, test-32 (39 programs, 0 failures); the proofs
through the capped stage, logs/20261107-195341 (47 s, ~1.8 GiB).

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

.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

CHANGELOG.md

@@ -1,5 +1,21 @@
 # Changelog
 
+## 2026-11-07 — LithosAnanke v4.0.0-alpha.3: the first published alpha
+
+`v4.0.0-alpha.2` (`2d43db25`) used the image's HOL-Library as intended, but its release run (200) ran
+the proofs with Isabelle's defaults -- Java's heap up to 4 GiB, a thread per CPU -- and they were
+killed in the StarForth session. Nothing was published; the tag stays where it is. The proofs now run
+capped (`scripts/nightly.sh proofs`: one thread, Java 512 MiB, Poly/ML 900 MiB; 47 s, ~1.8 GiB), and
+`v4.0.0-alpha.3` is the first alpha published. `docs/fabric/FABRIC-3.md` XLVII.6.
+
+## 2026-11-07 — LithosAnanke v4.0.0-alpha.2: not published
+
+`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

docs/fabric/FABRIC-3.md

@@ -6165,3 +6165,29 @@ 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.
+
+### 6. v4.0.0-alpha.2 not published either; v4.0.0-alpha.3
+
+PR #130 merged (`2d43db25`, acceptance run 199; run 197 before it failed one riscv64 check, #131);
+`v4.0.0-alpha.2` tagged there. Its release run (200) passed acceptance and used the image's
+Isabelle and HOL-Library, as XLVII.5 meant -- then the StarForth session was killed (exit 137) in
+the proofs: Isabelle ran with its defaults, Java's heap up to 4 GiB and a thread per CPU, more than
+the server (3.8 GiB, ~2.3 GiB free with the wikis stopped; perhaps a per-job cap besides). Capped
+-- one thread, Java 512 MiB, Poly/ML 900 MiB, in a settings file of a home made for the run, its
+heaps linked to the user's -- the session passes in 47 s at ~1.8 GiB, through
+`scripts/nightly.sh proofs` itself (`logs/20261107-195341`). Nothing was published. Ruled (Captain
+Bob, 2026-11-07): the tag stays; `LITHOS_VERSION` `4.0.0-alpha.3`, the first published alpha; the
+review list begun meanwhile goes to the milestone v4.0.0-alpha.4.

kernel/Makefile

@@ -95,6 +95,13 @@ 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).
+#   v4.0.0-alpha.3 — the first published alpha: v4.0.0-alpha.2 (2d43db25) kept the image's
+#             HOL-Library, but its proofs ran with Isabelle's defaults (Java 4 GiB, a thread per CPU)
+#             and were killed in the StarForth session; nothing was published, the tag stays. The
+#             proofs now run capped (scripts/nightly.sh: 1 thread, Java 512 MiB, ML 900 MiB).
 # 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 +110,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.3
 
 # ==============================================================================
 # BUILD PATHS

scripts/nightly.sh

@@ -16,7 +16,8 @@
 #   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 proofs
-#       isabelle build -c -D proof/: the StarForth session checked afresh every run, whatever is
+#       isabelle build -c -D proof/, capped to fit the server (one thread, small heaps): the StarForth
+#       session checked afresh every run, whatever is
 #       cached (HOL-Library is reused: the CI image has it built, ci/runner-image); its log is
 #       logs/<TS>/isabelle/, as a boot's is.
 #   scripts/nightly.sh images
@@ -121,7 +122,19 @@ proofs)
     need "$OUT/.started"
     ts=$(date -u +%Y%m%d-%H%M%S)
     mkdir -p "logs/$ts/isabelle"
-    isabelle build -c -v -D proof/ 2>&1 | tee "logs/$ts/isabelle/isabelle-$ts.log"
+    # Within the server's memory: one thread, Java's heap 512 MiB, Poly/ML's 900 MiB -- the
+    # StarForth session peaks at ~1.7 GiB so (46 s), where Isabelle's defaults (Java 4 GiB, a thread
+    # per CPU) were killed (release run 200, v4.0.0-alpha.2). The caps go in a settings file of a
+    # home made for the run; its heaps are the user's own, linked in, and the image's HOL-Library
+    # is found as always, with Isabelle itself.
+    isahome=$(mktemp -d)
+    isaver=$(isabelle getenv -b ISABELLE_IDENTIFIER)
+    mkdir -p "$isahome/.isabelle/$isaver/etc" "$HOME/.isabelle/$isaver/heaps"
+    ln -s "$HOME/.isabelle/$isaver/heaps" "$isahome/.isabelle/$isaver/heaps"
+    printf '%s\n' 'ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms128m -Xmx512m -Xss16m"' \
+                  'ML_OPTIONS="--minheap 200 --maxheap 900"' > "$isahome/.isabelle/$isaver/etc/settings"
+    USER_HOME="$isahome" isabelle build -o threads=1 -c -v -D proof/ 2>&1 | tee "logs/$ts/isabelle/isabelle-$ts.log"
+    rm -rf "$isahome"
     ;;
 images)
     need "$OUT/StarshipOS.iso"