ci: the workflows run in the runner image with HOL-Library #128

2026-11-07T17:47:23Z

rajames commented

2026-11-07 17:47:23 +00:00

What and why

The workflows run in lithosananke-runner:4f675c8b75b2, the image runner-image.yml built from master 4f675c8b (run 193) after #127: what init installs, Maven, and the HOL-Library heap, fetched prebuilt (checksum OK, 4.8 s), so the proofs step builds only the StarForth session (~2.2 GiB, under a minute) instead of HOL-Library (~5.3 GiB, which the server cannot hold). Without this, the v4.0.0-alpha.1 release run's proofs step would be killed as nightly 174's was.

Part of #120, #17. The step before tagging v4.0.0-alpha.1.

Acceptance

The Acceptance check on this pull request runs in the new image: it is the test.

Logs from runs made by hand are committed in logs/, if any -- none
Hardware this was tried on, if any: none (CI only)

The record

docs/fabric/FABRIC-3.md has the ruling and what was built, if this is design work -- XLVII.4 already describes it
CHANGELOG.md, if it is a milestone -- part of the v4.0.0-alpha.1 entry
Nothing in this PR is a fix nobody asked for (.claude/CLAUDE.md, Hard Rules)

🤖 Generated with Claude Code

https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2

## What and why The workflows run in **`lithosananke-runner:4f675c8b75b2`**, the image `runner-image.yml` built from master `4f675c8b` (run 193) after #127: what `init` installs, Maven, and the **HOL-Library heap, fetched prebuilt** (checksum OK, 4.8 s), so the proofs step builds only the StarForth session (~2.2 GiB, under a minute) instead of HOL-Library (~5.3 GiB, which the server cannot hold). Without this, the `v4.0.0-alpha.1` release run's proofs step would be killed as nightly 174's was. Part of #120, #17. The step before tagging `v4.0.0-alpha.1`. ## Acceptance The **Acceptance** check on this pull request runs in the new image: it is the test. - [ ] Logs from runs made by hand are committed in `logs/`, if any -- none - [ ] Hardware this was tried on, if any: none (CI only) ## The record - [ ] `docs/fabric/FABRIC-3.md` has the ruling and what was built, if this is design work -- XLVII.4 already describes it - [ ] `CHANGELOG.md`, if it is a milestone -- part of the v4.0.0-alpha.1 entry - [x] Nothing in this PR is a fix nobody asked for (`.claude/CLAUDE.md`, Hard Rules) 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2

rajames added 1 commit 2026-11-07 17:47:23 +00:00

ci: the workflows run in lithosananke-runner:4f675c8b75b2, with HOL-Library

Build / Image RASPI (push) Successful in 2m28s

Details

Build / Image PC (push) Successful in 2m56s

Details

Build / Image MILKV (push) Successful in 2m34s

Details

Build / v4 tests (32- and 64-bit cells) (push) Successful in 8m52s

Details

Acceptance / Acceptance (pull_request) Successful in 12m30s

Details

3c21a20f1a

The image runner-image.yml built from master 4f675c8b (run 193): what init
installs, Maven, and the HOL-Library heap fetched prebuilt (checksum OK, 4.8
s), so the proofs build only the StarForth session. Its acceptance run is
this PR's.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2

rajames merged commit 233025da88 into master

2026-11-07 18:17:53 +00:00

Sign in to join this conversation.

1 Participants

Notifications

Due Date

No due date set.

Dependencies

No dependencies set.

Reference: rajames/LithosAnanke#128