From 042bf99f02455ea4332ccc3680639da61f5d4645 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 21 Nov 2023 13:52:20 +0000 Subject: [PATCH] Also build and test OpenBSD, NetBSD Uses the same virtualisation set-up as FreeBSD checks. --- .github/workflows/bsd.yaml | 110 +++++++++++++++++++++++++++++++++++++ 1 file changed, 110 insertions(+) diff --git a/.github/workflows/bsd.yaml b/.github/workflows/bsd.yaml index 324ffe510eb..2dc705c8ec5 100644 --- a/.github/workflows/bsd.yaml +++ b/.github/workflows/bsd.yaml @@ -60,3 +60,113 @@ jobs: gmake -C regression/cbmc test-paths-lifo env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2 # gmake -C jbmc/regression test-parallel JOBS=3 + + # This job takes approximately X to Y minutes + openbsd: + runs-on: macos-12 + steps: + - uses: actions/checkout@v3 + with: + submodules: recursive + - name: Prepare ccache + uses: actions/cache@v3 + with: + path: .ccache + key: openbsd-7.4-gmake-${{ github.ref }}-${{ github.sha }}-PR + restore-keys: | + openbsd-7.4-gmake-${{ github.ref }} + openbsd-7.4-gmake + - name: ccache environment + run: | + echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV + echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV + - name: Build and Test + uses: cross-platform-actions/action@v0.21.1 + with: + operating_system: openbsd + version: '7.4' + run: | + echo "Fetch dependencies" + sudo pkg install -y bash gmake git www/p5-libwww python python3 patch flex bison ccache parallel cvc5 z3 + echo "Fetch JBMC dependencies" + sudo pkg install -y openjdk8 wget maven + echo "Zero ccache stats and limit in size" + ccache -z --max-size=500M + echo "Build with gmake" + # don't do JBMC as to keep the overall time in check + gmake -C src minisat2-download + gmake -C src -j3 CXX="ccache clang++" + # gmake -C jbmc/src setup-submodules + # gmake -C jbmc/src -j3 CXX="ccache clang++" + gmake -C unit "CXX=ccache clang++" + # gmake -C jbmc/unit "CXX=ccache clang++" + echo "Print ccache stats" + ccache -s + echo "Checking completeness of help output" + scripts/check_help.sh clang++ + echo "Run unit tests" + gmake -C unit test + # gmake -C jbmc/unit test + echo "Running expected failure tests" + gmake TAGS="[!shouldfail]" -C unit test + # gmake TAGS="[!shouldfail]" -C jbmc/unit test + echo "Run regression tests" + gmake -C regression test-parallel JOBS=3 + gmake -C regression/cbmc test-paths-lifo + env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2 + # gmake -C jbmc/regression test-parallel JOBS=3 + + # This job takes approximately X to Y minutes + netbsd: + runs-on: macos-12 + steps: + - uses: actions/checkout@v3 + with: + submodules: recursive + - name: Prepare ccache + uses: actions/cache@v3 + with: + path: .ccache + key: netbsd-9.3-gmake-${{ github.ref }}-${{ github.sha }}-PR + restore-keys: | + netbsd-9.3-gmake-${{ github.ref }} + netbsd-9.3-gmake + - name: ccache environment + run: | + echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV + echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV + - name: Build and Test + uses: cross-platform-actions/action@v0.21.1 + with: + operating_system: netbsd + version: '9.3' + run: | + echo "Fetch dependencies" + sudo pkg install -y bash gmake git www/p5-libwww python python3 patch flex bison ccache parallel cvc5 z3 + echo "Fetch JBMC dependencies" + sudo pkg install -y openjdk8 wget maven + echo "Zero ccache stats and limit in size" + ccache -z --max-size=500M + echo "Build with gmake" + # don't do JBMC as to keep the overall time in check + gmake -C src minisat2-download + gmake -C src -j3 CXX="ccache clang++" + # gmake -C jbmc/src setup-submodules + # gmake -C jbmc/src -j3 CXX="ccache clang++" + gmake -C unit "CXX=ccache clang++" + # gmake -C jbmc/unit "CXX=ccache clang++" + echo "Print ccache stats" + ccache -s + echo "Checking completeness of help output" + scripts/check_help.sh clang++ + echo "Run unit tests" + gmake -C unit test + # gmake -C jbmc/unit test + echo "Running expected failure tests" + gmake TAGS="[!shouldfail]" -C unit test + # gmake TAGS="[!shouldfail]" -C jbmc/unit test + echo "Run regression tests" + gmake -C regression test-parallel JOBS=3 + gmake -C regression/cbmc test-paths-lifo + env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2 + # gmake -C jbmc/regression test-parallel JOBS=3