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//starforth-- 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