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

CHANGELOG.md

@@ -1,6 +1,14 @@
 # Changelog
 
-## 2026-11-07 — LithosAnanke v4.0.0-alpha.2: the first published alpha
+## 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

docs/fabric/FABRIC-3.md

@@ -6178,3 +6178,16 @@ packages, which also fetched Isabelle into the workspace and pointed `/usr/local
 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

@@ -98,6 +98,10 @@ endif
 #   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
@@ -106,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.2
+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"