release: v4.0.0-alpha.3; the proofs run capped to fit the server #132

2026-11-07T20:09:52Z

rajames commented

2026-11-07 20:09:52 +00:00

What and why

v4.0.0-alpha.3, the first published alpha. v4.0.0-alpha.2 (2d43db25) used the runner image's prebuilt HOL-Library as #130 meant, but its release run (200) ran the Isabelle/HOL proofs with Isabelle's defaults -- Java's heap up to 4 GiB, a thread per CPU -- and the StarForth session was killed (exit 137). Nothing was published.

Ruled (Captain Bob, 2026-11-07): the alpha.2 tag stays where it is; this PR

runs the proofs capped in scripts/nightly.sh proofs -- one thread, Java 512 MiB, Poly/ML 900 MiB, through a settings file of a home made for the run, its heaps linked to the user's (the image's HOL-Library is still found, with Isabelle itself): 47 s at ~1.8 GiB, run through the stage itself (logs/20261107-195341); the nightly and the release both use it;
sets LITHOS_VERSION to 4.0.0-alpha.3; after it merges, master is tagged v4.0.0-alpha.3.

Records: FABRIC-3 XLVII.6, CHANGELOG. Part of #17.

Acceptance

The Acceptance check runs on this pull request. By hand, on this tree:

Logs committed in logs/: amd64 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 capped proofs -195341
Hardware this was tried on, if any: none

The record

docs/fabric/FABRIC-3.md XLVII.6
CHANGELOG.md
Nothing in this PR is a fix nobody asked for (.claude/CLAUDE.md, Hard Rules)

🤖 Generated with Claude Code

https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2

## What and why **v4.0.0-alpha.3, the first published alpha.** `v4.0.0-alpha.2` (`2d43db25`) used the runner image's prebuilt HOL-Library as #130 meant, but its release run (200) ran the Isabelle/HOL proofs with Isabelle's defaults -- Java's heap up to 4 GiB, a thread per CPU -- and the StarForth session was killed (exit 137). Nothing was published. Ruled (Captain Bob, 2026-11-07): the alpha.2 tag stays where it is; this PR - runs the proofs capped in `scripts/nightly.sh proofs` -- one thread, Java 512 MiB, Poly/ML 900 MiB, through a settings file of a home made for the run, its heaps linked to the user's (the image's HOL-Library is still found, with Isabelle itself): 47 s at ~1.8 GiB, run through the stage itself (`logs/20261107-195341`); the nightly and the release both use it; - sets `LITHOS_VERSION` to `4.0.0-alpha.3`; after it merges, master is tagged `v4.0.0-alpha.3`. Records: FABRIC-3 XLVII.6, CHANGELOG. Part of #17. ## Acceptance The **Acceptance** check runs on this pull request. By hand, on this tree: - [x] Logs committed in `logs/`: amd64 `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 capped proofs `-195341` - [ ] Hardware this was tried on, if any: none ## The record - [x] `docs/fabric/FABRIC-3.md` XLVII.6 - [x] `CHANGELOG.md` - [x] Nothing in this PR is a fix nobody asked for (`.claude/CLAUDE.md`, Hard Rules) 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2

rajames added 2 commits 2026-11-07 20:09:55 +00:00

release: v4.0.0-alpha.3; the proofs run capped to fit the server 50d2bc98d9

v4.0.0-alpha.2's release run (200) was killed in the StarForth session:
Isabelle's defaults (Java 4 GiB, a thread per CPU). scripts/nightly.sh
proofs now runs one thread, Java 512 MiB, Poly/ML 900 MiB, through a
settings file of a home made for the run (heaps linked to the user's):
47 s, ~1.8 GiB, logs/20261107-195341. Nothing was published from alpha.2;
its tag stays. LITHOS_VERSION 4.0.0-alpha.3. FABRIC-3.md XLVII.6.

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

release v4.0.0-alpha.3: accepted in full, logs

Build / Image PC (push) Successful in 3m56s

Details

Build / v4 tests (32- and 64-bit cells) (push) Successful in 10m7s

Details

Build / Image MILKV (push) Successful in 8m45s

Details

Acceptance / Acceptance (pull_request) Successful in 15m37s

Details

Build / Image RASPI (push) Successful in 4m11s

Details

b8951bc26b

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

rajames merged commit 777f739708 into master

2026-11-07 20:52:53 +00:00

Sign in to join this conversation.

1 Participants

Notifications

Due Date

No due date set.

Dependencies

No dependencies set.

Reference: rajames/LithosAnanke#132