Fix issues with Ninja build system and add configure option. (#3166)

Adds option --ninja to configure.sh.

diff --git a/CMakeLists.txt b/CMakeLists.txt
index d9cdf34818c3ac6034dc7bc2ce5d5577b7d22b00..0748c807528c1eda0fc2b1ff661a6108be611ff7 100644 (file)
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -1,4 +1,4 @@
-cmake_minimum_required(VERSION 3.1)
+cmake_minimum_required(VERSION 3.2)
 
 #-----------------------------------------------------------------------------#
 # Project configuration
@@ -306,7 +306,7 @@ if(ENABLE_COVERAGE)
     NAME coverage
     EXECUTABLE
       ctest -j${CTEST_NTHREADS} -LE "example"
-        --output-on-failure $(ARGS) || exit 0
+        --output-on-failure $$ARGS || exit 0
     DEPENDS
       build-tests)
 endif()

diff --git a/configure.sh b/configure.sh
index 9bf33ae8a44ed2b0c42d5d35793a778a65bf67f2..d7e807c65a936854611245c01a05d22b31dcd468 100755 (executable)
--- a/configure.sh
+++ b/configure.sh
@@ -20,6 +20,7 @@ General options;
   --best                   turn on dependencies known to give best performance
   --gpl                    permit GPL dependencies, if available
   --win64                  cross-compile for Windows 64 bit
+  --ninja                  use Ninja build system
 
 
 Features:
@@ -117,6 +118,7 @@ drat2er=default
 dumping=default
 gpl=default
 win64=default
+ninja=default
 glpk=default
 lfsc=default
 muzzle=default
@@ -217,6 +219,8 @@ do
     --win64) win64=ON;;
     --no-win64) win64=OFF;;
 
+    --ninja) ninja=ON;;
+
     --glpk) glpk=ON;;
     --no-glpk) glpk=OFF;;
 
@@ -357,6 +361,7 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DENABLE_GPL=$gpl"
 [ $win64 != default ] \
   && cmake_opts="$cmake_opts -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-mingw64.cmake"
+[ $ninja != default ] && cmake_opts="$cmake_opts -G Ninja"
 [ $muzzle != default ] \
   && cmake_opts="$cmake_opts -DENABLE_MUZZLE=$muzzle"
 [ $optimized != default ] \

diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
index 8cf2208ea8fa9bbe67a9557da61e3f12e6d3b774..f81c68236cfa21c17d5750f61f45e4b956175d85 100644 (file)
--- a/examples/CMakeLists.txt
+++ b/examples/CMakeLists.txt
@@ -18,7 +18,7 @@ add_custom_target(examples)
 # Create target runexamples.
 # Builds and runs all examples.
 add_custom_target(runexamples
-  COMMAND ctest --output-on-failure -L "example" -j${NTHREADS} $(ARGS)
+  COMMAND ctest --output-on-failure -L "example" -j${NTHREADS} $$ARGS
   DEPENDS examples)
 
 # Add example target and create test to run example with ctest.

diff --git a/src/base/CMakeLists.txt b/src/base/CMakeLists.txt
index db8eb8c3657a8113a94a6c0a16a0fddc6bf2be6f..8df40a6ff929dbaba1a8b484ec9415b02e06d157 100644 (file)
--- a/src/base/CMakeLists.txt
+++ b/src/base/CMakeLists.txt
@@ -50,6 +50,7 @@ add_custom_target(
   COMMAND
     ${gentmptags_script} ${CMAKE_CURRENT_LIST_DIR} Debug ${source_files_list}
   DEPENDS mktags
+  BYPRODUCTS ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags.tmp
 )
 
 add_custom_target(
@@ -57,6 +58,7 @@ add_custom_target(
   COMMAND
     ${gentmptags_script} ${CMAKE_CURRENT_LIST_DIR} Trace ${source_files_list}
   DEPENDS mktags
+  BYPRODUCTS ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags.tmp
 )
 
 add_custom_command(

diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
index 1970bb659eee4ff86867a912463a9de8e08e95dd..cd67c136e9d4f385ee9131c0565f6ee4e2aa970c 100644 (file)
--- a/test/CMakeLists.txt
+++ b/test/CMakeLists.txt
@@ -17,7 +17,7 @@ add_dependencies(build-tests examples)
 # Dependencies of check are added in the corresponding subdirectories.
 add_custom_target(check
   COMMAND
-    ctest --output-on-failure -LE "regress[3-4]" -j${CTEST_NTHREADS} $(ARGS)
+    ctest --output-on-failure -LE "regress[3-4]" -j${CTEST_NTHREADS} $$ARGS
   DEPENDS
     build-tests)
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 37e6e341409eac65b7f3383f8d81d55f2cf609b8..f3c80559acec6a09cec4a91aabbbdca3245f96ff 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2203,7 +2203,7 @@ add_dependencies(build-tests build-regress)
 
 add_custom_target(regress
   COMMAND
-    ctest --output-on-failure -L "regress[0-2]" -j${CTEST_NTHREADS} $(ARGS)
+    ctest --output-on-failure -L "regress[0-2]" -j${CTEST_NTHREADS} $$ARGS
   DEPENDS build-regress)
 
 macro(cvc4_add_regression_test level file)

diff --git a/test/system/CMakeLists.txt b/test/system/CMakeLists.txt
index 9d0d8424a7c1313fc402c9a30a9babc8cb41fa83..420ce8e6f02ee61ef211043a799f1b26871d7316 100644 (file)
--- a/test/system/CMakeLists.txt
+++ b/test/system/CMakeLists.txt
@@ -11,7 +11,7 @@ add_custom_target(build-systemtests)
 add_dependencies(build-tests build-systemtests)
 
 add_custom_target(systemtests
-  COMMAND ctest --output-on-failure -L "system" -j${CTEST_NTHREADS} $(ARGS)
+  COMMAND ctest --output-on-failure -L "system" -j${CTEST_NTHREADS} $$ARGS
   DEPENDS build-systemtests)
 
 set(CVC4_SYSTEM_TEST_FLAGS

diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index 09eff7175ead8d72d42a1895e714fa116337f535..83b0ec0dbfe00983c1f5f930b691e4e3d233001d 100644 (file)
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -17,7 +17,7 @@ add_custom_target(build-units)
 add_dependencies(build-tests build-units)
 
 add_custom_target(units
-  COMMAND ctest --output-on-failure -L "unit" -j${CTEST_NTHREADS} $(ARGS)
+  COMMAND ctest --output-on-failure -L "unit" -j${CTEST_NTHREADS} $$ARGS
   DEPENDS build-units)
 
 set(CVC4_CXXTEST_FLAGS_BLACK