Clean up ctest configuration and CI test configuration. (#7620)

Previously, on CI, unit tests and api tests were run twice since we use
a ctest exclude rule based on labels (-LE) which includes unit and api
tests, but then run them separately again. This cleans up the CI test
configuration.

Further, unit gtest unit tests were added with gtest_add_tests, which
adds every test of a unit test binary as a single test target to ctest.
In theory, this may speed up testing (because more parallelism) but in
practice it slows it down due to the start up overhead. It also clutters
CI output. This cleans up the gtest configuration to add the gtest unit
tests per test binary rather then per test of a test binary.

diff --git a/.github/actions/run-tests/action.yml b/.github/actions/run-tests/action.yml
index 5fddcbd365a97a2ee746aa361536fe5980e5a0cb..47c4ed9330b0d6377d3e15e2cbb8a20405473193 100644 (file)
--- a/.github/actions/run-tests/action.yml
+++ b/.github/actions/run-tests/action.yml
@@ -9,8 +9,6 @@ inputs:
     default: true
   check-python-bindings:
     default: false
-  check-unit-tests:
-    default: true
   regressions-args:
     default: ""
   regressions-exclude:
@@ -28,13 +26,6 @@ runs:
         RUN_REGRESSION_ARGS: ${{ inputs.regressions-args }}
       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: ${{ inputs.build-dir }}
-
     - name: Install Check
       shell: bash
       run: |

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index f8faab276ca0d732a1eea555ad4520b02535cd91..f2830965224fe0a8c83c6a1ffe6561abb74db7d6 100644 (file)
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -40,7 +40,6 @@ jobs:
             os: ubuntu-18.04
             config: production --auto-download --assertions --tracing --unit-testing --java-bindings --editline
             cache-key: dbg
-            check-units: true
             exclude_regress: 3-4
             run_regression_args: --tester base --tester model --tester synth --tester abduct --tester proof
 
@@ -86,7 +85,6 @@ jobs:
         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 }}
         regressions-args: ${{ matrix.run_regression_args }}
         regressions-exclude: ${{ matrix.exclude_regress }}
   
@@ -97,7 +95,6 @@ jobs:
         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
 

diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index 24158e00b0ce8bb8e6fb82d294d36e016cd1f6a3..11c2e8514d8bcc10c827aa22e990beea4e4c67fe 100644 (file)
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -14,7 +14,6 @@
 ##
 
 find_package(GTest REQUIRED)
-include(GoogleTest)
 
 include_directories(.)
 include_directories(${PROJECT_SOURCE_DIR}/src)
@@ -40,7 +39,6 @@ macro(cvc5_add_unit_test is_white name output_dir)
   set(test_src ${CMAKE_CURRENT_LIST_DIR}/${name}.cpp)
   add_executable(${name} ${test_src})
   target_compile_definitions(${name} PRIVATE ${CVC5_UNIT_TEST_FLAGS_BLACK})
-  gtest_add_tests(TARGET ${name})
   target_link_libraries(${name} PUBLIC main-test GMP)
   target_link_libraries(${name} PUBLIC GTest::Main)
   target_link_libraries(${name} PUBLIC GTest::GTest)