.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:<LITHOS_VERSION>-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

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 <amd64|aarch64|riscv64|stick-high>
 #       One boot of the acceptance protocol (.claude/CLAUDE.md), in the foreground, one QEMU at a
@@ -27,7 +28,8 @@
 #   scripts/nightly.sh publish <URL>
 #       org.starship:kernelImage:<VERSION> 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):
 #