Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Merged
merged 4 commits into from
Jul 17, 2024
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
1a2d603
Modify GH action to download and install cvc5
septract Jul 5, 2024
5cdbdfb
Make the CI script run both Z3 / CVC5
septract Jul 5, 2024
87708f9
Bump v to avoid deprecated nodejs
septract Jul 5, 2024
84916ff
Tidy up the tutorial repo CI by using the new `make check` target
septract Jul 10, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 15 additions & 6 deletions .github/workflows/ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 }}
Expand All @@ -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 }}
Expand All @@ -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 }}
Expand All @@ -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: |
Expand Down
54 changes: 5 additions & 49 deletions tests/run-cn-tutorial-ci.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
#!/bin/bash


TUTORIAL_PATH=$1

if [ -n "$TUTORIAL_PATH" ]
Expand All @@ -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"
Expand Down
Loading