From 0a41a21cedc789262f3035aa91ff6b924f309b4e Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Fri, 14 Sep 2018 14:21:35 -0700
Subject: [PATCH] cmake: Do not build examples and unit and system tests by
 default.

---
 CMakeLists.txt             |  2 +-
 test/CMakeLists.txt        | 10 +++++++---
 test/system/CMakeLists.txt |  3 ++-
 test/unit/CMakeLists.txt   |  6 ++++++
 4 files changed, 16 insertions(+), 5 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 862fc2ae5..23a52db59 100644
--- 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 2e062bd85..64fa378ff 100644
--- 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 01b4a384d..2ca33d1e9 100644
--- 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 0123ae7ff..5e45654a9 100644
--- 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)
-- 
2.30.2