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
Issues follow the record's Found / Ruled / Built / Verified
(docs/fabric/FABRIC-3.md): the reporter writes what was found and its
evidence; Captain Bob rules; the commits build it; the acceptance logs
verify it. A finding is not a request to fix it (.claude/CLAUDE.md).
.gitea/ISSUE_TEMPLATE/
1-bug.yaml Found, where, system (v4/v3), seen on (ISA, stick,
hardware), evidence (the log lines), how found
2-work.yaml what, why (the ruling or design section), done when
(with the acceptance protocol and its logs), area,
priority
3-ruling.yaml the question, the options and their costs, a
recommendation, where the ruling will be recorded,
what waits on it
4-board.yaml board, the image booted (Nexus version or commit),
what happened, the serial log, the BRINGUP.md item
config.yaml blank issues still allowed; the XWiki linked for
design and discussion
.gitea/pull_request_template.md what and why, Closes #, acceptance
(the check runs itself; hand-run logs; hardware), the
record (FABRIC-3.md, CHANGELOG), no unrequested fixes
Gitea reads these from the default branch: they apply once on master.
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