diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7f5ad5932..5027d1ce2 100644 --- a/.github/workflows/ci.yml +++ b/.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,9 +98,7 @@ 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 }} @@ -95,14 +106,12 @@ jobs: 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: | diff --git a/tests/run-cn-tutorial-ci.sh b/tests/run-cn-tutorial-ci.sh index d66ecf3aa..b03c7ce59 100755 --- a/tests/run-cn-tutorial-ci.sh +++ b/tests/run-cn-tutorial-ci.sh @@ -1,6 +1,5 @@ #!/bin/bash - TUTORIAL_PATH=$1 if [ -n "$TUTORIAL_PATH" ] @@ -11,8 +10,6 @@ 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` @@ -20,59 +17,18 @@ 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"