ci/runner-image/Dockerfile

@@ -1,7 +1,8 @@
 # The CI runner image (#120): gitea/runner-images' Ubuntu 24.04 with Node -- which
 # actions/checkout and upload-artifact run on -- plus everything the jobs install at their start:
 # what `make ARCH=amd64,aarch64,riscv64 init INIT_DOCS=0` installs (taken from the Makefile
-# itself, not copied, so the two cannot drift), and Maven and a JRE for the publish steps.
+# itself, not copied, so the two cannot drift), Maven and a JRE for the publish steps, and
+# Isabelle's HOL-Library already built, for the proofs.
 #
 # Built by .gitea/workflows/runner-image.yml, from a context of the Makefile, boards/ and this file.
 FROM gitea/runner-images:ubuntu-24.04-v26.11.03
@@ -11,4 +12,8 @@ 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
 WORKDIR /

scripts/nightly.sh

@@ -17,7 +17,8 @@
 #       make -C v4 test-32: v4 with 32-bit cells, every test (the acceptance's last part).
 #   scripts/nightly.sh proofs
 #       isabelle build -c -D proof/: the StarForth session checked afresh every run, whatever is
-#       cached (HOL-Library is reused); its log is logs/<TS>/isabelle/, as a boot's is.
+#       cached (HOL-Library is reused: the CI image has it built, ci/runner-image); its log is
+#       logs/<TS>/isabelle/, as a boot's is.
 #   scripts/nightly.sh images
 #       The board images, into build/nightly/:
 #         raspi5.img.xz   Raspberry Pi 5 (make boot_image TARGET=RASPI), for Raspberry Pi Imager