diff --git a/.gitea/workflows/release.yml b/.gitea/workflows/release.yml index 89469431..e58d82bd 100644 --- a/.gitea/workflows/release.yml +++ b/.gitea/workflows/release.yml @@ -54,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 diff --git a/CHANGELOG.md b/CHANGELOG.md index a8ad0b7a..409d7df9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,13 @@ # 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 diff --git a/docs/fabric/FABRIC-3.md b/docs/fabric/FABRIC-3.md index 82ca875d..755bc19a 100644 --- a/docs/fabric/FABRIC-3.md +++ b/docs/fabric/FABRIC-3.md @@ -6165,3 +6165,16 @@ Isabelle2025-2 (HOL-Library and its build database) is a package in this reposit `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. diff --git a/experiments/bare_metal/runs/doe-aarch64-20261107-184241.csv b/experiments/bare_metal/runs/doe-aarch64-20261107-184241.csv new file mode 100644 index 00000000..e69de29b diff --git a/experiments/bare_metal/runs/doe-amd64-20261107-184040.csv b/experiments/bare_metal/runs/doe-amd64-20261107-184040.csv new file mode 100644 index 00000000..e69de29b diff --git a/experiments/bare_metal/runs/doe-amd64-20261107-184753.csv b/experiments/bare_metal/runs/doe-amd64-20261107-184753.csv new file mode 100644 index 00000000..e69de29b diff --git a/experiments/bare_metal/runs/doe-riscv64-20261107-184616.csv b/experiments/bare_metal/runs/doe-riscv64-20261107-184616.csv new file mode 100644 index 00000000..e69de29b diff --git a/experiments/bare_metal/runs/doe-riscv64-20261107-190906.csv b/experiments/bare_metal/runs/doe-riscv64-20261107-190906.csv new file mode 100644 index 00000000..e69de29b diff --git a/experiments/bare_metal/runs/doe-riscv64-20261107-191105.csv b/experiments/bare_metal/runs/doe-riscv64-20261107-191105.csv new file mode 100644 index 00000000..e69de29b diff --git a/experiments/bare_metal/runs/doe-riscv64-20261107-191304.csv b/experiments/bare_metal/runs/doe-riscv64-20261107-191304.csv new file mode 100644 index 00000000..e69de29b diff --git a/kernel/Makefile b/kernel/Makefile index 81bcbd7b..a7c86bb5 100644 --- a/kernel/Makefile +++ b/kernel/Makefile @@ -95,6 +95,9 @@ endif # 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 @@ -103,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 ?= 4.0.0-alpha.1 +LITHOS_VERSION ?= 4.0.0-alpha.2 # ============================================================================== # BUILD PATHS diff --git a/logs/20261107-184040/amd64/qemu-amd64-20261107-184040.log b/logs/20261107-184040/amd64/qemu-amd64-20261107-184040.log new file mode 100644 index 00000000..6bc54f35 --- /dev/null +++ b/logs/20261107-184040/amd64/qemu-amd64-20261107-184040.log @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:16ff21b314d76f58304fefba58921194b848b2a7521a91b6a9bf6ac72b01a368 +size 6637 diff --git a/logs/20261107-184241/aarch64/qemu-aarch64-20261107-184241.log b/logs/20261107-184241/aarch64/qemu-aarch64-20261107-184241.log new file mode 100644 index 00000000..c24e88d0 --- /dev/null +++ b/logs/20261107-184241/aarch64/qemu-aarch64-20261107-184241.log @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:72acbac8e5db7027b26c1b9689116d434368421961330f6199cbdd6116c449e1 +size 5602 diff --git a/logs/20261107-184616/riscv64/qemu-riscv64-20261107-184616.log b/logs/20261107-184616/riscv64/qemu-riscv64-20261107-184616.log new file mode 100644 index 00000000..20ab5c94 --- /dev/null +++ b/logs/20261107-184616/riscv64/qemu-riscv64-20261107-184616.log @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:a52383c54ba6f2e57dbbdc6115a66d21a877661ae8b053da2748d1dc6f297c07 +size 7993 diff --git a/logs/20261107-184753/amd64/qemu-amd64-20261107-184753.log b/logs/20261107-184753/amd64/qemu-amd64-20261107-184753.log new file mode 100644 index 00000000..28491434 --- /dev/null +++ b/logs/20261107-184753/amd64/qemu-amd64-20261107-184753.log @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:6632ed60fecd61ebdb02cced5f7dc99b821046108ebce0b32e6bf2e94a8fc82d +size 6708 diff --git a/logs/20261107-185450/isabelle/isabelle-20261107-185450.log b/logs/20261107-185450/isabelle/isabelle-20261107-185450.log new file mode 100644 index 00000000..86e1a00e --- /dev/null +++ b/logs/20261107-185450/isabelle/isabelle-20261107-185450.log @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:ea0e788b3fc07f4dd6688a54f4409002ae96f2e1f48d8833f7abf243264a61a2 +size 7783 diff --git a/logs/20261107-190906/riscv64/qemu-riscv64-20261107-190906.log b/logs/20261107-190906/riscv64/qemu-riscv64-20261107-190906.log new file mode 100644 index 00000000..4d1bf87c --- /dev/null +++ b/logs/20261107-190906/riscv64/qemu-riscv64-20261107-190906.log @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:ce8ff0557f7784c52621ceda6bb14d1cc95e2482aea02876a7fc17605f64e9eb +size 7993 diff --git a/logs/20261107-191105/riscv64/qemu-riscv64-20261107-191105.log b/logs/20261107-191105/riscv64/qemu-riscv64-20261107-191105.log new file mode 100644 index 00000000..8684f46a --- /dev/null +++ b/logs/20261107-191105/riscv64/qemu-riscv64-20261107-191105.log @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:d160ab458d8f4a422051dc13cc707f7c1b8fc97ba73c285316b7315cbe827237 +size 7993 diff --git a/logs/20261107-191304/riscv64/qemu-riscv64-20261107-191304.log b/logs/20261107-191304/riscv64/qemu-riscv64-20261107-191304.log new file mode 100644 index 00000000..67b56259 --- /dev/null +++ b/logs/20261107-191304/riscv64/qemu-riscv64-20261107-191304.log @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:3074fcf7f8b8a8dd33fee887877dc51965eb461e49f1bf2c134d2ecc402342bf +size 7993