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/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