Refactor cmake to build either static or shared (#7534)

This PR simplifies the cmake setup to only build either shared or statically. It also attempts to fix windows builds, both shared and static.

3 files changed, 19 insertions, 6 deletions

diff --git a/.github/actions/configure-and-build/action.yml b/.github/actions/configure-and-build/action.yml
index 4e2bea7a1..ace887be1 100644
--- a/.github/actions/configure-and-build/action.yml
+++ b/.github/actions/configure-and-build/action.yml
@@ -44,7 +44,7 @@ runs:
         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
+          --prefix=$(pwd)/build-static/install --werror --static --name=build-static --no-java-bindings
 
         cd build-static/ && pwd=$(pwd)
         $SED -i.orig -n -e '/^base_dir = /!p' -e "\$abase_dir = $pwd" $CCACHE_CONFIGPATH
diff --git a/.github/actions/run-tests/action.yml b/.github/actions/run-tests/action.yml
index bc3936d47..ba4502b95 100644
--- a/.github/actions/run-tests/action.yml
+++ b/.github/actions/run-tests/action.yml
@@ -5,12 +5,14 @@ inputs:
     default: build/
   check-examples:
     default: true
+  check-install:
+    default: true
   check-python-bindings:
     default: false
   check-unit-tests:
     default: true
   regressions-args:
-    default: "--no-check-unsat-cores --no-check-proofs"
+    default: ""
   regressions-exclude:
     default: "3-4"
 runs:
@@ -36,6 +38,7 @@ runs:
     - name: Install Check
       shell: bash
       run: |
+        if [[ "${{ inputs.check-install }}" != "true" ]]; then exit 0; fi
         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
@@ -52,8 +55,7 @@ runs:
       shell: bash
       run: |
         if [[ "${{ inputs.check-examples }}" != "true" ]]; then exit 0; fi
-        mkdir build
-        cd build
+        mkdir -p build && cd build
         cmake .. -DCMAKE_PREFIX_PATH=${{ inputs.build-dir }}/install/lib/cmake
         make -j${{ env.num_proc }}
         ctest -j${{ env.num_proc }} --output-on-failure
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index fedcb9bb4..f8faab276 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -8,7 +8,7 @@ jobs:
         include:
           - name: ubuntu:production
             os: ubuntu-latest
-            config: production --auto-download --all-bindings --editline --docs --static
+            config: production --auto-download --all-bindings --editline --docs
             cache-key: production
             python-bindings: true
             build-documentation: true
@@ -19,7 +19,7 @@ jobs:
 
           - name: macos:production
             os: macos-11
-            config: production --auto-download --all-bindings --editline --static
+            config: production --auto-download --all-bindings --editline
             cache-key: production
             python-bindings: true
             check-examples: true
@@ -89,6 +89,17 @@ jobs:
         check-unit-tests: ${{ matrix.check-units }}
         regressions-args: ${{ matrix.run_regression_args }}
         regressions-exclude: ${{ matrix.exclude_regress }}
+  
+    - name: Run tests
+      uses: ./.github/actions/run-tests
+      with:
+        build-dir: ${{ steps.configure-and-build.outputs.static-build-dir }}
+        check-examples: false
+        check-install: false
+        check-python-bindings: false
+        check-unit-tests: ${{ matrix.check-units }}
+        regressions-args: ${{ matrix.run_regression_args }}
+        regressions-exclude: 1-4
 
     - name: Build documentation
       if: matrix.build-documentation