From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 9 Nov 2021 20:21:08 +0000 (-0800)
Subject: Clean up ctest configuration and CI test configuration. (#7620)
X-Git-Tag: cvc5-1.0.0~846
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a71f9a9dfdc512274635d80be9e3662ed745b14c;p=cvc5.git

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 5fddcbd36..47c4ed933 100644
--- 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 f8faab276..f28309652 100644
--- 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 24158e00b..11c2e8514 100644
--- 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)