Compare commits
24
Commits
| Author | SHA1 | Date | |
|---|---|---|---|
 rajames
|
2d43db252a | ||
 Claude
|
37f62d688b | ||
|
Claude
|
cabe974872 | ||
|
Claude
|
4a125cdd21 | ||
|
Claude
|
d8bf2e1121 | ||
|
Claude
|
04006bff12 | ||
|
rajames
|
233025da88 | ||
|
Claude
|
3c21a20f1a | ||
|
rajames
|
4f675c8b75 | ||
|
Claude
|
da020a430d | ||
|
Claude
|
2580a40e1d | ||
|
Claude
|
857083359f | ||
|
Claude
|
458f8f3ec8 | ||
|
Claude
|
4ca935d82e | ||
|
Robert A. James
|
c589d3d5b7 | ||
|
Claude
|
d7d431f1d6 | ||
|
Claude
|
b7534107f3 | ||
|
Claude
|
236839a914 | ||
|
Claude
|
bb3246f924 | ||
|
Claude
|
038556bb3e | ||
|
Claude
|
dca3ea56b9 | ||
|
Claude
|
c2ff10015f | ||
|
Claude
|
7d9dd4e4a9 | ||
|
Claude
|
8918951482 |
@@ -18,7 +18,8 @@ on:
|
||||
workflow_dispatch:
|
||||
|
||||
concurrency:
|
||||
group: qemu # one QEMU at a time on the runner: shared with nightly.yml and release.yml
|
||||
group: qemu # every workflow shares this one group: one run at a time,
|
||||
# a runner-image rebuild included (Captain Bob, 2026-11-07)
|
||||
cancel-in-progress: false
|
||||
|
||||
jobs:
|
||||
@@ -26,7 +27,7 @@ jobs:
|
||||
name: Acceptance
|
||||
runs-on: ubuntu-latest
|
||||
container:
|
||||
image: gitea.starshipos-f18.org/rajames/lithosananke-runner:72b6cf370db1 # ci/runner-image (#120)
|
||||
image: gitea.starshipos-f18.org/rajames/lithosananke-runner:4f675c8b75b2 # ci/runner-image (#120)
|
||||
credentials: # the registry refuses anonymous pulls
|
||||
username: rajames
|
||||
password: ${{ secrets.PACKAGES_TOKEN }}
|
||||
|
||||
@@ -9,14 +9,20 @@ name: Build
|
||||
on:
|
||||
push:
|
||||
branches: [StarForth-v4.0.0] # not master: what reaches it has just passed acceptance (#119)
|
||||
paths-ignore: ['site/**'] # the websites (site/) build nothing here; each run is ~17 min on
|
||||
# the server the wikis share (Captain Bob, 2026-11-07)
|
||||
workflow_dispatch:
|
||||
|
||||
concurrency:
|
||||
group: qemu # every workflow shares this one group (Captain Bob, 2026-11-07: a
|
||||
cancel-in-progress: false # runner-image rebuild blocks other jobs, always): one run at a time
|
||||
|
||||
jobs:
|
||||
image:
|
||||
name: Image ${{ matrix.board }}
|
||||
runs-on: ubuntu-latest
|
||||
container:
|
||||
image: gitea.starshipos-f18.org/rajames/lithosananke-runner:72b6cf370db1 # ci/runner-image (#120)
|
||||
image: gitea.starshipos-f18.org/rajames/lithosananke-runner:4f675c8b75b2 # ci/runner-image (#120)
|
||||
credentials: # the registry refuses anonymous pulls
|
||||
username: rajames
|
||||
password: ${{ secrets.PACKAGES_TOKEN }}
|
||||
@@ -64,7 +70,7 @@ jobs:
|
||||
name: v4 tests (32- and 64-bit cells)
|
||||
runs-on: ubuntu-latest
|
||||
container:
|
||||
image: gitea.starshipos-f18.org/rajames/lithosananke-runner:72b6cf370db1 # ci/runner-image (#120)
|
||||
image: gitea.starshipos-f18.org/rajames/lithosananke-runner:4f675c8b75b2 # ci/runner-image (#120)
|
||||
credentials: # the registry refuses anonymous pulls
|
||||
username: rajames
|
||||
password: ${{ secrets.PACKAGES_TOKEN }}
|
||||
|
||||
@@ -14,12 +14,16 @@ on:
|
||||
- cron: '0 4 * * *' # 04:00 UTC, after the images (nightly.yml, 03:00)
|
||||
workflow_dispatch:
|
||||
|
||||
concurrency:
|
||||
group: qemu # every workflow shares this one group (Captain Bob, 2026-11-07: a
|
||||
cancel-in-progress: false # runner-image rebuild blocks other jobs, always): one run at a time
|
||||
|
||||
jobs:
|
||||
docs:
|
||||
name: Book, volumes, API reference
|
||||
runs-on: ubuntu-latest
|
||||
container:
|
||||
image: gitea.starshipos-f18.org/rajames/lithosananke-runner:72b6cf370db1 # ci/runner-image (#120)
|
||||
image: gitea.starshipos-f18.org/rajames/lithosananke-runner:4f675c8b75b2 # ci/runner-image (#120)
|
||||
credentials: # the registry refuses anonymous pulls
|
||||
username: rajames
|
||||
password: ${{ secrets.PACKAGES_TOKEN }}
|
||||
|
||||
@@ -20,7 +20,8 @@ on:
|
||||
workflow_dispatch:
|
||||
|
||||
concurrency:
|
||||
group: qemu # one QEMU at a time on the runner: shared with acceptance.yml
|
||||
group: qemu # every workflow shares this one group: one run at a time,
|
||||
# a runner-image rebuild included (Captain Bob, 2026-11-07)
|
||||
cancel-in-progress: false
|
||||
|
||||
jobs:
|
||||
@@ -28,7 +29,7 @@ jobs:
|
||||
name: Acceptance, images, proofs
|
||||
runs-on: ubuntu-latest
|
||||
container:
|
||||
image: gitea.starshipos-f18.org/rajames/lithosananke-runner:72b6cf370db1 # ci/runner-image (#120)
|
||||
image: gitea.starshipos-f18.org/rajames/lithosananke-runner:4f675c8b75b2 # ci/runner-image (#120)
|
||||
credentials: # the registry refuses anonymous pulls
|
||||
username: rajames
|
||||
password: ${{ secrets.PACKAGES_TOKEN }}
|
||||
|
||||
@@ -14,7 +14,8 @@ on:
|
||||
tags: ['v*']
|
||||
|
||||
concurrency:
|
||||
group: qemu # one QEMU at a time on the runner: shared with acceptance.yml
|
||||
group: qemu # every workflow shares this one group: one run at a time,
|
||||
# a runner-image rebuild included (Captain Bob, 2026-11-07)
|
||||
cancel-in-progress: false
|
||||
|
||||
jobs:
|
||||
@@ -22,7 +23,7 @@ jobs:
|
||||
name: Release ${{ github.ref_name }}
|
||||
runs-on: ubuntu-latest
|
||||
container:
|
||||
image: gitea.starshipos-f18.org/rajames/lithosananke-runner:72b6cf370db1 # ci/runner-image (#120)
|
||||
image: gitea.starshipos-f18.org/rajames/lithosananke-runner:4f675c8b75b2 # ci/runner-image (#120)
|
||||
credentials: # the registry refuses anonymous pulls
|
||||
username: rajames
|
||||
password: ${{ secrets.PACKAGES_TOKEN }}
|
||||
@@ -53,7 +54,10 @@ jobs:
|
||||
echo "NIGHTLY_VERSION=${tree#v}" >> "$GITHUB_ENV"
|
||||
|
||||
- name: Install the dependencies
|
||||
run: make ARCH=amd64,aarch64,riscv64 init # the image has all but the documents' packages
|
||||
# INIT_PROOFS=0: the image's Isabelle has HOL-Library prebuilt; a full init would fetch a fresh
|
||||
# Isabelle into the workspace and point isabelle at it, and the proofs would build HOL-Library
|
||||
# from scratch -- killed (release run 196, v4.0.0-alpha.1)
|
||||
run: make ARCH=amd64,aarch64,riscv64 init INIT_PROOFS=0 # the image has all but the documents' packages
|
||||
|
||||
- name: Acceptance amd64
|
||||
run: scripts/nightly.sh accept amd64
|
||||
|
||||
@@ -17,6 +17,10 @@ on:
|
||||
paths: ['ci/runner-image/**', 'Makefile']
|
||||
workflow_dispatch:
|
||||
|
||||
concurrency:
|
||||
group: qemu # every workflow shares this one group (Captain Bob, 2026-11-07: a
|
||||
cancel-in-progress: false # runner-image rebuild blocks other jobs, always): one run at a time
|
||||
|
||||
jobs:
|
||||
image:
|
||||
name: Build and publish the runner image
|
||||
@@ -44,7 +48,9 @@ jobs:
|
||||
tag=$(git rev-parse --short=12 HEAD)
|
||||
ctx=$(mktemp -d) # not the repository: 7 GB of context
|
||||
cp -r Makefile boards ci/runner-image/Dockerfile "$ctx/"
|
||||
docker build -t "$img:$tag" "$ctx"
|
||||
tok=$(mktemp); printf '%s' "$TOKEN" > "$tok" # the HOL-Library heap's download (Dockerfile)
|
||||
docker build --secret id=pkgtoken,src="$tok" -t "$img:$tag" "$ctx"
|
||||
rm -f "$tok"
|
||||
echo "$TOKEN" | docker login gitea.starshipos-f18.org -u rajames --password-stdin
|
||||
docker push "$img:$tag"
|
||||
echo "Published $img:$tag"
|
||||
|
||||
@@ -1,5 +1,26 @@
|
||||
# Changelog
|
||||
|
||||
## 2026-11-07 — LithosAnanke v4.0.0-alpha.2: the first published alpha
|
||||
|
||||
`v4.0.0-alpha.1` (`233025da`) was accepted and tagged, but its release run (196) built HOL-Library
|
||||
from scratch in the proofs step and was killed: `release.yml`'s full `make init` replaced the
|
||||
image's Isabelle, the one with HOL-Library prebuilt. Nothing was published; the tag stays where it is
|
||||
(Captain Bob, 2026-11-07). `release.yml` now runs `init INIT_PROOFS=0`, and `v4.0.0-alpha.2` is the
|
||||
first alpha published -- the same system as below. `docs/fabric/FABRIC-3.md` XLVII.5.
|
||||
|
||||
## 2026-11-07 — LithosAnanke v4.0.0-alpha.1: the first alpha release
|
||||
|
||||
The first alpha of the kernel, `v4.0.0-alpha.1`: v4, StarForth's F18 engine, is the system every
|
||||
board boots by default, with v3 a boot argument away. The kernel's version goes from 2.1.0 to the
|
||||
4.x working line (Captain Bob, 2026-11-07); the engine stays 3.2.0. Accepted in full before the tag:
|
||||
amd64, aarch64 and riscv64 to `[zuse@Hera] ok>` with POST 538/538 and one `dict_hash`
|
||||
(`0xfec8c47cfc6f437f`), the PC stick loaded high, `test-32` (39 programs, 0 failures), and the
|
||||
Isabelle/HOL proofs. An alpha: the v4.0.0 milestone's own definition -- parity with v3's vocabulary,
|
||||
K=1.0 measured on v4, the hosted mesh, Verilator -- is still open, and the capsules are unsigned until
|
||||
the StarshipOS CA is made (FABRIC-3.md XLVI). Also today: CI in a prebuilt runner image, the
|
||||
nightly's proofs no longer able to hold back its images, and the .com and .org websites. Full record:
|
||||
`docs/fabric/FABRIC-3.md` XLVII.
|
||||
|
||||
## 2026-11-07 — CI jobs start ready: the runner image
|
||||
|
||||
The CI jobs now run in `lithosananke-runner` (`ci/runner-image`, #120), an image with everything
|
||||
|
||||
Binary file not shown.
Binary file not shown.
@@ -12,8 +12,19 @@ WORKDIR /opt/starship-init
|
||||
RUN make --no-print-directory ARCH=amd64,aarch64,riscv64 init INIT_DOCS=0 \
|
||||
&& DEBIAN_FRONTEND=noninteractive apt-get install -y -qq maven default-jre-headless \
|
||||
&& rm -rf /var/lib/apt/lists/* /opt/starship-init/build/cache/downloads
|
||||
# HOL-Library, built once here, into Isabelle's own heaps (system_heaps), so the nightly's proofs
|
||||
# build only the StarForth session: ~2.2 GiB and under a minute, where HOL-Library from scratch
|
||||
# takes ~5.3 GiB and ~11 minutes -- more than the runner had (nightly 174, killed).
|
||||
RUN isabelle build -b -o system_heaps -o threads=1 HOL-Library
|
||||
# HOL-Library, prebuilt, into Isabelle's own heaps, so the proofs build only the StarForth session
|
||||
# (~2.2 GiB, under a minute). Built from scratch it takes ~5.3 GiB (nightly 174 was killed doing it),
|
||||
# and capped it still needs ~2.6-3.3 GiB: more than the server has. So it is built once, elsewhere,
|
||||
# by the same Isabelle2025-2, and fetched from this repository's package registry, its checksum
|
||||
# pinned here (FABRIC-3.md XLVII). Isabelle ships its own HOL heap the same way. The token is a
|
||||
# build secret (runner-image.yml): it is in neither the image nor its history.
|
||||
ARG HOL_LIBRARY_URL=https://gitea.starshipos-f18.org/api/packages/rajames/generic/isabelle-hol-library/Isabelle2025-2/hol-library-Isabelle2025-2.tar.xz
|
||||
ARG HOL_LIBRARY_SHA256=bb24784664def9379e5db27f88802e3679b8e1c628177f6fbe7084e999cb339e
|
||||
RUN --mount=type=secret,id=pkgtoken \
|
||||
curl -fsSL -H "Authorization: token $(cat /run/secrets/pkgtoken)" -o /tmp/hol-library.tar.xz "$HOL_LIBRARY_URL" \
|
||||
&& echo "$HOL_LIBRARY_SHA256 /tmp/hol-library.tar.xz" | sha256sum -c - \
|
||||
&& heaps=$(isabelle getenv -b ISABELLE_HEAPS_SYSTEM) && mkdir -p "$heaps" \
|
||||
&& xz -dc /tmp/hol-library.tar.xz | tar -C "$heaps" -xf - \
|
||||
&& rm /tmp/hol-library.tar.xz \
|
||||
&& test -s "$heaps/polyml-5.9.2_x86_64_32-linux/HOL-Library"
|
||||
WORKDIR /
|
||||
|
||||
@@ -6105,3 +6105,76 @@ With a CA made by `make-ca.sh` in a scratch directory (not the real one): `opens
|
||||
chain OK; `make-ca.sh` refuses a second run; `mkcapsule` with the signing key -- "signing key
|
||||
matches"; with the root's key -- refused; with a key and no certificate -- refused; with no key --
|
||||
unsigned, as before. The acceptance with the real certificate is the PR's.
|
||||
|
||||
## XLVII. LithosAnanke v4.0.0-alpha.1: the first alpha release (2026-11-07)
|
||||
|
||||
### 1. Ruled
|
||||
|
||||
Captain Bob, 2026-11-07: "next on the list is do a tag/release of v4.0.0" -- then, on what the number
|
||||
names: "StarForth version stays the same ... Kernel is 4.0.0. This is our first alpha release." The
|
||||
tag names the kernel (`release.yml`: `v<LITHOS_VERSION>`), so:
|
||||
|
||||
- `LITHOS_VERSION` 2.1.0 -> **4.0.0-alpha.1**; the tag is `v4.0.0-alpha.1`; Nexus takes
|
||||
`org.starship:kernelImage:4.0.0-alpha.1` and `org.starship:documentation:4.0.0-alpha.1`.
|
||||
- The engine's `VERSION` stays **3.2.0**.
|
||||
- The versioning policy (`kernel/Makefile`, FABRIC-3.5.md XXX): 4.x is a working line (even major).
|
||||
v3.0.0, the first LTS, is no longer the next number; an LTS line takes the next odd major when
|
||||
XXX.5's criteria are met. Alphas are numbered: a release repository takes each version once.
|
||||
- The v4.0.0 milestone is unchanged: its definition (v4 equivalent to v3, K=1.0 on all three host
|
||||
ISAs, a hosted mesh, Verilator co-simulation) is what 4.0.0 itself will be; nine of its issues
|
||||
are open. This is an alpha of it.
|
||||
- The release is built and proved here first (this session, 15 GiB), its logs committed; the
|
||||
server's release run follows once it can pass -- the proofs need HOL-Library in the runner image.
|
||||
The capsules are unsigned for this release.
|
||||
|
||||
### 2. Verified (this session, `b7534107`, before the tag)
|
||||
|
||||
- amd64 (`logs/20261107-150809`), aarch64 (`-151023`), riscv64 (`-151359`): `LithosAnanke
|
||||
v4.0.0-alpha.1 <arch>`, `[zuse@Hera] ok>`, `PARITY:V4_POST tests=538 pass=538 fail=0`,
|
||||
`POST: PASSED`, Zuse identity confirmed, `PARITY:V4_SYSTEM word_count=317
|
||||
dict_hash=0xfec8c47cfc6f437f` on all three.
|
||||
- The PC stick loaded high (`logs/20261107-151539`): the same, from the stick, no fault.
|
||||
- `make -C v4 test-32`: 39 programs, 0 failures.
|
||||
- The Isabelle/HOL proofs (`logs/20261107-152312/isabelle`).
|
||||
- Each v4 capsule logs `signature: no root key (cert not found/parseable)`: the kernel looks for the
|
||||
StarshipOS Capsule Signing certificate (XLVI), which is not in the tree until `ci/pki/make-ca.sh`
|
||||
has run. A warning, as "missing (unsigned)" was before; nothing is refused.
|
||||
|
||||
### 3. The StarshipOS CA, and acceptance again (`4ca935d8`)
|
||||
|
||||
`ci/pki/make-ca.sh` ran on the CI box (2026-11-07 16:50 UTC): the StarshipOS Root CA there, the
|
||||
signing key in the secret `CAPSULE_SIGN_KEY`, and the certificate -- O=StarshipOS, CN=StarshipOS
|
||||
Capsule Signing, issued by the root, 2026-11-07 to 2036-11-06, `CA:TRUE, pathlen:0`, SHA-256 of the
|
||||
DER `13a28dda...029b9a6c` -- in the tree as `capsules/pki/starshipos-intermediate.der`, the snakeoil
|
||||
intermediate out of it. The tree changed, so the protocol ran again here: amd64
|
||||
(`logs/20261107-165611`), aarch64 (`-165817`), riscv64 (`-170149`) -- POST 538/538,
|
||||
`dict_hash=0xfec8c47cfc6f437f` on all three; the stick loaded high (`-170326`); `test-32`, 39
|
||||
programs, 0 failures; the proofs (`-171020`). Each capsule now logs `signature: missing (unsigned)`:
|
||||
the kernel found and read the StarshipOS certificate (it said "no root key" without it), and this
|
||||
session has no key to sign with. CI signs with the secret: the PR's acceptance and the release are
|
||||
where every capsule first verifies.
|
||||
|
||||
### 4. HOL-Library, prebuilt
|
||||
|
||||
The runner image was to build HOL-Library itself (XLVI's companion change, `4ae1f759`); the server
|
||||
cannot: from scratch it peaks at ~5.3 GiB, and with Poly/ML capped at 1.6 GiB the build still needs
|
||||
Isabelle's Java side at ~1 GiB (at 384 MiB it ran out and hung) -- 2.6-3.3 GiB against the server's
|
||||
3.8 GiB in all, ~2.3 GiB free with both wikis stopped. So the heap built here by the same
|
||||
Isabelle2025-2 (HOL-Library and its build database) is a package in this repository's registry,
|
||||
`generic/isabelle-hol-library/Isabelle2025-2/hol-library-Isabelle2025-2.tar.xz` (45 MB, SHA-256
|
||||
`bb247846...e999cb339e`), and the image fetches it into Isabelle's system heaps, checksum pinned,
|
||||
its token a Docker build secret. Shown portable first: a fresh Isabelle home holding only that heap
|
||||
checks the StarForth session without rebuilding HOL-Library (24 s).
|
||||
|
||||
### 5. v4.0.0-alpha.1 not published; v4.0.0-alpha.2
|
||||
|
||||
PR #127 merged (`4f675c8b`, acceptance run 192 with the capsules signed); `runner-image.yml` built
|
||||
`lithosananke-runner:4f675c8b75b2` with HOL-Library fetched (checksum OK, 4.8 s); PR #128 moved the
|
||||
workflows onto it (`233025da`, acceptance run 195 in the new image). `v4.0.0-alpha.1` was tagged on
|
||||
`233025da`. Its release run (196) passed acceptance in full, then the proofs step built HOL-Library
|
||||
from scratch and was killed (exit 137): `release.yml` ran a full `make init` for the documents'
|
||||
packages, which also fetched Isabelle into the workspace and pointed `/usr/local/bin/isabelle` at it
|
||||
-- an Isabelle without the image's HOL-Library. Nothing was published. Ruled (Captain Bob,
|
||||
2026-11-07): the tag stays where it is; `release.yml` runs `init INIT_PROOFS=0` (as
|
||||
`nightly-docs.yml` does), `LITHOS_VERSION` becomes `4.0.0-alpha.2`, and `v4.0.0-alpha.2` is the
|
||||
first published alpha.
|
||||
|
||||
+10
-1
@@ -89,6 +89,15 @@ endif
|
||||
# v2.2.0 — amd64 bare-metal bring-up (Beelink SER5)
|
||||
# v2.x — further working releases; riscv64 / aarch64 board bring-up
|
||||
# v3.0.0 — FIRST LTS, when and only when FABRIC-3.5.md §XXX.5's 5 criteria are met
|
||||
# v4.0.0-alpha.1 — the first alpha release (Captain Bob, 2026-11-07: "Kernel is 4.0.0. This is
|
||||
# our first alpha release"): v4, the F18 engine, the default system. The kernel goes
|
||||
# from v2.1.0 straight to the 4.x working line (even: breaking changes land here);
|
||||
# v3.0.0, the first LTS, is no longer the next number -- an LTS line takes the next
|
||||
# odd major when §XXX.5's criteria are met. The engine stays 3.2.0. Alphas are
|
||||
# numbered (-alpha.N); a release repository takes each version once.
|
||||
# v4.0.0-alpha.2 — the first published alpha: v4.0.0-alpha.1 (233025da) was accepted and tagged,
|
||||
# but its release run's proofs step built HOL-Library from scratch and was killed, so
|
||||
# nothing was published; the tag stays where it is (Captain Bob, 2026-11-07).
|
||||
# LITHOS_VERSION (kernel) and VERSION (embedded StarForth engine) are independent
|
||||
# and do not auto-sync (§XXX.4) — do not infer a relationship if they ever coincide.
|
||||
# Engine VERSION bumps at tag time by what actually changed (§XXX.6): major = any
|
||||
@@ -97,7 +106,7 @@ endif
|
||||
# the messaging layer was replaced by kernel-Hermes, PLOT/FB-* relocated to Hestia —
|
||||
# all dictionary-visible, no FORTH-79 word semantics changed.
|
||||
VERSION ?= 3.2.0
|
||||
LITHOS_VERSION ?= 2.1.0
|
||||
LITHOS_VERSION ?= 4.0.0-alpha.2
|
||||
|
||||
# ==============================================================================
|
||||
# BUILD PATHS
|
||||
|
||||
Binary file not shown.
Binary file not shown.
Binary file not shown.
Some files were not shown because too many files have changed in this diff Show More
Reference in New Issue
Block a user