Build and infrastructure fixes for FreeBSD #22
Workflow file for this run
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Build and Test on *BSD | |
| on: | |
| push: | |
| branches: [ develop ] | |
| pull_request: | |
| branches: [ develop ] | |
| jobs: | |
| # This job takes approximately X to Y minutes | |
| FreeBSD: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v3 | |
| with: | |
| submodules: recursive | |
| - name: Prepare ccache | |
| uses: actions/cache@v3 | |
| with: | |
| path: .ccache | |
| key: freebsd-13.2-gmake-${{ github.ref }}-${{ github.sha }}-PR | |
| restore-keys: | | |
| freebsd-13.2-gmake-${{ github.ref }} | |
| freebsd-13.2-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/[email protected] | |
| with: | |
| operating_system: freebsd | |
| version: '13.2' | |
| hypervisor: qemu | |
| 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 -j2 CXX="ccache clang++" | |
| # gmake -C jbmc/src setup-submodules | |
| # gmake -C jbmc/src -j2 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=2 | |
| 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=2 | |
| # This job takes approximately X to Y minutes | |
| OpenBSD: | |
| runs-on: ubuntu-latest | |
| 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/[email protected] | |
| with: | |
| operating_system: openbsd | |
| version: '7.4' | |
| hypervisor: qemu | |
| run: | | |
| echo "Fetch dependencies" | |
| sudo pkg_add -v bash gmake llvm16 git python3 bison ccache parallel z3 | |
| echo "Fetch JBMC dependencies" | |
| sudo pkg_add -v jdk1.8 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 -j2 CXX="ccache clang++" | |
| # gmake -C jbmc/src setup-submodules | |
| # gmake -C jbmc/src -j2 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=2 | |
| 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=2 | |
| # This job takes approximately X to Y minutes | |
| NetBSD: | |
| runs-on: ubuntu-latest | |
| 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/[email protected] | |
| with: | |
| operating_system: netbsd | |
| version: '9.3' | |
| hypervisor: qemu | |
| run: | | |
| echo "Fetch dependencies" | |
| export PATH=/usr/pkg/sbin:/usr/pkg/bin:$PATH | |
| export PKG_PATH=https://cdn.netbsd.org/pub/pkgsrc/packages/NetBSD/amd64/9.3/All/ | |
| # sudo --preserve-env=PKG_PATH pkg_add -v pkgin | |
| sudo pkgin -y install bash gmake git python311 patch flex bison ccache parallel z3 | |
| echo "Fetch JBMC dependencies" | |
| sudo pkgin -y install openjdk8 wget apache-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 -j2 CXX="ccache clang++" | |
| # gmake -C jbmc/src setup-submodules | |
| # gmake -C jbmc/src -j2 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=2 | |
| 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=2 |