From 08daef99710c700c19773c97880a5816b5f8dcb9 Mon Sep 17 00:00:00 2001
From: Robert James <rajames440@gmail.com>
Date: Fri, 6 Nov 2026 04:20:00 +0000
Subject: [PATCH] ci: add Isabelle/HOL proof verification job

Runs StarForth session (52 theories) in parallel with the board build
matrix. Caches the Isabelle2024 installation (~800MB) and the compiled
heaps keyed on proof/**/*.thy + ROOT, so only theory changes trigger a
full rebuild. Uploads the build log as an artifact on every run
(pass or fail) for audit.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
---
 .gitea/workflows/build.yml | 46 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)

diff --git a/.gitea/workflows/build.yml b/.gitea/workflows/build.yml
index 547135e4..53ceffae 100644
--- a/.gitea/workflows/build.yml
+++ b/.gitea/workflows/build.yml
@@ -166,3 +166,49 @@ jobs:
           # starforth/<version>/starforth-<version>-<board>
           push "starforth/${SFVER}/starforth-${SFVER}-${BOARD}" \
             "build/${VM_ARCH}/fastest/starforth"
+
+  verify-isabelle:
+    name: Isabelle/HOL Proofs
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Cache Isabelle installation
+        uses: actions/cache@v3
+        id: isabelle-install-cache
+        with:
+          path: /opt/Isabelle2024
+          key: isabelle-2024-linux
+
+      - name: Install Isabelle
+        if: steps.isabelle-install-cache.outputs.cache-hit != 'true'
+        run: |
+          apt-get update -qq
+          apt-get install -y --no-install-recommends curl ca-certificates
+          curl -fsSL \
+            "https://isabelle.in.tum.de/dist/Isabelle2024_linux.tar.gz" \
+            -o /tmp/isabelle.tar.gz
+          tar -xzf /tmp/isabelle.tar.gz -C /opt
+          rm /tmp/isabelle.tar.gz
+
+      - name: Cache Isabelle heaps
+        uses: actions/cache@v3
+        with:
+          path: ~/.isabelle/Isabelle2024
+          key: isabelle-heaps-${{ hashFiles('proof/**/*.thy', 'proof/ROOT') }}
+          restore-keys: isabelle-heaps-
+
+      - name: Verify StarForth proofs
+        run: |
+          export PATH=/opt/Isabelle2024/bin:$PATH
+          isabelle build -v -d proof StarForth 2>&1 | tee /tmp/isabelle-build.log
+          # Exit code reflects proof success/failure
+          grep -q "Finished StarForth" /tmp/isabelle-build.log
+
+      - name: Upload proof log
+        if: always()
+        uses: actions/upload-artifact@v3
+        with:
+          name: isabelle-proof-log-${{ github.sha }}
+          path: /tmp/isabelle-build.log