From: Gereon Kremer <gkremer@cs.stanford.edu>
Date: Sat, 2 Apr 2022 20:03:56 +0000 (+0200)
Subject: use one process more than we have cores (#8545)
X-Git-Tag: cvc5-1.0.0~34
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=afdc254640a2c8535c10feb6662793c12011b86e;p=cvc5.git

use one process more than we have cores (#8545)

This PR uses one process more than we have cores in the CI. This speeds up the CI jobs when time is spent waiting on IO instead of actually using the CPU.
---

diff --git a/.github/actions/install-dependencies/action.yml b/.github/actions/install-dependencies/action.yml
index 1dc3a1ad3..85bf208da 100644
--- a/.github/actions/install-dependencies/action.yml
+++ b/.github/actions/install-dependencies/action.yml
@@ -38,7 +38,7 @@ runs:
         echo "SED=sed" >> $GITHUB_ENV
         echo "CCACHE_CONFIGPATH=/home/runner/.ccache/ccache.conf" >> $GITHUB_ENV
         echo "image_version=$ImageVersion" >> $GITHUB_ENV
-        echo "num_proc=$(nproc)" >> $GITHUB_ENV
+        echo "num_proc=$(( $(nproc) + 1 ))" >> $GITHUB_ENV
         echo "/usr/lib/ccache" >> $GITHUB_PATH
         echo "::endgroup::"
 
@@ -81,7 +81,7 @@ runs:
         echo "SED=gsed" >> $GITHUB_ENV
         echo "CCACHE_CONFIGPATH=/Users/runner/Library/Preferences/ccache/ccache.conf" >> $GITHUB_ENV
         echo "image_version=$ImageVersion" >> $GITHUB_ENV
-        echo "num_proc=$(sysctl -n hw.logicalcpu)" >> $GITHUB_ENV
+        echo "num_proc=$(( $(sysctl -n hw.logicalcpu) + 1 ))" >> $GITHUB_ENV
         echo "/usr/local/opt/ccache/libexec" >> $GITHUB_PATH
         echo "::endgroup::"