Build shared and static in CI (#7472)

This PR changes our strategy to deal with shared vs. static builds in CI jobs.
All jobs now build cvc5 both shared and static by default. The builds happen in different build directories (build-shared and build-static), and we configure ccache such that these two build directories share a common cache.

7 files changed, 106 insertions, 21 deletions

diff --git a/.github/actions/add-to-release/action.yml b/.github/actions/add-to-release/action.yml
index 1db34bdf8..a5939e20c 100644
--- a/.github/actions/add-to-release/action.yml
+++ b/.github/actions/add-to-release/action.yml
@@ -1,6 +1,8 @@
 name: Add binary to release
 description: Add cvc5 binary to the current release
 inputs:
+  binary:
+    description: file name of binary
   github-token:
     description: token to upload binary
 runs:
@@ -9,7 +11,7 @@ runs:
     - name: Rename binaries for release
       shell: bash
       run: |
-        cp build/bin/cvc5 cvc5-${{ runner.os }}
+        cp ${{ inputs.binary }} cvc5-${{ runner.os }}
 
     - name: Add binaries to release
       uses: softprops/action-gh-release@v1
diff --git a/.github/actions/build-documentation/action.yml b/.github/actions/build-documentation/action.yml
index cb5587c51..8224ac4bb 100644
--- a/.github/actions/build-documentation/action.yml
+++ b/.github/actions/build-documentation/action.yml
@@ -1,5 +1,8 @@
 name: Build documentation
 description: Build documentation and store it as artifact
+inputs:
+  build-dir:
+    default: build
 runs:
   using: composite
   steps:
@@ -10,10 +13,10 @@ runs:
         if [ "${{ github.event_name }}" == "pull_request" ] ; then
           echo "${{ github.event.number }}" > docs/sphinx-gh/prnum
         fi
-      working-directory: build
+      working-directory: ${{ inputs.build-dir }}
     
     - name: Store Documentation
       uses: actions/upload-artifact@v2
       with:
         name: documentation
-        path: build/docs/sphinx-gh/
+        path: ${{ inputs.build-dir }}/docs/sphinx-gh/
diff --git a/.github/actions/configure-and-build/action.yml b/.github/actions/configure-and-build/action.yml
new file mode 100644
index 000000000..4e2bea7a1
--- /dev/null
+++ b/.github/actions/configure-and-build/action.yml
@@ -0,0 +1,62 @@
+name: Configure and build
+description: Run configure script and build
+inputs:
+  configure-env:
+    default: ""
+  configure-config:
+    default: ""
+  build-shared:
+    default: true
+  build-static:
+    default: true
+outputs:
+  shared-build-dir:
+    description: build directory of the shared build
+    value: ${{ steps.shared-build.outputs.build-dir }}
+  static-build-dir:
+    description: build directory of the static build
+    value: ${{ steps.static-build.outputs.build-dir }}
+runs:
+  using: composite
+  steps:
+    - name: Shared build
+      id: shared-build
+      shell: bash
+      run: |
+        echo "::group::Shared build"
+        if [[ "${{ inputs.build-shared }}" != "true" ]]; then exit 0; fi
+        ${{ inputs.configure-env }} ./configure.sh ${{ inputs.configure-config }} \
+          --prefix=$(pwd)/build-shared/install --werror --name=build-shared
+        
+        # can not use `ccache --set-config=base_dir=` due to ccache bug, fixed with 3.7.10
+        cd build-shared/ && pwd=$(pwd)
+        $SED -i.orig -n -e '/^base_dir = /!p' -e "\$abase_dir = $pwd" $CCACHE_CONFIGPATH
+        
+        make -j${{ env.num_proc }}
+
+        echo "::set-output name=build-dir::$pwd"
+        echo "::endgroup::"
+
+    - name: Static build
+      id: static-build
+      shell: bash
+      run: |
+        echo "::group::Static build"
+        if [[ "${{ inputs.build-static }}" != "true" ]]; then exit 0; fi
+        ${{ inputs.configure-env }} ./configure.sh ${{ inputs.configure-config }} \
+          --prefix=$(pwd)/build-static/install --werror --static --name=build-static
+
+        cd build-static/ && pwd=$(pwd)
+        $SED -i.orig -n -e '/^base_dir = /!p' -e "\$abase_dir = $pwd" $CCACHE_CONFIGPATH
+
+        make -j${{ env.num_proc }}
+
+        echo "::set-output name=build-dir::$pwd"
+        echo "::endgroup::"
+        
+    - name: Reset ccache base_dir
+      shell: bash
+      run: |
+        echo "::group::Reset ccache base_dir"
+        $SED -i.orig -n -e '/^base_dir = /!p' -e "\$abase_dir =" $CCACHE_CONFIGPATH
+        echo "::endgroup::"
diff --git a/.github/actions/install-dependencies/action.yml b/.github/actions/install-dependencies/action.yml
index f019594b2..d1fb975a9 100644
--- a/.github/actions/install-dependencies/action.yml
+++ b/.github/actions/install-dependencies/action.yml
@@ -11,6 +11,7 @@ runs:
     - name: Install Linux software
       shell: bash
       run: |
+        echo "::group::Install Linux software"
         if [[ $RUNNER_OS != "Linux" ]]; then exit 0; fi
         sudo apt-get update
         sudo apt-get install -y \
@@ -34,14 +35,18 @@ runs:
         # variables of the runner are not automatically imported:
         #
         # https://github.com/actions/runner/blob/master/docs/adrs/0278-env-context.md#dont-populate-the-env-context-with-environment-variables-from-runner-machine
+        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 "/usr/lib/ccache" >> $GITHUB_PATH
+        echo "::endgroup::"
 
     # Note: macOS comes with a libedit; it does not need to brew-installed
     - name: Install macOS software
       shell: bash
       run: |
+        echo "::group::Install macOS software"
         if [[ $RUNNER_OS != "macOS" ]]; then exit 0; fi
         brew update --quiet
         brew install \
@@ -49,31 +54,39 @@ runs:
           cln \
           gmp \
           pkgconfig \
-          flex
+          flex \
+          gnu-sed
         python3 -m pip install pexpect setuptools toml
         # Make ImageVersion accessible as env.image_version. Environment
         # variables of the runner are not automatically imported:
         #
         # https://github.com/actions/runner/blob/master/docs/adrs/0278-env-context.md#dont-populate-the-env-context-with-environment-variables-from-runner-machine
+        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 "/usr/local/opt/ccache/libexec" >> $GITHUB_PATH
+        echo "::endgroup::"
 
-    - name: Install Python packages
+    - name: Install software for Python bindings
       shell: bash
       run: |
+        echo "::group::Install software for Python bindings"
         if [[ "${{ inputs.with-python-bindings }}" != "true" ]]; then exit 0; fi
         python3 -m pip install pytest scikit-build
         python3 -m pytest --version
         python3 -m pip install \
           Cython==0.29.* --install-option="--no-cython-compile"
         echo "$(python3 -m site --user-base)/bin" >> $GITHUB_PATH
+        echo "::endgroup::"
     
     - name: Install software for documentation
       shell: bash
       run: |
+        echo "::group::Install software for documentation"
         if [[ "${{ inputs.with-documentation }}" != "true" ]]; then exit 0; fi
         sudo apt-get install -y doxygen python3-docutils python3-jinja2
         python3 -m pip install \
           sphinxcontrib-bibtex sphinx-tabs sphinx-rtd-theme breathe \
           sphinxcontrib-programoutput
+        echo "::endgroup::"
diff --git a/.github/actions/run-tests/action.yml b/.github/actions/run-tests/action.yml
index 2b2326699..bc3936d47 100644
--- a/.github/actions/run-tests/action.yml
+++ b/.github/actions/run-tests/action.yml
@@ -1,6 +1,8 @@
 name: Run tests
 description: Run all available tests
 inputs:
+  build-dir:
+    default: build/
   check-examples:
     default: true
   check-python-bindings:
@@ -22,14 +24,14 @@ runs:
         ARGS: --output-on-failure -LE regress[${{ inputs.regressions-exclude }}]
         CVC5_REGRESSION_ARGS: --no-early-exit
         RUN_REGRESSION_ARGS: ${{ inputs.regressions-args }}
-      working-directory: build
+      working-directory: ${{ inputs.build-dir }}
 
     - name: Run Unit Tests
       shell: bash
       run: |
         if [[ "${{ inputs.check-unit-tests }}" != "true" ]]; then exit 0; fi
         make -j${{ env.num_proc }} apitests units
-      working-directory: build
+      working-directory: ${{ inputs.build-dir }}
 
     - name: Install Check
       shell: bash
@@ -37,13 +39,13 @@ runs:
         make -j${{ env.num_proc }} install
         echo -e "#include <cvc5/cvc5.h>\nint main() { cvc5::api::Solver s; return 0; }" > /tmp/test.cpp
         g++ -std=c++17 /tmp/test.cpp -I install/include -L install/lib -lcvc5
-      working-directory: build
+      working-directory: ${{ inputs.build-dir }}
 
     - name: Python Install Check
       shell: bash
       run: |
         if [[ "${{ inputs.check-python-bindings }}" != "true" ]]; then exit 0; fi
-        export PYTHONPATH="$PYTHONPATH:$(dirname $(find build/install/ -name "pycvc5" -type d))"
+        export PYTHONPATH="$PYTHONPATH:$(dirname $(find ${{ inputs.build-dir }}/install/ -name "pycvc5" -type d))"
         python3 -c "import pycvc5"
 
     - name: Check Examples
@@ -52,7 +54,7 @@ runs:
         if [[ "${{ inputs.check-examples }}" != "true" ]]; then exit 0; fi
         mkdir build
         cd build
-        cmake .. -DCMAKE_PREFIX_PATH=$(pwd)/../../build/install/lib/cmake
+        cmake .. -DCMAKE_PREFIX_PATH=${{ inputs.build-dir }}/install/lib/cmake
         make -j${{ env.num_proc }}
         ctest -j${{ env.num_proc }} --output-on-failure
-      working-directory: examples
\ No newline at end of file
+      working-directory: examples
diff --git a/.github/actions/setup-cache/action.yml b/.github/actions/setup-cache/action.yml
index ad485f2dc..5a20ebcdc 100644
--- a/.github/actions/setup-cache/action.yml
+++ b/.github/actions/setup-cache/action.yml
@@ -64,6 +64,8 @@ runs:
     - name: Setup dependencies cache
       uses: actions/cache@v2
       with:
-        path: build/deps
+        path: |
+          build-shared/deps
+          build-static/deps
         key: ${{ inputs.cache-key }}-${{ runner.os }}-deps-${{ hashFiles('cmake/**') }}-${{ hashFiles('.github/**') }}
 
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 89c108b93..82916f26b 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -70,15 +70,12 @@ jobs:
       with:
         cache-key: ${{ matrix.cache-key }}
 
-    - name: Configure
-      run: |
-        ${{ matrix.env }} ./configure.sh ${{ matrix.config }} \
-          --prefix=$(pwd)/build/install \
-          --werror
-
-    - name: Build
-      run: make -j${{ env.num_proc }}
-      working-directory: build
+    - name: Configure and build
+      id: configure-and-build
+      uses: ./.github/actions/configure-and-build
+      with:
+        configure-env: ${{ matrix.env }}
+        configure-config: ${{ matrix.config }}
 
     - name: ccache Statistics
       run: ccache -s
@@ -86,6 +83,7 @@ jobs:
     - name: Run tests
       uses: ./.github/actions/run-tests
       with:
+        build-dir: ${{ steps.configure-and-build.outputs.shared-build-dir }}
         check-examples: ${{ matrix.check-examples }}
         check-python-bindings: ${{ matrix.python-bindings }}
         check-unit-tests: ${{ matrix.check-units }}
@@ -95,9 +93,12 @@ jobs:
     - name: Build documentation
       if: matrix.build-documentation
       uses: ./.github/actions/build-documentation
+      with:
+        build-dir: ${{ steps.configure-and-build.outputs.shared-build-dir }}
 
     - name: Add binary to release
       if: matrix.store-to-release && startsWith(github.ref, 'refs/tags/')
       uses: ./.github/actions/add-to-release
       with:
+        binary: ${{ steps.configure-and-build.outputs.static-build-dir }}/bin/cvc5
         github-token: ${{ secrets.GITHUB_TOKEN }}