Fix public headers for make install. (#2856)

This commit fixes make install, which previously copied all public header files to ${CMAKE_INSTALL_PREFIX}/ instead of ${CMAKE_INSTALL_PREFIX}/cvc4.
Further, the old build system modified all #include directives in the installed public header files to use the installed headers, e.g., #include "cvc4_public.h" was changed to #include <cvc4/cvc4_public.h>. Now, after make install the script src/fix-install-headers.sh is executed to change the #include directives accordingly (this should be obsolete with the new C++ API).

diff --git a/.travis.yml b/.travis.yml
index 265f42bb49a8ee066362cc73f8ca47107c04fa5d..61a40a9f6246c92782b91264d4c9bac72da97bd5 100644 (file)
--- a/.travis.yml
+++ b/.travis.yml
@@ -56,7 +56,7 @@ script:
    normal="$(echo -e '\033[0m')" red="$normal$(echo -e '\033[01;31m')" green="$normal$(echo -e '\033[01;32m')"
    configureCVC4() {
      echo "CVC4 config - $TRAVIS_CVC4_CONFIG";
-     ./configure.sh --name=build --unit-testing $TRAVIS_CVC4_CONFIG
+     ./configure.sh --name=build --prefix=$(pwd)/build/install --unit-testing $TRAVIS_CVC4_CONFIG
    }
    error() {
      echo;
@@ -69,6 +69,12 @@ script:
      make -j2 check ARGS='-LE regress[1-4]' CVC4_REGRESSION_ARGS='--no-early-exit' || error "BUILD/UNIT/SYSTEM/REGRESSION TEST FAILED"
      ctest -j2 -L example || error "RUNNING EXAMPLES FAILED"
    }
+   makeInstallCheck() {
+     cd build
+     make install -j2
+     echo -e "#include <cvc4/cvc4.h>\nint main() { CVC4::ExprManager em; return 0; }" > /tmp/test.cpp
+     $CXX -std=c++11 /tmp/test.cpp -I install/include -L install/lib -lcvc4 -lcln || exit 1
+   }
    run() {
      echo "travis_fold:start:$1"
      echo "Running $1"
@@ -77,7 +83,7 @@ script:
    }
    [ -n "$TRAVIS_CVC4" ] && [ -n "$TRAVIS_WITH_LFSC" ] && run contrib/get-lfsc-checker
    [ -n "$TRAVIS_CVC4" ] && run configureCVC4
-   [ -n "$TRAVIS_CVC4" ] && run makeCheck
+   [ -n "$TRAVIS_CVC4" ] && run makeCheck && run makeInstallCheck
    [ -z "$TRAVIS_CVC4" ] && error "Unknown Travis-CI configuration"
    echo "travis_fold:end:load_script"
  - echo; echo "${green}EVERYTHING SEEMED TO PASS!${normal}"

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index e142ff46c7be2af36e4d0a4124c16ef66bb4c326..388e3c4fb8d6e54aa3db53b34186b3ec7ad59368 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -791,27 +791,27 @@ install(FILES
           api/cvc4cpp.h
           api/cvc4cppkind.h
         DESTINATION
-          include/api)
+          include/cvc4/api)
 install(FILES
           base/configuration.h
           base/exception.h
           base/listener.h
           base/modal_exception.h
         DESTINATION
-          include/base)
+          include/cvc4/base)
 install(FILES
           context/cdhashmap_forward.h
           context/cdhashset_forward.h
           context/cdinsert_hashmap_forward.h
           context/cdlist_forward.h
         DESTINATION
-          include/context)
+          include/cvc4/context)
 install(FILES
           include/cvc4.h
           include/cvc4_public.h
           include/cvc4parser_public.h
         DESTINATION
-          include)
+          include/cvc4)
 install(FILES
           expr/array.h
           expr/array_store_all.h
@@ -831,7 +831,7 @@ install(FILES
           ${CMAKE_CURRENT_BINARY_DIR}/expr/kind.h
           ${CMAKE_CURRENT_BINARY_DIR}/expr/expr_manager.h
         DESTINATION
-          include/expr)
+          include/cvc4/expr)
 install(FILES
           options/argument_extender.h
           options/arith_heuristic_pivot_rule.h
@@ -848,38 +848,38 @@ install(FILES
           options/sygus_out_mode.h
           options/theoryof_mode.h
         DESTINATION
-          include/options)
+          include/cvc4/options)
 install(FILES
           parser/input.h
           parser/parser.h
           parser/parser_builder.h
           parser/parser_exception.h
         DESTINATION
-          include/parser)
+          include/cvc4/parser)
 install(FILES
           printer/sygus_print_callback.h
         DESTINATION
-          include/printer)
+          include/cvc4/printer)
 install(FILES
           proof/unsat_core.h
         DESTINATION
-          include/proof)
+          include/cvc4/proof)
 install(FILES
           smt/command.h
           smt/logic_exception.h
           smt/smt_engine.h
         DESTINATION
-          include/smt)
+          include/cvc4/smt)
 install(FILES
           smt_util/lemma_channels.h
           smt_util/lemma_input_channel.h
           smt_util/lemma_output_channel.h
         DESTINATION
-          include/smt_util)
+          include/cvc4/smt_util)
 install(FILES
           theory/logic_info.h
         DESTINATION
-          include/theory)
+          include/cvc4/theory)
 install(FILES
           util/abstract_value.h
           util/bitvector.h
@@ -906,4 +906,10 @@ install(FILES
           ${CMAKE_CURRENT_BINARY_DIR}/util/integer.h
           ${CMAKE_CURRENT_BINARY_DIR}/util/rational.h
         DESTINATION
-          include/util)
+          include/cvc4/util)
+
+# Fix include paths for all public headers.
+# Note: This is a temporary fix until the new C++ API is in place.
+install(CODE "execute_process(COMMAND
+                ${CMAKE_CURRENT_LIST_DIR}/fix-install-headers.sh
+                ${CMAKE_INSTALL_PREFIX})")

diff --git a/src/fix-install-headers.sh b/src/fix-install-headers.sh
new file mode 100755 (executable)
index 0000000..a1f1599
--- /dev/null
+++ b/src/fix-install-headers.sh
@@ -0,0 +1,5 @@
+#!/bin/bash
+
+dir=$1
+find "$dir/include/cvc4/" -type f | \
+  xargs sed -i 's/include.*"\(.*\)"/include <cvc4\/\1>/'