[CN] Make CN run both Z3 and CVC5 in CI, tidy up runner CI script (#365)

* Modify GH action to download and install cvc5

* Make the CI script run both Z3 / CVC5

* Bump v to avoid deprecated nodejs

* Tidy up the tutorial repo CI by using the new `make check` target

.github/workflows/ci.yml

@@ -31,7 +31,7 @@ jobs:
     
     - name: Restore cached opam
       id: cache-opam-restore
-      uses: actions/cache/restore@v3
+      uses: actions/cache/restore@v4
       with:
         path: ~/.opam
         key: ${{ matrix.version }}
@@ -53,7 +53,7 @@ jobs:
     - name: Save cached opam
       if: steps.cache-opam-restore.outputs.cache-hit != 'true'
       id: cache-opam-save
-      uses: actions/cache/save@v3
+      uses: actions/cache/save@v4
       with:
         path: ~/.opam
         key: ${{ steps.cache-opam-restore.outputs.cache-primary-key }}
@@ -73,6 +73,19 @@ jobs:
         cd tests; USE_OPAM='' ./run-ci.sh
         cd ..
 
+    - 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: Install CN
       run: |
         opam switch ${{ matrix.version }}
@@ -85,24 +98,20 @@ jobs:
       with: 
         repository: rems-project/cn-tutorial
         path: cn-tutorial
-        # ref: fix-semicolon-syntax
 
-    # copying 'Run Cerberus CI tests'
     - name: Run CN CI tests
       run: |
         opam switch ${{ matrix.version }}
         eval $(opam env --switch=${{ matrix.version }})
         cd tests; USE_OPAM='' ./run-cn.sh
         cd ..
 
-    # copying 'Run Cerberus CI tests'
     - 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
 
-
     - name: Install Cerberus-CHERI
       if: ${{ matrix.version == '4.14.1' }}
       run: |

tests/run-cn-tutorial-ci.sh

@@ -1,6 +1,5 @@
 #!/bin/bash
 
-
 TUTORIAL_PATH=$1
 
 if [ -n "$TUTORIAL_PATH" ] 
@@ -11,68 +10,25 @@ else
     exit 1
 fi
 
-
-
 # copying from run-ci.sh
 export DYLD_LIBRARY_PATH=$DYLD_LIBRARY_PATH:`ocamlfind query z3`
 export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:`ocamlfind query z3`
 CN=$OPAM_SWITCH_PREFIX/bin/cn
 
 HERE=$(pwd)
 
-cd "$TUTORIAL_PATH"/src/example-archive/
-
-if [ -f ./check-all.sh ]; then
-    ./check-all.sh $CN
-    exit $?
-fi
+cd "$TUTORIAL_PATH"
 
 FAILURE=0
 
-cd dafny-tutorial
-../check.sh $CN
-if [ $? != 0 ] 
-then
-   FAILURE=1
-fi
-cd ..
+make check CN_PATH="$CN --solver-type=cvc5"
+FAILURE+=$?
 
-cd SAW
-../check.sh $CN
-if [ $? != 0 ] 
-then
-   FAILURE=1
-fi
-cd ..
-
-cd c-testsuite
-../check.sh $CN
-if [ $? != 0 ] 
-then
-   FAILURE=1
-fi
-cd ..
-
-cd simple-examples
-../check.sh $CN
-if [ $? != 0 ] 
-then
-   FAILURE=1
-fi
-cd ..
-
-
-cd ../..
-./check.sh $CN
-if [ $? != 0 ] 
-then
-   FAILURE=1
-fi
+make check CN_PATH="$CN --solver-type=z3"
+FAILURE+=$?
 
 cd $HERE
 
-
-
 if [ $FAILURE == 0 ]
 then
     echo "Ok"