ci: add Isabelle/HOL proof verification job
StarshipOS Build / milkv (push) Failing after 30s
StarshipOS Build / pc (push) Failing after 28s
StarshipOS Build / pi4 (push) Failing after 29s
StarshipOS Build / pi5 (push) Failing after 24s
StarshipOS Build / qemu (push) Failing after 32s
StarshipOS Build / Isabelle/HOL Proofs (push) Failing after 25s
StarshipOS Build / milkv (push) Failing after 30s
StarshipOS Build / pc (push) Failing after 28s
StarshipOS Build / pi4 (push) Failing after 29s
StarshipOS Build / pi5 (push) Failing after 24s
StarshipOS Build / qemu (push) Failing after 32s
StarshipOS Build / Isabelle/HOL Proofs (push) Failing after 25s
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>
This commit is contained in:
@@ -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
|
||||
|
||||
Reference in New Issue
Block a user