4 Commits

Include renames

Author	SHA1	Message	Date
Claude	da020a430d	ci: one concurrency group for every workflow; a runner-image rebuild blocks the rest ... Captain Bob, 2026-11-07: "I also want that rebuilds block other jobs always." acceptance, nightly and release shared the group qemu; now runner-image, build and nightly-docs do too, so a rebuild of the runner image (on the host's Docker daemon) never overlaps another job, whatever the runner's capacity (#121). On this server every CI run is then one at a time. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2	2026-11-07 17:17:11 +00:00
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	fb24d3f482	ci: run the jobs in the runner image (#120) ... The workflows' containers are now lithosananke-runner:72b6cf370db1, built and published by runner-image.yml, with everything init installs and Maven already in it; the install steps are gone, except the documents' packages in nightly-docs.yml and release.yml. The registry refuses anonymous pulls, so each job pulls with PACKAGES_TOKEN. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2	2026-11-07 00:57:35 +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