Merge pull request #37 from rems-project/mdd/run-cn-tests

Add a workflow to run CN on examples

.github/workflows/run-cn-examples.yml

@@ -0,0 +1,100 @@
+# Modified from rems-project/cerberus/blob/master/.github/workflows/ci.yml
+
+name: Test all examples with CN
+
+on:   
+  pull_request:
+  push:
+    branches:
+      - main
+
+# cancel in-progress job when a new push is performed
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  build:
+    strategy:
+      matrix:
+        version: [4.14.1]
+
+    runs-on: ubuntu-22.04
+
+    steps:
+    - uses: actions/checkout@v4
+      with:  
+        repository: rems-project/cerberus 
+
+    - name: System dependencies (ubuntu)
+      run: |
+        sudo apt install build-essential libgmp-dev z3 opam
+    
+    - 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
+
+    - name: Download cvc5 release 
+      uses: robinraju/release-downloader@v1 
+      with: 
+        repository: cvc5/cvc5
+        tag: cvc5-1.1.2
+        fileName: cvc5-Linux-static.zip
+
+    - name: Unzip and install cvc5
+      run: |
+        unzip cvc5-Linux-static.zip
+        chmod +x cvc5-Linux-static/bin/cvc5
+        sudo cp cvc5-Linux-static/bin/cvc5 /usr/local/bin/
+
+    - name: Checkout cn-tutorial
+      uses: actions/checkout@v4
+      with: 
+        repository: rems-project/cn-tutorial
+        path: cn-tutorial
+
+    - name: Run CN Tutorial CI tests
+      run: |
+        opam switch ${{ matrix.version }}
+        eval $(opam env --switch=${{ matrix.version }})
+        USE_OPAM='' tests/run-cn-tutorial-ci.sh cn-tutorial

src/example-archive/check-all.sh

@@ -23,7 +23,7 @@ FAILURE=0
 for subdir in "${subdirs[@]}"; do
   cd "$subdir" || continue
 
-  ../check.sh $CN 
+  ../check.sh "$CN" 
 
   if [ $? != 0 ]
   then 

src/example-archive/check.sh

@@ -43,7 +43,7 @@ check_file() {
   local expected_exit_code=$2
 
   printf "[$file]... "
-  timeout 10 cn "$file" > /dev/null 2>&1
+  timeout 10 $CN "$file" > /dev/null 2>&1
   local result=$?
 
   if [ $result -eq $expected_exit_code ]; then