Claude
2580a40e1d
Build / Image MILKV (push) Successful in 2m18s
Build / v4 tests (32- and 64-bit cells) (push) Successful in 8m45s
Build / Image RASPI (push) Successful in 2m13s
Build / Image PC (push) Successful in 2m29s
Acceptance / Acceptance (pull_request) Canceled after 0s
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
31 lines
2.1 KiB
Docker
31 lines
2.1 KiB
Docker
# 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), 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
|
|
COPY Makefile /opt/starship-init/Makefile
|
|
COPY boards /opt/starship-init/boards
|
|
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, 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 /
|