ci: the nightly's proofs run last, and cannot hold back the images #124

2026-11-07T11:22:13Z

rajames commented

2026-11-07 11:22:13 +00:00

What and why

Nightly 174 (2026-11-07 03:00) passed acceptance, then the Isabelle/HOL proofs step was killed building HOL-Library (exit 137, out of memory on the runner), so the board images were never built or published to Nexus (#17). The proofs check the theories, not the images: they now run last in nightly.yml, after the publish, whatever happened before them. A failed proof still turns the run red; its log stays in the run's logs artifact. release.yml is unchanged: a release still runs the proofs before it publishes.

This is 5690d298 alone, cherry-picked onto master on its own branch nightly-proofs-last (Captain Bob's permission, 2026-11-07), so tonight's nightly publishes the images. The rest of StarForth-v4.0.0 (HOL-Library in the runner image, the StarshipOS CA) follows in its own PR.

Part of #17

Acceptance

The Acceptance check runs on this pull request.

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 -- not design work
CHANGELOG.md, if it is a milestone -- not a milestone
Nothing in this PR is a fix nobody asked for (.claude/CLAUDE.md, Hard Rules) -- asked for 2026-11-07 ("Yes, fix")

🤖 Generated with Claude Code

https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2

## What and why Nightly 174 (2026-11-07 03:00) passed acceptance, then the Isabelle/HOL proofs step was killed building HOL-Library (exit 137, out of memory on the runner), so the board images were never built or published to Nexus (#17). The proofs check the theories, not the images: they now run last in `nightly.yml`, after the publish, whatever happened before them. A failed proof still turns the run red; its log stays in the run's logs artifact. `release.yml` is unchanged: a release still runs the proofs before it publishes. This is `5690d298` alone, cherry-picked onto `master` on its own branch `nightly-proofs-last` (Captain Bob's permission, 2026-11-07), so tonight's nightly publishes the images. The rest of `StarForth-v4.0.0` (HOL-Library in the runner image, the StarshipOS CA) follows in its own PR. Part of #17 ## Acceptance The **Acceptance** check runs on this pull request. - [ ] 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 -- not design work - [ ] `CHANGELOG.md`, if it is a milestone -- not a milestone - [x] Nothing in this PR is a fix nobody asked for (`.claude/CLAUDE.md`, Hard Rules) -- asked for 2026-11-07 ("Yes, fix") 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2

rajames added 1 commit 2026-11-07 11:22:14 +00:00

ci: the nightly's proofs run last, and cannot hold back the images

Acceptance / Acceptance (pull_request) Successful in 13m29s

Details

c27fdc6289

Nightly 174 passed acceptance, then Isabelle was killed building HOL-Library
(exit 137, out of memory on the runner), and the images were never built or
published. The proofs check the theories, not the images: they now run after
the publish, whatever happened before them, and a failure still turns the run
red. Their log stays in the run's logs artifact. A release still runs them
before it publishes.

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

rajames merged commit e15d9022cf into master

2026-11-07 11:36:22 +00:00

Sign in to join this conversation.

1 Participants

Notifications

Due Date

No due date set.

Dependencies

No dependencies set.

Reference: rajames/LithosAnanke#124