release: v4.0.0-alpha.2; release.yml keeps the image's Isabelle [skip ci]
v4.0.0-alpha.1's release run (196) was killed in the proofs: release.yml's full `make init` fetched Isabelle into the workspace and pointed isabelle at it, without the image's prebuilt HOL-Library, so the proofs built it from scratch. Nothing was published. Ruled: the tag stays; release.yml runs `init INIT_PROOFS=0`; LITHOS_VERSION 4.0.0-alpha.2, the first published alpha. FABRIC-3.md XLVII.5, CHANGELOG. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
This commit is contained in:
@@ -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.
|
||||
|
||||
Reference in New Issue
Block a user