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
Measured here (Isabelle2025-2, one thread): HOL-Library from scratch takes
~11 minutes and peaks at ~5.3 GiB -- what nightly 174 was killed doing; the
StarForth session on a built HOL-Library takes under a minute and ~2.2 GiB.
The image builds HOL-Library once into Isabelle's own heaps, so every job
finds it.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
Nightly 174 passed acceptance, then Isabelle was killed building HOL-Library
(exit 137, out of memory on the runner), and the images were never built or
published. The proofs check the theories, not the images: they now run after
the publish, whatever happened before them, and a failure still turns the run
red. Their log stays in the run's logs artifact. A release still runs them
before it publishes.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
scripts/nightly.sh, one stage per call, a step each in the workflows:
accept <amd64|aarch64|riscv64|stick-high> the acceptance protocol --
qemu_session.py zuse, and stick_zuse --target qemu-stick-high;
after the last, dict_hash must be equal on the three
test-32 make -C v4 test-32
proofs isabelle build -c -D proof/ (StarForth checked afresh each run)
images the Pi 5 and Mars images, xz for Raspberry Pi Imager
publish org.starship:kernelImage: pc (iso), raspi5, milkv (img.xz),
logs (tar.gz: this run's serial logs, proof log, DoE CSVs)
docs, publish-docs book, vol1-3, api -> org.starship:documentation
.gitea/workflows/nightly.yml (03:00) and nightly-docs.yml (04:00) publish
<LITHOS_VERSION>-SNAPSHOT to starshipos-snapshots; release.yml, on a tag
v*, builds and publishes both to starshipos-releases at the tag's version,
refusing a tag that is not v<LITHOS_VERSION>. Until this branch is merged
to master, master carries copies of the two nightlies naming it.
make init: INIT_DOCS=0 leaves out TeX and Doxygen, INIT_PROOFS=0 Isabelle.
Checked here, stage by stage, in order: the four acceptance boots PASS,
dict_hash 0xfec8c47cfc6f437f on the three, test-32 0 failures, StarForth
proved (0:00:41), images built; publish to a local file:// repository,
and the images' publish to Nexus starshipos-snapshots read back byte for
byte. The docs stage and publish-docs: not yet checked when committed.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
Three stages, each a step of the nightly workflow:
boot <amd64|aarch64|riscv64> qemu_session.py headless, one QEMU at a time,
in the acceptance order; amd64 keeps the ISO it
booted as build/nightly/StarshipOS.iso
images make boot_image for RASPI (Pi 5) and MILKV
(Mars) -> raspi5.img.xz, MilkV.img.xz (for
Raspberry Pi Imager), and SHA256SUMS
publish <url> mvn deploy:deploy-file (maven-deploy-plugin
3.1.2): org.starship:kernelImage:
<LITHOS_VERSION>-SNAPSHOT, classifier pc (iso),
raspi5 and milkv (img.xz), in one deploy
Classifier by board, not ISA: two aarch64 boards would collide. No Pi 4:
there is no BCM2711 port. QEMU boots the aarch64 and riscv64 kernels, not
the Pi 5 and Mars images, which are for hardware QEMU does not model.
make init takes INIT_DOCS=0: without the TeX and Doxygen packages and
Isabelle, which an image build does not need.
Checked here: the three boot checks pass (logs in the next commit), the
images build, and publish to a local file:// repository gives the
timestamped snapshot files, the POM and maven-metadata.xml with one
snapshotVersion per classifier. Not checked: Nexus itself.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
Claude