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
Scheduled runs use -SNAPSHOT version suffix and publish to
starshipos-snapshots Nexus repo instead of starshipos-releases.
Push-to-master releases continue to use -<sha> suffix.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Runs api-docs (Doxygen → AsciiDoc), docs-latex (AsciiDoc → LaTeX via
asciidoctor), and math-companion (LaTeX → PDF) in a dedicated job
parallel to builds and Isabelle verification. Installs doxygen, Ruby +
asciidoctor-latex gem, and texlive. Uploads docs as a Gitea artifact
on every run regardless of pass/fail.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Runs StarForth session (52 theories) in parallel with the board build
matrix. Caches the Isabelle2024 installation (~800MB) and the compiled
heaps keyed on proof/**/*.thy + ROOT, so only theory changes trigger a
full rebuild. Uploads the build log as an artifact on every run
(pass or fail) for audit.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Builds all boards (qemu, pc, pi4, pi5, milkv) in parallel. Installs
cross-compilers (aarch64-linux-gnu, riscv64-linux-gnu) and clang-18
for the aarch64 loader. Packs ISO (amd64/aarch64) and GPT image (riscv64).
On master push, publishes to Nexus starshipos-releases using Maven
coordinates org.f18:kernel:<version>-<sha>:<board> and
org.f18:starforth:<version>-<sha>:<board>.
CROSS_COMPILE wired into StarForth Makefile via mk/boards.mk so
make T=pi4 picks up aarch64-linux-gnu-gcc automatically.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
rajames