From 2702dbaed71f6695dc95a88b7543501ce1d8701c Mon Sep 17 00:00:00 2001
From: Mike Dodds <miked@galois.com>
Date: Thu, 8 Aug 2024 03:55:30 -0700
Subject: [PATCH] [CN-exec] Add CI for CN runtime testing capability  (#458)

* Add dummy ci for CN-runtime

* Point checkout to branch

* Point to Dhruv's fork

* Tweak

* Tweak

* Point CI script to master
---
 .github/workflows/ci-runtime.yml | 93 ++++++++++++++++++++++++++++++++
 1 file changed, 93 insertions(+)
 create mode 100644 .github/workflows/ci-runtime.yml

diff --git a/.github/workflows/ci-runtime.yml b/.github/workflows/ci-runtime.yml
new file mode 100644
index 000000000..f842d7c69
--- /dev/null
+++ b/.github/workflows/ci-runtime.yml
@@ -0,0 +1,93 @@
+name: CI (CN runtime checks)
+
+on:
+  pull_request:
+  push:
+    branches:
+      - master
+      - cheri-tests
+
+env:
+  CERBERUS_IMAGE_ID: ghcr.io/rems-project/cerberus/cn:release
+
+# cancel in-progress job when a new push is performed
+concurrency:
+  group: ci-${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  build:
+    strategy:
+      matrix:
+        # version: [4.12.0, 4.14.1]
+        version: [4.14.1]
+
+
+    runs-on: ubuntu-22.04
+
+    steps:
+
+    - name: Checkout cerberus 
+      uses: actions/checkout@v4
+
+    - name: System dependencies (ubuntu)
+      run: |
+        sudo apt install build-essential libgmp-dev z3 opam cmake
+
+    - name: Restore cached opam
+      id: cache-opam-restore
+      uses: actions/cache/restore@v4
+      with:
+        path: ~/.opam
+        key: ${{ matrix.version }}
+
+    - name: Setup opam
+      if: steps.cache-opam-restore.outputs.cache-hit != 'true'
+      run: |
+        opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }}
+        opam install --deps-only --yes ./cerberus-lib.opam
+        opam switch create with_coq ${{ matrix.version }}
+        eval $(opam env --switch=with_coq)
+        opam repo add --yes --this-switch coq-released https://coq.inria.fr/opam/released
+        opam pin --yes -n coq-struct-tact https://github.com/uwplse/StructTact.git
+        opam repo add --yes --this-switch iris-dev https://gitlab.mpi-sws.org/iris/opam.git
+        opam pin --yes -n coq-sail-stdpp https://github.com/rems-project/coq-sail.git#f319aad
+        opam pin --yes -n coq-cheri-capabilities https://github.com/rems-project/coq-cheri-capabilities.git
+        opam install --deps-only --yes ./cerberus-lib.opam ./cerberus-cheri.opam
+
+    - name: Save cached opam
+      if: steps.cache-opam-restore.outputs.cache-hit != 'true'
+      id: cache-opam-save
+      uses: actions/cache/save@v4
+      with:
+        path: ~/.opam
+        key: ${{ steps.cache-opam-restore.outputs.cache-primary-key }}
+
+    - name: Install Cerberus
+      run: |
+        opam switch ${{ matrix.version }}
+        eval $(opam env --switch=${{ matrix.version }})
+        opam pin --yes --no-action add cerberus-lib .
+        opam pin --yes --no-action add cerberus .
+        opam install --yes cerberus
+
+    - name: Install CN
+      run: |
+        opam switch ${{ matrix.version }}
+        eval $(opam env --switch=${{ matrix.version }})
+        opam pin --yes --no-action add cn .
+        opam install --yes cn ocamlformat.0.26.2
+
+    - name: Checkout cn-tutorial
+      uses: actions/checkout@v4
+      with:
+        repository: rems-project/cn-tutorial
+        path: cn-tutorial
+        ref: cn-runtime-testing # FIXME: remove once the branch is merged 
+
+    - name: Run CN-runtime CI tests 
+      run: |
+        opam switch ${{ matrix.version }}
+        eval $(opam env --switch=${{ matrix.version }})
+        cd cn-tutorial; ./runtime-test.sh 
+        cd ..