Skip to content

Commit 90f01b5

Browse files
tautschnigtautschnig
committed
GitHub CI: Move number of Linux/Windows vCPUs to config variable
The churn in the preceding commit should be avoided for future infrastructure upgrades.
1 parent 55e5bdf commit 90f01b5

File tree

1 file changed

+43
-41
lines changed

1 file changed

+43
-41
lines changed

‎.github/workflows/pull-request-checks.yaml

Lines changed: 43 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,8 @@ on:
66
branches: [ develop ]
77
env:
88
cvc5-version: "1.0.0"
9+
linux-vcpus: 4
10+
windows-vcpus: 4
911

1012
jobs:
1113
# This job takes approximately 21 to 40 minutes
@@ -50,13 +52,13 @@ jobs:
5052
run: |
5153
git clone https://github.com/conp-solutions/riss riss.git
5254
cmake -Hriss.git -Briss.git/release -DCMAKE_BUILD_TYPE=Release
53-
make -C riss.git/release riss-coprocessor-lib-static -j4
54-
make -C src -j4 CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
55-
make -C jbmc/src -j4 CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
55+
make -C riss.git/release riss-coprocessor-lib-static -j${{env.linux-vcpus}}
56+
make -C src -j${{env.linux-vcpus}} CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
57+
make -C jbmc/src -j${{env.linux-vcpus}} CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
5658
57-
make -C unit -j4 CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
59+
make -C unit -j${{env.linux-vcpus}} CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
5860
59-
make -C jbmc/unit -j4 CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
61+
make -C jbmc/unit -j${{env.linux-vcpus}} CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
6062
- name: Print ccache stats
6163
run: ccache -s
6264
- name: Checking completeness of help output
@@ -70,10 +72,10 @@ jobs:
7072
make TAGS="[!shouldfail]" -C jbmc/unit test IPASIR=$PWD/riss.git/riss
7173
- name: Run regression tests
7274
run: |
73-
make -C regression test-parallel JOBS=4 LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
75+
make -C regression test-parallel JOBS=${{env.linux-vcpus}} LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
7476
make -C regression/cbmc test-paths-lifo
7577
env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
76-
make -C jbmc/regression test-parallel JOBS=4
78+
make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}}
7779
- name: Check cleanup
7880
run: |
7981
make -C src clean IPASIR=$PWD/riss.git/riss
@@ -134,10 +136,10 @@ jobs:
134136
run: ccache -z --max-size=500M
135137
- name: Build with make
136138
run: |
137-
make -C src -j4 MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
138-
make -C unit -j4
139-
make -C jbmc/src -j4
140-
make -C jbmc/unit -j4
139+
make -C src -j${{env.linux-vcpus}} MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
140+
make -C unit -j${{env.linux-vcpus}}
141+
make -C jbmc/src -j${{env.linux-vcpus}}
142+
make -C jbmc/unit -j${{env.linux-vcpus}}
141143
- name: Print ccache stats
142144
run: ccache -s
143145
- name: Run unit tests
@@ -151,10 +153,10 @@ jobs:
151153
make TAGS="[!shouldfail]" -C jbmc/unit test
152154
- name: Run regression tests
153155
run: |
154-
make -C regression test-parallel JOBS=4
156+
make -C regression test-parallel JOBS=${{env.linux-vcpus}}
155157
make -C regression/cbmc test-paths-lifo
156158
env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
157-
make -C jbmc/regression test-parallel JOBS=4
159+
make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}}
158160
159161
# This job has been copied from the one above it, and modified to only build CBMC
160162
# and run the `regression/cbmc/` regression tests against Z3. The rest of the tests
@@ -198,7 +200,7 @@ jobs:
198200
- name: Zero ccache stats and limit in size
199201
run: ccache -z --max-size=500M
200202
- name: Build with make
201-
run: make -C src -j4
203+
run: make -C src -j${{env.linux-vcpus}}
202204
- name: Print ccache stats
203205
run: ccache -s
204206
- name: Run regression/cbmc tests with z3 as the backend
@@ -247,7 +249,7 @@ jobs:
247249
- name: Zero ccache stats and limit in size
248250
run: ccache -z --max-size=500M
249251
- name: Build with Ninja
250-
run: ninja -C build -j4
252+
run: ninja -C build -j${{env.linux-vcpus}}
251253
- name: Print ccache stats
252254
run: ccache -s
253255
- name: Checking completeness of help output
@@ -258,7 +260,7 @@ jobs:
258260
ninja package
259261
ls *.deb
260262
- name: Run tests
261-
run: cd build; ctest . -V -L CORE -j4
263+
run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}}
262264
- name: Check cleanup
263265
run: |
264266
rm -r build
@@ -320,10 +322,10 @@ jobs:
320322
make -C src/cpp library_check
321323
- name: Build with make
322324
run: |
323-
make -C src -j4 MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
324-
make -C unit -j4
325-
make -C jbmc/src -j4
326-
make -C jbmc/unit -j4
325+
make -C src -j${{env.linux-vcpus}} MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
326+
make -C unit -j${{env.linux-vcpus}}
327+
make -C jbmc/src -j${{env.linux-vcpus}}
328+
make -C jbmc/unit -j${{env.linux-vcpus}}
327329
- name: Print ccache stats
328330
run: ccache -s
329331
- name: Run unit tests
@@ -337,10 +339,10 @@ jobs:
337339
make TAGS="[!shouldfail]" -C jbmc/unit test
338340
- name: Run regression tests
339341
run: |
340-
make -C regression test-parallel JOBS=4
342+
make -C regression test-parallel JOBS=${{env.linux-vcpus}}
341343
make -C regression/cbmc test-paths-lifo
342344
env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
343-
make -C jbmc/regression test-parallel JOBS=4
345+
make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}}
344346
345347
# This job takes approximately 22 to 41 minutes
346348
check-ubuntu-22_04-cmake-gcc:
@@ -385,7 +387,7 @@ jobs:
385387
- name: Zero ccache stats and limit in size
386388
run: ccache -z --max-size=500M
387389
- name: Build with Ninja
388-
run: ninja -C build -j4
390+
run: ninja -C build -j${{env.linux-vcpus}}
389391
- name: Print ccache stats
390392
run: ccache -s
391393
- name: Check if package building works
@@ -394,7 +396,7 @@ jobs:
394396
ninja package
395397
ls *.deb
396398
- name: Run tests
397-
run: cd build; ctest . -V -L CORE -j4
399+
run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}}
398400

