Build and infrastructure fixes for FreeBSD #32
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" | |
| setenv CCACHE_BASEDIR $PWD | |
| setenv CCACHE_DIR $PWD/.ccache | |
| ccache -z --max-size=500M | |
| ccache -p | |
| 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" | |
| set histchars | |
| 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 34 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 llvm%16 git python3 bison ccache parallel z3 | |
| sudo ln -s $(which llvm-ar-16) /usr/local/bin/llvm-ar | |
| echo "Fetch JBMC dependencies" | |
| sudo pkg_add -v jdk%1.8 wget maven | |
| echo "Zero ccache stats and limit in size" | |
| export CCACHE_BASEDIR=$PWD | |
| export CCACHE_DIR=$PWD/.ccache | |
| ccache -z --max-size=500M | |
| ccache -p | |
| echo "Build with gmake" | |
| gmake -C src minisat2-download | |
| # we only build util.a to keep job execution time in check | |
| gmake -C src -j2 CXX="ccache clang++" util.dir | |
| # # don't do JBMC so as to keep the overall time in check | |
| # 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 21 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 pkgin -y install bash gmake git python311 patch flex bison ccache parallel z3 | |
| sudo ln -s $(which python3.11) /usr/pkg/bin/python3 | |
| echo "Fetch JBMC dependencies" | |
| sudo pkgin -y install openjdk8 wget apache-maven | |
| echo "Zero ccache stats and limit in size" | |
| export CCACHE_BASEDIR=$PWD | |
| export CCACHE_DIR=$PWD/.ccache | |
| ccache -z --max-size=500M | |
| ccache -p | |
| echo "Build with gmake" | |
| gmake -C src minisat2-download | |
| # we only build util.a to keep job execution time in check | |
| gmake -C src -j2 CXX="ccache g++" util.dir | |
| # # don't do JBMC so as to keep the overall time in check | |
| # gmake -C src -j2 CXX="ccache g++" | |
| # # gmake -C jbmc/src setup-submodules | |
| # # gmake -C jbmc/src -j2 CXX="ccache g++" | |
| # gmake -C unit "CXX=ccache g++" | |
| # # gmake -C jbmc/unit "CXX=ccache g++" | |
| # echo "Print ccache stats" | |
| # ccache -s | |
| # echo "Checking completeness of help output" | |
| # scripts/check_help.sh g++ | |
| # echo "Run unit tests" | |
| # # ignore failures for the moment | |
| # 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 |