- scripts/nightly.sh images builds the PC's USB stick too (make boot_image
TARGET=PC -> pc-stick.img.xz, in SHA256SUMS); publish sends it to Nexus
as classifier pc-stick. pc stays the ISO QEMU boots.
- scripts/nightly.sh gitea-release <tag>: the tag as a Gitea release -- a
pre-release for -alpha.N and the like -- notes from the tag's message with
the checksums, the images, SHA256SUMS, the documents and the StarshipOS
Root CA's certificate attached; run again, it adds only what is missing.
release.yml runs it after the Nexus publish, with the secret RELEASE_TOKEN.
Tested here: images builds pc-stick.img.xz (785 KB); gitea-release against
a stand-in Gitea API made a pre-release with the notes and ten files, and a
second run added nothing.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
v4.0.0-alpha.1's release run (196) was killed in the proofs: release.yml's
full `make init` fetched Isabelle into the workspace and pointed isabelle
at it, without the image's prebuilt HOL-Library, so the proofs built it
from scratch. Nothing was published. Ruled: the tag stays; release.yml runs
`init INIT_PROOFS=0`; LITHOS_VERSION 4.0.0-alpha.2, the first published
alpha. FABRIC-3.md XLVII.5, CHANGELOG.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
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 server cannot build it (5.3 GiB from scratch; capped, still 2.6-3.3
GiB against ~2.3 GiB free). The heap built here by the same Isabelle2025-2
is a generic package in this repository's registry (45 MB, SHA-256
bb247846...e999cb339e); the Dockerfile fetches it into Isabelle's system
heaps with the checksum pinned, the token a build secret. Portable: a
fresh Isabelle home with only this heap checks StarForth without
rebuilding HOL-Library. FABRIC-3.md XLVII.4.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
Five website commits queued five Build runs (183-187), ~17 minutes of image
builds each on the server both wikis run on; the .org stopped answering.
build.yml now ignores pushes whose changes are all under site/.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
Ruled by Captain Bob, 2026-11-07: "New root CA on the CI box. Valid
StarshipOS rather than snake oil intermediate."
- ci/pki/make-ca.sh makes the StarshipOS Root CA (its key stays on the CI
box) and the StarshipOS Capsule Signing intermediate it issues, and
stores the signing key as the secret CAPSULE_SIGN_KEY.
- The kernel finds the signing certificate by one name,
CAPSULE_SIGNING_CERT_NAME = pki:starshipos-intermediate.der. The
certificate itself lands once make-ca.sh has run; until then the
snakeoil intermediate is in the tree under its old name and the
capsules check as "no root key" (a warning, as "missing" was).
- mkcapsule refuses a signing key that is not that certificate's.
- SIGN_KEY has no default; acceptance, build, nightly and release set it
from the secret.
FABRIC-3.md XLVI.
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
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
Captain Bob, 2026-11-06: a small server, a little sluggish. Each change
cost about an hour of runner time; the gate itself is about 15 minutes.
#119 -- build.yml runs on pushes to the working branch only. What
reaches master arrives through a PR whose content just passed
acceptance; checking it again cost ~23 minutes after every merge.
#120, first step -- ci/runner-image/Dockerfile: gitea/runner-images'
Ubuntu 24.04 (with Node, for the actions) plus what
make ARCH=amd64,aarch64,riscv64 init INIT_DOCS=0 installs -- run from
the Makefile itself, not a copied list -- and Maven for publishing.
.gitea/workflows/runner-image.yml builds it and publishes it to the
package registry as lithosananke-runner:<commit>. The workflows switch
to it in a later change, once it is published and has passed
acceptance. It needs the runner to lend jobs its Docker daemon
(container.docker_host: automount) and a PACKAGES_TOKEN secret, unless
the Actions token may publish packages.
make init does git lfs install --local only inside a checkout: the
image build is not one.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
Captain Bob, 2026-11-06: what a developer runs, what CI runs and what
the nightly runs are one process, and "failures should not be allowed
to be merged to master".
acceptance.yml runs on every PR into master (opened, pushed to,
reopened): .claude/CLAUDE.md's acceptance protocol through the same
scripts/nightly.sh stages -- amd64, aarch64, riscv64 to [zuse@Hera]
ok>, the PC stick loaded high (and the three agree on dict_hash), then
make -C v4 test-32 -- one QEMU at a time, in one job. Its logs and DoE
CSVs are kept, pass or fail. master's branch protection requires it.
acceptance, nightly and release share the concurrency group qemu, so
the runner never runs two of them at once: CLAUDE.md's one-QEMU rule
holds in CI too. build.yml becomes the quick check on pushes only.
.claude/CLAUDE.md's Hard Rules: commit and push directly on the working
branch; master only through a PR that passed acceptance, no direct
pushes; no approval required while there is one developer. Named: the
Captain Bob method.
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
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>
Claude
rajames