From 0c275ddad0fa8da71f6a9f8c89b404c355a471d2 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@data61.csiro.au>
Date: Thu, 26 Nov 2020 08:22:21 +1100
Subject: [PATCH] github: remove Refine sessions from github CI

With Isabelle2020 the Refine sessions are too close to memory
boundaries on github runners, the tests randomly fail with out-of-store
exceptions in polyml (but also randomly succeed without change).

Removing the session here until we have a better solution.

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
---
 .github/workflows/proof.yml | 46 ++++++++++++++++++++-----------------
 1 file changed, 25 insertions(+), 21 deletions(-)

diff --git a/.github/workflows/proof.yml b/.github/workflows/proof.yml
index 03af34d8a..2c8fc5286 100644
--- a/.github/workflows/proof.yml
+++ b/.github/workflows/proof.yml
@@ -53,27 +53,31 @@ jobs:
         isa_branch: ts-2020
         session: ExecSpec ASpec AInvs EVTutorial
 
-  refine:
-    name: Refine
-    needs: ainvs
-    runs-on: ubuntu-latest
-    strategy:
-      fail-fast: false
-      matrix:
-        arch: [ARM, ARM_HYP, RISCV64, X64]
-    steps:
-    - name: Cache Isabelle Images
-      uses: actions/cache@v2
-      with:
-        path: cache/
-        key: ${{ runner.os }}-${{ matrix.arch }}-images-${{ github.sha }}
-        restore-keys: ${{ runner.os }}-${{ matrix.arch }}-images
-    - name: Run Proofs
-      uses: seL4/ci-actions/run-proofs@master
-      with:
-        L4V_ARCH: ${{ matrix.arch }}
-        isa_branch: ts-2020
-        session: Refine
+#  With Isabelle2020 the Refine session is now too close to resource
+#  boundaries on github runners -- it runs out of memory from time
+#  to time.
+#
+#  refine:
+#    name: Refine
+#    needs: ainvs
+#    runs-on: ubuntu-latest
+#    strategy:
+#      fail-fast: false
+#      matrix:
+#        arch: [ARM, ARM_HYP, RISCV64, X64]
+#    steps:
+#    - name: Cache Isabelle Images
+#      uses: actions/cache@v2
+#      with:
+#        path: cache/
+#        key: ${{ runner.os }}-${{ matrix.arch }}-images-${{ github.sha }}
+#        restore-keys: ${{ runner.os }}-${{ matrix.arch }}-images
+#    - name: Run Proofs
+#      uses: seL4/ci-actions/run-proofs@master
+#      with:
+#        L4V_ARCH: ${{ matrix.arch }}
+#        isa_branch: ts-2020
+#        session: Refine
 
   cspec:
     name: CSpec