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
Captain Bob, 2026-11-07: "I also want that rebuilds block other jobs
always." acceptance, nightly and release shared the group qemu; now
runner-image, build and nightly-docs do too, so a rebuild of the runner
image (on the host's Docker daemon) never overlaps another job, whatever
the runner's capacity (#121). On this server every CI run is then one at a
time.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
The workflows' containers are now lithosananke-runner:72b6cf370db1, built
and published by runner-image.yml, with everything init installs and Maven
already in it; the install steps are gone, except the documents' packages in
nightly-docs.yml and release.yml. The registry refuses anonymous pulls, so
each job pulls with PACKAGES_TOKEN.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
build.yml, as master had it, could not run here: it called
Makefile.starkernel and make T=<board> (the tree has kernel/Makefile
and TARGET=<board>), listed a Pi 4 with no port, published "releases"
under org/f18 on every push, installed Isabelle2024 (the proofs need
Isabelle2025-2) from a mirror that answered 503, and duplicated the
nightlies with its own 02:00 schedule. Now it is the check on every
push to master and StarForth-v4.0.0 and every PR into master: each
board's image (make boot_image TARGET=PC|RASPI|MILKV, xz'd, kept with
its SBOM) and make -C v4 test, both cell widths. It publishes nothing;
the nightlies and release.yml do.
Every job of every workflow now names its container,
gitea/runner-images:ubuntu-24.04-v26.11.03: the runner maps
ubuntu-latest to node:20-bullseye, Debian 11, where every job of PR
#30's runs failed at its first apt-get, and which has no
qemu-efi-riscv64 and a far older QEMU and compilers than the Ubuntu
24.04 all of this was tested on. Node is needed in the image:
actions/checkout and upload-artifact run inside the job's container.
The dated tag keeps a run from changing under an image update.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
For PR #30. master's 9 commits since the fork (T= board selection,
mk/boards.mk, build.yml, the nightly workflows) conflicted in four
files; each is resolved to the branch's version:
.gitea/workflows/nightly.yml added on both; master's copy named
.gitea/workflows/nightly-docs.yml the branch in its checkout, the
branch's builds the default branch
Makefile master's T= and mk/boards.mk against
kernel/Makefile the branch's TARGET=<board> and
boards/; master's edits were to
Makefile.starkernel, renamed here
The two workflows' header comment now says they build master.
Merged cleanly from master: build.yml (its board matrix, Nexus publish
and 02:00 nightly; it still calls Makefile.starkernel and make
T=<board>, which this tree does not have -- #18) and mk/boards.mk
(nothing here includes it).
Against the branch the merge changes only those CI files and
mk/boards.mk: no kernel, v4 or Makefile source, so the build is the one
accepted on 2026-11-06.
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
Gitea runs schedules from the default branch only, so until StarForth-v4.0.0
is merged here, master carries copies of that branch's two nightly
workflows, identical to them but for the checkout's ref:
nightly.yml 03:00 UTC: the acceptance protocol (zuse amd64, aarch64,
riscv64; the PC stick loaded high; dict_hash equal on the
three; test-32), the Isabelle/HOL proofs, the board images,
then org.starship:kernelImage:<LITHOS_VERSION>-SNAPSHOT --
classifiers pc (iso), raspi5, milkv (img.xz), logs
nightly-docs.yml 04:00 UTC: the book, the formal volumes, the API reference
-> org.starship:documentation:<LITHOS_VERSION>-SNAPSHOT
Both publish to starshipos-snapshots as ci-publisher (secret
NEXUS_CI_PASSWORD), and only if every stage before passed. The work is that
branch's scripts/nightly.sh. At the merge, take that branch's copies (this
ref line goes). build.yml's own 02:00 schedule is untouched.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
Claude