Skip to content

Commit

Permalink
Use 4 vCPUs for running coverage-recording tests
Browse files Browse the repository at this point in the history
We changed the number of vCPUs for most scenarios in 55e5bdf, but
failed to also propagate this to coverage-recording test execution.
  • Loading branch information
tautschnig committed Jun 21, 2024
1 parent 3e5e423 commit 7cb9ed2
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions .github/workflows/coverage.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ env:
windows-vcpus: 4

jobs:
# This job takes approximately 40 to 75 minutes
# This job takes approximately 22 to 75 minutes
Linux:
runs-on: ubuntu-20.04
steps:
Expand Down Expand Up @@ -54,7 +54,7 @@ jobs:
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
- name: Configure CMake CBMC build with coverage instrumentation parameters
run: cmake -S . -Bbuild -Denable_coverage=1 -Dparallel_tests=2 -DCMAKE_CXX_COMPILER=/usr/bin/g++
run: cmake -S . -Bbuild -Denable_coverage=1 -Dparallel_tests=${{env.linux-vcpus}} -DCMAKE_CXX_COMPILER=/usr/bin/g++
- name: Zero ccache stats and limit in size
run: ccache -z --max-size=7G
- name: Execute CMake CBMC build
Expand Down

0 comments on commit 7cb9ed2

Please sign in to comment.