cmake: Do not build examples and unit and system tests by default.

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 862fc2ae5d9b57ff54d40b81024569072ed5da94..23a52db59e6cae13e9117142f4f00ed28327ae98 100644 (file)
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -433,7 +433,7 @@ if(ENABLE_PROOFS)
 endif()
 
 add_subdirectory(doc)
-add_subdirectory(examples)
+add_subdirectory(examples EXCLUDE_FROM_ALL)
 add_subdirectory(src)
 add_subdirectory(test)
 

diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
index 2e062bd852ac891fd5223440d1b0fd85c375f8b4..64fa378ff99eeb9447aee274283d615f0432576c 100644 (file)
--- a/test/CMakeLists.txt
+++ b/test/CMakeLists.txt
@@ -10,14 +10,14 @@ endif()
 # Add subdirectories
 
 add_subdirectory(regress)
-add_subdirectory(system)
+add_subdirectory(system EXCLUDE_FROM_ALL)
 
 if(BUILD_BINDINGS_JAVA)
   add_subdirectory(java)
 endif()
 
 if(ENABLE_UNIT_TESTING)
-       add_subdirectory(unit)
+  add_subdirectory(unit EXCLUDE_FROM_ALL)
 endif()
 
 #-----------------------------------------------------------------------------#
@@ -27,4 +27,8 @@ endif()
 # > system tests
 
 add_custom_target(check
-  COMMAND ctest --output-on-failure -LE "regress[2-4]" -j${NTHREADS} $(ARGS))
+  COMMAND ctest --output-on-failure -LE "regress[2-4]" -j${NTHREADS} $(ARGS)
+  DEPENDS units regress systemtests)
+if(BUILD_BINDINGS_JAVA)
+  add_dependencies(check cvc4javatests)
+endif()

diff --git a/test/system/CMakeLists.txt b/test/system/CMakeLists.txt
index 01b4a384dc2f526a4a87877b22374ea32bb83c24..2ca33d1e99d3adc9fb8e46b10c2e8da6f96802a2 100644 (file)
--- a/test/system/CMakeLists.txt
+++ b/test/system/CMakeLists.txt
@@ -8,7 +8,8 @@ include_directories(${CMAKE_BINARY_DIR}/src)
 # > system tests
 
 add_custom_target(systemtests
-  COMMAND ctest --output-on-failure -L "system" -j${NTHREADS} $(ARGS))
+  COMMAND ctest --output-on-failure -L "system" -j${NTHREADS} $(ARGS)
+  DEPENDS cvc4)
 
 set(CVC4_SYSTEM_TEST_FLAGS
   -D__BUILDING_CVC4_SYSTEM_TEST -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS)

diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index 0123ae7ff9ffa555eed9bbac0071750009a3cf3b..5e45654a911e4892368d84446a4641c152f6b64e 100644 (file)
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -16,6 +16,12 @@ set(CVC4_CXXTEST_FLAGS_BLACK
 set(CVC4_CXXTEST_FLAGS_WHITE -fno-access-control ${CVC4_CXXTEST_FLAGS_BLACK})
 
 macro(cvc4_add_unit_test is_white name)
+  # cxxtest_add_test generates the unit test executables into directory
+  # CMAKE_BINARY_DIR/test/unit by default and does not allow to change this
+  # location (it's possible to set corresponding target properties with
+  # set_target_properties, but then the test environment does not find them).
+  # Hence, these are the only executables that are not generated into our
+  # default directory for executables (CMAKE_BINARY_DIR/bin).
   cxxtest_add_test(${name} ${name}.cpp ${CMAKE_CURRENT_LIST_DIR}/${name}.h)
   set_tests_properties(${name} PROPERTIES LABELS "unit")
   target_link_libraries(${name} main-test)