Skip to content

Commit a537fc0

Browse files
tautschnigtautschnig
committed
Use vmactions
This appears to have much better performance (FreeBSD job completes in 26 minutes instead of 4 hours). We can now also enable the same number of steps in OpenBSD and NetBSD.
1 parent 711deca commit a537fc0

File tree

1 file changed

+67
-67
lines changed

1 file changed

+67
-67
lines changed

‎.github/workflows/bsd.yaml

+67-67
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ on:
66
branches: [ develop ]
77

88
jobs:
9-
# This job takes approximately X to Y minutes
9+
# This job takes approximately 6 to 26 minutes
1010
FreeBSD:
1111
runs-on: ubuntu-latest
1212
steps:
@@ -26,19 +26,20 @@ jobs:
2626
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
2727
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
2828
- name: Build and Test
29-
uses: cross-platform-actions/[email protected]
29+
uses: vmactions/freebsd-vm@v1
3030
with:
31-
operating_system: freebsd
32-
version: '13.2'
33-
hypervisor: qemu
31+
release: 13.2
32+
usesh: true
3433
run: |
34+
# apparently fail-on-error isn't the default here
35+
set -e -x
3536
echo "Fetch dependencies"
36-
sudo pkg install -y bash gmake git www/p5-libwww python python3 patch flex bison ccache parallel cvc5 z3
37+
pkg install -y bash gmake git www/p5-libwww python python3 patch flex bison ccache parallel cvc5 z3
3738
echo "Fetch JBMC dependencies"
38-
sudo pkg install -y openjdk8 wget maven
39+
pkg install -y openjdk8 wget maven
3940
echo "Zero ccache stats and limit in size"
40-
setenv CCACHE_BASEDIR $PWD
41-
setenv CCACHE_DIR $PWD/.ccache
41+
export CCACHE_BASEDIR=$PWD
42+
export CCACHE_DIR=$PWD/.ccache
4243
ccache -z --max-size=500M
4344
ccache -p
4445
echo "Build with gmake"
@@ -57,7 +58,6 @@ jobs:
5758
gmake -C unit test
5859
# gmake -C jbmc/unit test
5960
echo "Running expected failure tests"
60-
set histchars
6161
gmake TAGS='[!shouldfail]' -C unit test
6262
# gmake TAGS='[!shouldfail]' -C jbmc/unit test
6363
echo "Run regression tests"
@@ -67,7 +67,7 @@ jobs:
6767
# env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
6868
# # gmake -C jbmc/regression test-parallel JOBS=2
6969
70-
# This job takes approximately X to 34 minutes
70+
# This job takes approximately 7 to 34 minutes
7171
OpenBSD:
7272
runs-on: ubuntu-latest
7373
steps:
@@ -87,49 +87,48 @@ jobs:
8787
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
8888
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
8989
- name: Build and Test
90-
uses: cross-platform-actions/[email protected]
90+
uses: vmactions/openbsd-vm@v1
9191
with:
92-
operating_system: openbsd
93-
version: '7.4'
94-
hypervisor: qemu
92+
release: 7.4
9593
run: |
94+
# apparently fail-on-error isn't the default here
95+
set -e -x
9696
echo "Fetch dependencies"
97-
sudo pkg_add -v bash gmake llvm%16 git python3 bison ccache parallel z3
98-
sudo ln -s $(which llvm-ar-16) /usr/local/bin/llvm-ar
97+
pkg_add -v bash gmake llvm%16 git python3 bison ccache parallel z3
98+
ln -s $(which llvm-ar-16) /usr/local/bin/llvm-ar
9999
echo "Fetch JBMC dependencies"
100-
sudo pkg_add -v jdk%1.8 wget maven
100+
pkg_add -v jdk%1.8 wget maven
101101
echo "Zero ccache stats and limit in size"
102102
export CCACHE_BASEDIR=$PWD
103103
export CCACHE_DIR=$PWD/.ccache
104104
ccache -z --max-size=500M
105105
ccache -p
106106
echo "Build with gmake"
107+
# don't do JBMC so as to keep the overall time in check
107108
gmake -C src minisat2-download
108-
# we only build util.a to keep job execution time in check
109-
gmake -C src -j2 CXX="ccache clang++" util.dir
110-
# # don't do JBMC so as to keep the overall time in check
111-
# gmake -C src -j2 CXX="ccache clang++"
112-
# # gmake -C jbmc/src setup-submodules
113-
# # gmake -C jbmc/src -j2 CXX="ccache clang++"
114-
# gmake -C unit "CXX=ccache clang++"
115-
# # gmake -C jbmc/unit "CXX=ccache clang++"
116-
# echo "Print ccache stats"
117-
# ccache -s
118-
# echo "Checking completeness of help output"
119-
# scripts/check_help.sh clang++
120-
# echo "Run unit tests"
121-
# gmake -C unit test
122-
# # gmake -C jbmc/unit test
123-
# echo "Running expected failure tests"
124-
# gmake TAGS='[!shouldfail]' -C unit test
125-
# # gmake TAGS='[!shouldfail]' -C jbmc/unit test
126-
# echo "Run regression tests"
109+
gmake -C src -j2 CXX="ccache clang++"
110+
# gmake -C jbmc/src setup-submodules
111+
# gmake -C jbmc/src -j2 CXX="ccache clang++"
112+
gmake -C unit "CXX=ccache clang++"
113+
# gmake -C jbmc/unit "CXX=ccache clang++"
114+
echo "Print ccache stats"
115+
ccache -s
116+
echo "Checking completeness of help output"
117+
scripts/check_help.sh clang++
118+
echo "Run unit tests"
119+
gmake -C unit test
120+
# gmake -C jbmc/unit test
121+
echo "Running expected failure tests"
122+
gmake TAGS='[!shouldfail]' -C unit test
123+
# gmake TAGS='[!shouldfail]' -C jbmc/unit test
124+
echo "Run regression tests"
125+
gmake -C regression/cbmc test
127126
# gmake -C regression test-parallel JOBS=2
128127
# gmake -C regression/cbmc test-paths-lifo
129128
# env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
130129
# # gmake -C jbmc/regression test-parallel JOBS=2
131130
132-
# This job takes approximately X to 21 minutes
131+
# This job takes approximately 6 to 29 minutes
133132
NetBSD:
134133
runs-on: ubuntu-latest
135134
steps:
@@ -149,43 +148,44 @@ jobs:
149148
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
150149
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
151150
- name: Build and Test
152-
uses: cross-platform-actions/[email protected]
151+
uses: vmactions/netbsd-vm@v1
153152
with:
154-
operating_system: netbsd
155-
version: '9.3'
156-
hypervisor: qemu
153+
release: 9.3
157154
run: |
155+
# apparently fail-on-error isn't the default here
156+
set -e -x
158157
echo "Fetch dependencies"
159-
export PATH=/usr/pkg/sbin:/usr/pkg/bin:$PATH
160-
export PKG_PATH=https://cdn.netbsd.org/pub/pkgsrc/packages/NetBSD/amd64/9.3/All/
161-
sudo pkgin -y install bash gmake git python311 patch flex bison ccache parallel z3
162-
sudo ln -s $(which python3.11) /usr/pkg/bin/python3
158+
pkg_add -v bash gmake git python311 patch flex bison ccache parallel z3 gcc10
159+
ln -s $(which python3.11) /usr/pkg/bin/python3
160+
export PATH=/usr/pkg/gcc10/bin:$PATH
163161
echo "Fetch JBMC dependencies"
164-
sudo pkgin -y install openjdk8 wget apache-maven
162+
pkg_add -v openjdk8 wget apache-maven
165163
echo "Zero ccache stats and limit in size"
166164
export CCACHE_BASEDIR=$PWD
167165
export CCACHE_DIR=$PWD/.ccache
168166
ccache -z --max-size=500M
169167
ccache -p
170168
echo "Build with gmake"
169+
# don't do JBMC so as to keep the overall time in check
171170
gmake -C src minisat2-download
172-
# we only build util.a to keep job execution time in check
173-
gmake -C src -j2 CXX="ccache g++" util.dir
174-
# # don't do JBMC so as to keep the overall time in check
175-
# gmake -C src -j2 CXX="ccache g++"
176-
# # gmake -C jbmc/src setup-submodules
177-
# # gmake -C jbmc/src -j2 CXX="ccache g++"
178-
# gmake -C unit "CXX=ccache g++"
179-
# # gmake -C jbmc/unit "CXX=ccache g++"
180-
# echo "Print ccache stats"
181-
# ccache -s
182-
# echo "Checking completeness of help output"
183-
# scripts/check_help.sh g++
184-
# echo "Run unit tests"
185-
# # ignore failures for the moment
186-
# gmake -C unit test
187-
# # gmake -C jbmc/unit test
188-
# echo "Running expected failure tests"
189-
# gmake TAGS='[!shouldfail]' -C unit test
190-
# # gmake TAGS='[!shouldfail]' -C jbmc/unit test
191-
# echo "Run regression tests"
171+
gmake -C src -j2 CXX="ccache g++"
172+
# gmake -C jbmc/src setup-submodules
173+
# gmake -C jbmc/src -j2 CXX="ccache g++"
174+
gmake -C unit "CXX=ccache g++"
175+
# gmake -C jbmc/unit "CXX=ccache g++"
176+
echo "Print ccache stats"
177+
ccache -s
178+
echo "Checking completeness of help output"
179+
scripts/check_help.sh g++
180+
echo "Run unit tests"
181+
gmake -C unit test
182+
# gmake -C jbmc/unit test
183+
echo "Running expected failure tests"
184+
gmake TAGS='[!shouldfail]' -C unit test
185+
# gmake TAGS='[!shouldfail]' -C jbmc/unit test
186+
echo "Run regression tests"
187+
gmake -C regression/cbmc test
188+
# gmake -C regression test-parallel JOBS=2
189+
# gmake -C regression/cbmc test-paths-lifo
190+
# env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
191+
# # gmake -C jbmc/regression test-parallel JOBS=2

0 commit comments

Comments
 (0)