ci: the runner image fetches HOL-Library, prebuilt, instead of building it

The server cannot build it (5.3 GiB from scratch; capped, still 2.6-3.3
GiB against ~2.3 GiB free). The heap built here by the same Isabelle2025-2
is a generic package in this repository's registry (45 MB, SHA-256
bb247846...e999cb339e); the Dockerfile fetches it into Isabelle's system
heaps with the checksum pinned, the token a build secret. Portable: a
fresh Isabelle home with only this heap checks StarForth without
rebuilding HOL-Library. FABRIC-3.md XLVII.4.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2

.gitea/workflows/runner-image.yml

@@ -44,7 +44,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"

ci/runner-image/Dockerfile

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

docs/fabric/FABRIC-3.md

@@ -6153,3 +6153,15 @@ programs, 0 failures; the proofs (`-171020`). Each capsule now logs `signature:
 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).