From 4ae1f759d55b4ed3b76b3443ebfdab070cc48c33 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 7 Nov 2026 03:41:34 +0000 Subject: [PATCH] ci: HOL-Library built into the runner image Measured here (Isabelle2025-2, one thread): HOL-Library from scratch takes ~11 minutes and peaks at ~5.3 GiB -- what nightly 174 was killed doing; the StarForth session on a built HOL-Library takes under a minute and ~2.2 GiB. The image builds HOL-Library once into Isabelle's own heaps, so every job finds it. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2 --- ci/runner-image/Dockerfile | 7 ++++++- scripts/nightly.sh | 3 ++- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/ci/runner-image/Dockerfile b/ci/runner-image/Dockerfile index 542b73de..2270dda6 100644 --- a/ci/runner-image/Dockerfile +++ b/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 / diff --git a/scripts/nightly.sh b/scripts/nightly.sh index 02d4ceeb..0b51dd10 100755 --- a/scripts/nightly.sh +++ b/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//isabelle/, as a boot's is. +# cached (HOL-Library is reused: the CI image has it built, ci/runner-image); its log is +# logs//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