399401
# This job takes approximately 26 to 46 minutes
400402
check-ubuntu-24_04-cmake-gcc-13:
@@ -443,11 +445,11 @@ jobs:
443445
- name: Zero ccache stats and limit in size
444446
run: ccache -z --max-size=500M
445447
- name: Build with Ninja
446-
run: ninja -C build -j4
448+
run: ninja -C build -j${{env.linux-vcpus}}
447449
- name: Print ccache stats
448450
run: ccache -s
449451
- name: Run tests
450-
run: cd build; ctest . -V -L CORE -j4
452+
run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}}
451453

452454
# This job takes approximately 30 to 60 minutes
453455
check-ubuntu-22_04-cmake-gcc-32bit:
@@ -490,11 +492,11 @@ jobs:
490492
- name: Zero ccache stats and limit in size
491493
run: ccache -z --max-size=500M
492494
- name: Build with Ninja
493-
run: ninja -C build -j4
495+
run: ninja -C build -j${{env.linux-vcpus}}
494496
- name: Print ccache stats
495497
run: ccache -s
496498
- name: Run tests
497-
run: cd build; ctest . -V -L CORE -j4
499+
run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}}
498500

499501
# This job takes approximately 5 to 24 minutes
500502
check-ubuntu-20_04-cmake-gcc-KNOWNBUG:
@@ -529,13 +531,13 @@ jobs:
529531
- name: Zero ccache stats and limit in size
530532
run: ccache -z --max-size=500M
531533
- name: Build with Ninja
532-
run: ninja -C build -j4
534+
run: ninja -C build -j${{env.linux-vcpus}}
533535
- name: Print ccache stats
534536
run: ccache -s
535537
- name: Run tests
536538
run: |
537539
cd build
538-
ctest . -V -L KNOWNBUG -j4
540+
ctest . -V -L KNOWNBUG -j${{env.linux-vcpus}}
539541
export PATH=$PWD/bin:$PATH
540542
cd ../regression/cbmc
541543
sed -i '1s/^CORE\(.*\)broken-smt-backend/KNOWNBUG\1broken-smt-backend/' */*.desc
@@ -576,11 +578,11 @@ jobs:
576578
- name: Zero ccache stats and limit in size
577579
run: ccache -z --max-size=500M
578580
- name: Build with Ninja
579-
run: ninja -C build -j4
581+
run: ninja -C build -j${{env.linux-vcpus}}
580582
- name: Print ccache stats
581583
run: ccache -s
582584
- name: Run tests
583-
run: cd build; ctest . -V -L THOROUGH -j4
585+
run: cd build; ctest . -V -L THOROUGH -j${{env.linux-vcpus}}
584586

585587
# This job takes approximately 39 to 69 minutes
586588
check-macos-13-make-clang:
@@ -732,7 +734,7 @@ jobs:
732734
- name: Test cbmc
733735
run: |
734736
Set-Location build
735-
ctest -V -L CORE -C Release . -j4
737+
ctest -V -L CORE -C Release . -j${{env.windows-vcpus}}
736738
737739
# This job takes approximately 65 to 84 minutes
738740
check-vs-2022-make-build-and-test:
@@ -784,15 +786,15 @@ jobs:
784786
- name: Download minisat with make
785787
run: make -C src minisat2-download
786788
- name: Build CBMC with make
787-
run: make CXX=clcache BUILD_ENV=MSVC -j4 -C src
789+
run: make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C src
788790
- name: Build unit tests with make
789-
run: make CXX=clcache BUILD_ENV=MSVC -j4 -C unit all
791+
run: make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C unit all
790792
- name: Build jbmc with make
791793
run: |
792-
make CXX=clcache -j4 -C jbmc/src setup-submodules
793-
make CXX=clcache BUILD_ENV=MSVC -j4 -C jbmc/src
794+
make CXX=clcache -j${{env.windows-vcpus}} -C jbmc/src setup-submodules
795+
make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C jbmc/src
794796
- name: Build JBMC unit tests
795-
run: make CXX=clcache BUILD_ENV=MSVC -j4 -C jbmc/unit all
797+
run: make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C jbmc/unit all
796798
- name: Print ccache stats
797799
run: clcache -s
798800
- name: Run CBMC and JBMC unit tests
@@ -906,7 +908,7 @@ jobs:
906908
run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++
907909
- name: Run include-what-you-use
908910
run: |
909-
iwyu_tool -p build/compile_commands.json -j4 | tee includes.txt
911+
iwyu_tool -p build/compile_commands.json -j${{env.linux-vcpus}} | tee includes.txt
910912
if sed '/minisat2-src/,/^--$/d' includes.txt | grep '^- ' -B1 ; then
911913
echo "Unnecessary includes found. Use '// IWYU pragma: keep' to override this."
912914
exit 1
@@ -960,13 +962,13 @@ jobs:
960962
- name: Zero ccache stats and limit in size
961963
run: ccache -z --max-size=7G
962964
- name: Execute CMake CBMC build
963-
run: cmake --build build -- -j4
965+
run: cmake --build build -- -j${{env.linux-vcpus}}
964966
- name: Print ccache stats
965967
run: ccache -s
966968
- name: Run CTest and collect coverage statistics
967969
run: |
968970
echo "lcov_excl_line = UNREACHABLE" > ~/.lcovrc
969-
cmake --build build --target coverage -- -j4
971+
cmake --build build --target coverage -- -j${{env.linux-vcpus}}
970972
- name: Upload coverage statistics to Codecov
971973
uses: codecov/codecov-action@v4
972974
with:

0 commit comments

Comments
 (0)