From 5690d2980bde462cdf0edee36520042b1236ceb4 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 7 Nov 2026 03:38:39 +0000 Subject: [PATCH] ci: the nightly's proofs run last, and cannot hold back the images 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 Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2 --- .gitea/workflows/nightly.yml | 19 ++++++++++++------- scripts/nightly.sh | 6 ++++-- 2 files changed, 16 insertions(+), 9 deletions(-) diff --git a/.gitea/workflows/nightly.yml b/.gitea/workflows/nightly.yml index 709694d4..7a3d89d3 100644 --- a/.gitea/workflows/nightly.yml +++ b/.gitea/workflows/nightly.yml @@ -1,12 +1,15 @@ -# Nightly snapshot of the kernel images: the acceptance protocol, the proofs, the board images, -# then Nexus. Each stage is a step of scripts/nightly.sh (its header says what each does); any -# failure stops the run, and nothing is published unless every stage before it passed. +# Nightly snapshot of the kernel images: the acceptance protocol, the board images, Nexus, then +# the proofs. Each stage is a step of scripts/nightly.sh (its header says what each does); any +# failure stops the run, and nothing is published unless every stage before it passed. The proofs +# come last and run whatever happened before them: they check the theories, not the images, so a +# failed proof does not hold back images that passed acceptance -- it turns the run red. # # org.starship:kernelImage:-SNAPSHOT, starshipos-snapshots # classifier pc StarshipOS.iso amd64, UEFI -- the ISO the amd64 acceptance boot booted # classifier raspi5 raspi5.img.xz Raspberry Pi 5, for Raspberry Pi Imager # classifier milkv MilkV.img.xz Milk-V Mars -# classifier logs logs.tar.gz this run's serial logs, proof log and DoE CSVs +# classifier logs logs.tar.gz this run's serial logs and DoE CSVs (the proof log is in +# the run's logs artifact) # # Gitea runs a schedule from the default branch, master, so this builds master. name: Nightly snapshot @@ -22,7 +25,7 @@ concurrency: jobs: nightly: - name: Acceptance, proofs, images + name: Acceptance, images, proofs runs-on: ubuntu-latest container: image: gitea.starshipos-f18.org/rajames/lithosananke-runner:72b6cf370db1 # ci/runner-image (#120) @@ -46,8 +49,6 @@ jobs: run: scripts/nightly.sh accept stick-high - name: Acceptance 32-bit build run: scripts/nightly.sh test-32 - - name: Isabelle/HOL proofs - run: scripts/nightly.sh proofs - name: Images run: scripts/nightly.sh images @@ -64,6 +65,10 @@ jobs: name: kernel-images-${{ github.run_number }} path: build/nightly/ + - name: Isabelle/HOL proofs + if: always() + run: scripts/nightly.sh proofs + - name: Keep the logs and DoE CSVs if: always() uses: actions/upload-artifact@v3 diff --git a/scripts/nightly.sh b/scripts/nightly.sh index a749fc85..02d4ceeb 100755 --- a/scripts/nightly.sh +++ b/scripts/nightly.sh @@ -3,7 +3,8 @@ # images, the documents, and Nexus. One stage per call; the workflows run each as a step # (.gitea/workflows/nightly.yml, release.yml, nightly-docs.yml). # -# The images, in this order (any failure ends the run; nothing is published after it): +# The images, in this order (any failure ends the run; nothing is published after it) -- except +# that the nightly runs the proofs last, whatever happened before them (nightly.yml says why): # # scripts/nightly.sh accept # One boot of the acceptance protocol (.claude/CLAUDE.md), in the foreground, one QEMU at a @@ -27,7 +28,8 @@ # scripts/nightly.sh publish # org.starship:kernelImage: to that Maven repository, in one deploy (one # timestamp): classifier pc (iso), raspi5 and milkv (img.xz), and logs (tar.gz: this -# run's serial logs, proof log and DoE CSVs -- the evidence for the rest). +# run's serial logs and DoE CSVs -- the evidence for the rest; and the proof log, when the +# proofs ran before it, as a release runs them). # # The documents (a separate pipeline): #