The first run on starshipos-f18.org created the dashboards, then XWiki
refused the group and rights objects: a form-encoded POST needs XWiki's
form token (CSRF), an XML one does not. For about two minutes Admin.WebHome
and Contributors.WebHome were readable by guests (links and the names of
secrets, no values). Objects now go as XML, and the spaces' rights are made
before the pages, so a failed run cannot leave a dashboard open. Installed:
Main 200, Admin and Contributors 401 as a guest, 200 as rajames; a second
run changes nothing.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
Captain Bob, 2026-11-07: build the .com from the StarshipOS.com canvas.
canvas/ holds the artboards as drawn; build.py makes Main, Inquiries and
TryIt as {{html}} pages (the wiki's links and domains, the images as
attachments, the real console in Try it, the forms by e-mail); install.sh
puts them on the wiki and checks a guest's view. Installed on
starshipos-f18.com: every page and image reads 200 as a guest, and renders
without a macro error.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
Captain Bob, 2026-11-07: style .org like the StarshipOS.com design canvas.
build.py makes the three pages from one source, as {{html}} blocks in the
canvas's look (navy, orange accent, JetBrains Mono and Exo 2), and the same
pages as the canvas's .org artboards.
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: a generic landing page for anonymous
visitors, a login-protected admin dashboard for him, and a protected
contributors' dashboard. Main.WebHome (everyone), Admin.WebHome
(XWiki.rajames alone), Contributors.WebHome (XWiki.StarshipContributors
and the administrator); CI shown as Gitea's live workflow badges.
install.sh puts them on the wiki through XWiki's REST API, with the group
and the space rights, and checks a guest's view. Not yet run: the .org
XWiki answers 503.
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
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
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
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 off master (#119); the runner image recipe (part of #120); the Try-it page in the .com landing page style.
Accepted by acceptance.yml, run 166, on 7be2047a.
demo/: the demo Zuse, the saved machine, the session, the ttyd service, an Apache example and the XWiki page. Closes#112, #113, #114.
Accepted by acceptance.yml, run 163, on 4f6a267b.
Captain Bob, 2026-11-06: "I want the try it as it's very own page and
use the landing page we designed earlier ... as a baseline."
The landing page is the .com's Main.WebHome. The Try-it page follows
it: a floating box -- Your Machine, in place of Quick Facts -- a linked
title, == sections, {{info}} and {{warning}}. It goes at TryIt on the
.com (/bin/view/TryIt/), with the console embedded and links back to
the landing page and the source.
The page is on the .com now, so apache-demo.conf lets the .com frame
the console (frame-ancestors), and the demo's host is
try.starshipos-f18.com.
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: a terminal with QEMU amd64 for people to play
with; "Mint Zuse for demo console" (#111); "Make the most recent of
builds that's green the demo"; a Try-it XWiki page with the console
embedded.
demo/ -- see its README:
mint-zuse.sh a Zuse of the demo's own, as a stick: blank pair,
system=v3 genesis, a second boot to confirm, make
zusestick. Never anyone's real Zuse
build-iso.sh the amd64 ISO, packed as make qemu packs it
make-snapshot.sh boot once to [zuse@Hera] ok>, save the machine
start-session.sh one visitor: the saved machine resumed, ended on
hang-up, close or time-out
console.py joins the visitor's terminal only once the machine
runs; keys typed while it loads are discarded
qemu-args.sh the machine, shared by save and resume
starshipos-demo.service, apache-demo.conf, xwiki-try-it.xwiki
Every session is a copy: no network, read-only image, the Zuse stick's
writes discarded, QEMU's seccomp sandbox, an unprivileged user, a
fenced systemd unit, 30 minutes at most.
Tested here, from the sources master accepted (run 153): the Zuse
minted (logs/20261106-192626, -192739); the saved machine at POST
538/538 and [zuse@Hera] ok>; a session through ttyd's websocket ready
in 0.2 s, 3 4 + . -> 7 ok, 7 SQUARE . -> 49 ok; QEMU gone at once on
hang-up, close and time-out. Found and fixed on the way: a machine
saved stopped resumes stopped; a prompt matched as a regex; QEMU left
behind by a hang-up; keys lost while the machine loads. Not tested
here: Apache, several sessions at once (#116).
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
master's only commit not on the branch is c809de73, the merge of #30, whose tree is the
branch's own 0fd7648a. Nothing changes in the tree; the branch protection's up-to-date
rule is satisfied.
Merges StarForth-v4.0.0 into master: StarForth v4 as the default system, the tree reorganised
(v3/, kernel/, boards/), the stick and the identity gate, and the day's CI -- the acceptance gate,
the nightlies and release to Nexus. Closes#19, #18.
Accepted by acceptance.yml, run 153, on 0fd7648a: amd64, aarch64, riscv64 to [zuse@Hera] ok>, the
PC stick loaded high (the three agree on dict_hash), make -C v4 test-32 -- the first acceptance
run in CI. The quick checks (run 152) passed too.
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
The day's record, in FABRIC-3.md's own form (ruled, found, built,
verified, open): the review's three v4 bugs; the logs and DoE CSVs put
into LFS; make init with syft and Isabelle2025-2; the Doxygen fix; the
nightlies, the release and the Nexus coordinates
(org.starship:kernelImage and :documentation, classifier by board); the
runner's Debian 11 default found and every job moved to Ubuntu 24.04;
the acceptance gate and master's protection; the StarForth repository
archived as a tag and deleted, this one renamed LithosAnanke; Gitea's
labels, milestones, issues #4-#29 and PR #30; what is still open.
CHANGELOG.md: the same, in one paragraph.
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
From /doctor's review: .claude/CLAUDE.md (40206 chars) was at the size
Claude Code warns about, and is read at the start of every session.
Now 30973.
Cut, as a session can read them from the tree itself: the Source Tree
listing, the boot-sequence diagram, "Key distinguishing features" and
License. The listing's two facts the code does not tell -- the stale
"M7: Not started" header in kernel_main.c, and virtio_blk.c not
meaning M9 is done -- are kept, as "Gotchas in the tree".
Moved, word for word, to files that load only when working there:
"Physics-Driven Adaptive Runtime" and "Critical Implementation
Details" to v3/CLAUDE.md; the superseded ACL-RWT DoE campaign
history to experiments/bare_metal/CLAUDE.md.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
logs/20261106-151805: scripts/nightly.sh proofs before -c was added. The
StarForth session's sources were unchanged since the day's earlier build,
so Isabelle reused its result and proved nothing anew (0:00:10). Kept as
the record of that run; the stage now passes -c, and the run after it
(20261106-151902) checked StarForth afresh.
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
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
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>
T= now names a specific board (qemu, pc, pi4, pi5, milkv) rather than
an arch alias. mk/boards.mk is the single table: sets ARCH, BOARD, and
BOARD_NAME. Each Makefile applies board-specific compiler flags after its
arch block — pi5 gets Cortex-A76 tuning, pi4 gets Cortex-A72, qemu uses
portable x86-64 baseline instead of -march=native. Zynq-7020 is stubbed
in comments for future 32-bit ARM support. ARCH= override still works
for raw arch selection without a named board.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
T= is now shorthand for ARCH=, selecting the target board (raspi, amd64,
aarch64, riscv64). StarForth TARGET is locked to fastest — it's the only
build profile. Makefile.starkernel T= wired the same way before ARCH
normalization runs.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Lets you type make T=fastest or make -f Makefile.starkernel ARCH=amd64 T=kernel
instead of the full TARGET= form. T= is resolved before the strip pass so it
behaves identically to TARGET= in all cases.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
fix-doxygen-unicode.py protected the first argument of each
\doxynewunicodechar{...} from its replacements, then turned every
non-ASCII character left in the file -- the protected ones too -- into
"?" and wrote the file as ASCII. refman.tex's \doxynewunicodechar{⁻},
{²} and {³} became \doxynewunicodechar{?}, and newunicodechar stopped
the build: "ASCII character requested".
The "?" fallback now applies to the unprotected parts of each line
only, and the file is written as UTF-8.
make -C docs/formal doxygen, from clean, with doxygen 1.9.8: exit 0,
build/doxygen/StarForth-API-Reference.pdf, 3561 pages.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
isabelle build -v -D proof/ with Isabelle2025-2 (installed by make init):
HOL-Library built (0:04:42), then the StarForth session's 52 theories,
every one in proof/ROOT (0:00:24); 0:05:24 in all, exit 0, nothing
FAILED. No sorry or oops in any proof (the words appear only in
comments) and quick_and_dirty is not set. The two explicit axioms are
both in StarForth_Transition.thy, the inventory StarForth_Correctness.thy
gives.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
Neither is packaged. make ARCH=<arch> init now downloads both to
build/cache/downloads, checks each archive's SHA-256, unpacks it into
build/cache/tools (both kept by make clean) and links it into
/usr/local/bin:
- syft 1.52.0, the version sbom.spdx was made with (make sbom,
boot_image); sums from the release's checksums.txt;
- Isabelle2025-2, the version proof/COVERAGE.md names (isabelle build
-D proof/), from the release's own site (the /dist mirror answered
503); Isabelle publishes no sums, so these are of the archives as
downloaded on 2026-11-06.
An archive already there with the right sum is not downloaded again;
a download with the wrong sum is deleted and init stops. The host's
build is chosen by uname -m (amd64 or arm64).
Checked on Ubuntu 24.04 (x86_64): both fetched, checked and run (syft
1.52.0, Isabelle2025-2); a wrong sum is refused and deleted; isabelle
build -n -D proof/ finds the StarForth session.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
One ISA or several (ARCH=amd64,aarch64,riscv64, for the full
acceptance), on Debian/Ubuntu with apt-get, sudo when not root:
- common: the build, the disk-image tools (scripts/mkdiskimage.sh;
sfdisk is in fdisk), git-lfs for the logs and DoE CSVs, and the
documents -- docs/book/Makefile's own list, and pdflatex, doxygen and
graphviz for docs/formal;
- per ISA: its QEMU, its UEFI firmware at kernel/Makefile's paths, and
its compiler (aarch64's loader also needs clang and lld-link).
Then git lfs install --local, so a log or CSV committed from this
checkout goes into LFS (the 1003 plain files fixed in 027b144e came
from a checkout without it). Not installed: syft (make sbom), which is
not packaged.
Checked on Ubuntu 24.04: init for all three ISAs, then make docs and
make -C docs/formal vols build. make -C docs/formal doxygen fails in
LaTeX on "newunicodechar Error: ASCII character requested" with every
package present -- a separate fault, not a missing dependency.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
The acceptance runs of .claude/CLAUDE.md, one QEMU at a time, in order,
each with clean (scripts/qemu_session.py, QEMU_DISPLAY=none):
amd64 zuse 20261106-004933 PASS
aarch64 zuse 20261106-005153 PASS
riscv64 zuse 20261106-005530 PASS
amd64 stick_zuse 20261106-005712 PASS (--target qemu-stick-high)
Each: [zuse@Hera] ok>, `3 4 + .` -> 7 ok, PARITY:V4_POST tests=538
pass=538 fail=0, POST: PASSED. PARITY:V4_SYSTEM word_count=317
dict_hash=0xfec8c47cfc6f437f on all three architectures.
make -C v4 test-32: 39 test programs, 1868561 checks, 0 failures.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
.gitattributes has routed logs/**/*.log, *.log and the DoE run CSVs
through LFS since the initial commit, and 3944 of them are pointers.
1003 were committed as plain files instead (from a checkout without
git-lfs), so every fresh clone showed them as modified. git add
--renormalize moves them to LFS like the rest. Content unchanged: each
pointer's oid is the sha256 of the file it replaces.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
- hosted (v4/tools/hosted.c): a line longer than the buffer is read to its
end and refused as too long. Before, fgets handed it over in 1025-byte
pieces and the last piece ran as a line of its own.
- bare metal (kernel/src/v4/sk_v4.c): the line editor takes 1024
characters, as the boot does, and a line typed past that is refused as
too long instead of being cut at 255 and run. V4_BOOT_LINE_TOO_LONG is
now reported at the prompt and while a line waits.
- engine (v4/src/exec.c): a store the node itself refuses (to "any port",
"which port", How or Have) left the opcode running on: !+ advanced A,
against node.h's FAULTS, and !p advanced P past the handler, into the
next fault kind's entry. A refused store now does nothing more; a store
that raises an error (D-18) still counts as made, but P stays the
handler's.
- test_port.c: both cases; they fail on the old exec.c (A 1017, P 901).
Engine-level tests (all v4/tests/test_*.c but test_host_*) pass at 32 and
64 bits; test_port also under ASan/UBSan. Not yet run: make -C v4 test,
test-32, hosted-check, and the three QEMU acceptance boots.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
Five tasks, each closed by full acceptance: the proxy Zuse (a stick's first boot mints its own;
genesis marker version 2), Artemis grown to fill the stick (metadata only), acceptance on a fresh
data stick, MINT-ZUSE onto a second stick (read back before the marker names her), and the fixed
screen whose only action is a replacement that kills the old stick.
R1 ruled (Captain Bob, 2026-10-29: "256 GiB is ruled"): Artemis grows to at most 256 GiB, not
STICK.md §5a's 2 TiB -- the block map costs two bytes of the 2 GiB kernel heap per 1 KiB block.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude
rajames