4 Commits

Include renames

Author	SHA1	Message	Date
Claude	2580a40e1d	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	2026-11-07 17:15:56 +00:00
Claude	03027f9769	pki: the StarshipOS CA, made on the CI box; capsules signed in CI ... Ruled by Captain Bob, 2026-11-07: "New root CA on the CI box. Valid StarshipOS rather than snake oil intermediate." - ci/pki/make-ca.sh makes the StarshipOS Root CA (its key stays on the CI box) and the StarshipOS Capsule Signing intermediate it issues, and stores the signing key as the secret CAPSULE_SIGN_KEY. - The kernel finds the signing certificate by one name, CAPSULE_SIGNING_CERT_NAME = pki:starshipos-intermediate.der. The certificate itself lands once make-ca.sh has run; until then the snakeoil intermediate is in the tree under its old name and the capsules check as "no root key" (a warning, as "missing" was). - mkcapsule refuses a signing key that is not that certificate's. - SIGN_KEY has no default; acceptance, build, nightly and release set it from the secret. FABRIC-3.md XLVI. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2	2026-11-07 04:15:29 +00:00
Claude	4ae1f759d5	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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2	2026-11-07 03:41:34 +00:00
rajamesandClaude Opus 5.5	672d275f5c	ci: no quick check on master after a merge (#119); the runner image's recipe (#120) ... Captain Bob, 2026-11-06: a small server, a little sluggish. Each change cost about an hour of runner time; the gate itself is about 15 minutes. #119 -- build.yml runs on pushes to the working branch only. What reaches master arrives through a PR whose content just passed acceptance; checking it again cost ~23 minutes after every merge. #120, first step -- ci/runner-image/Dockerfile: gitea/runner-images' Ubuntu 24.04 (with Node, for the actions) plus what make ARCH=amd64,aarch64,riscv64 init INIT_DOCS=0 installs -- run from the Makefile itself, not a copied list -- and Maven for publishing. .gitea/workflows/runner-image.yml builds it and publishes it to the package registry as lithosananke-runner:<commit>. The workflows switch to it in a later change, once it is published and has passed acceptance. It needs the runner to lend jobs its Docker daemon (container.docker_host: automount) and a PACKAGES_TOKEN secret, unless the Actions token may publish packages. make init does git lfs install --local only inside a checkout: the image build is not one. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2	2026-11-06 20:43:42 +00:00