fix bug #264: competition / other static library builds when readline isn't available

diff --git a/config/readline.m4 b/config/readline.m4
index 70f36bc79dec26000d8a4cc4606666df40c0f163..ce1d1deda4eb46700f645e6719a8281b9fb32b3c 100644 (file)
--- a/config/readline.m4
+++ b/config/readline.m4
@@ -15,12 +15,47 @@ else
   fi
   AC_CHECK_LIB([readline], [readline],
                [AC_CHECK_HEADER([readline/readline.h],
-                  AC_SUBST([READLINE_LDFLAGS], ["-lreadline -lncurses"])
-                  AC_DEFINE([HAVE_LIBREADLINE], [1], [Define to 1 to use libreadline]))],
+                  [READLINE_LIBS="-lreadline -lncurses"],
+                  [if test "$with_readline" != check; then
+                     AC_MSG_FAILURE([cannot find libreadline!])
+                   fi])],
                [if test "$with_readline" != check; then
                   AC_MSG_FAILURE([cannot find libreadline!])
                 fi], -lncurses)
-  if test -z "$READLINE_LDFLAGS"; then with_readline=no; else with_readline=yes; fi
+  if test -z "$READLINE_LIBS"; then
+    with_readline=no
+  else
+    # make sure it works in static builds, too
+    if test "$enable_static_binary" = yes; then
+      AC_MSG_CHECKING([whether statically-linked readline is functional])
+      AC_LANG_PUSH([C++])
+      cvc4_save_LIBS="$LIBS"
+      cvc4_save_LDFLAGS="$LDFLAGS"
+      LDFLAGS="-static $LDFLAGS"
+      LIBS="$READLINE_LIBS $LIBS"
+      AC_LINK_IFELSE(AC_LANG_PROGRAM([#include <readline/readline.h>],
+                                     [readline("")]),
+        [ AC_MSG_RESULT([yes, it works])
+          with_readline=yes ],
+        [ AC_MSG_RESULT([no])
+          if test "$with_readline" != check; then
+            AC_MSG_FAILURE([readline installation incompatible with static-binary])
+          fi
+          with_readline=no ])
+      LIBS="$cvc4_save_LIBS"
+      LDFLAGS="$cvc4_save_LDFLAGS"
+      AC_LANG_POP([C++])
+    else
+      with_readline=yes
+    fi
+  fi
+  if test "$with_readline" = yes; then
+    HAVE_LIBREADLINE=1
+  else
+    HAVE_LIBREADLINE=0
+  fi
+  AC_DEFINE_UNQUOTED([HAVE_LIBREADLINE], ${HAVE_LIBREADLINE}, [Define to 1 to use libreadline])
+  AC_SUBST([READLINE_LIBS])
 fi
 ])# CVC4_CHECK_FOR_READLINE
 

diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index d53ae55a09f8458bfdf5252b0dc177bd2efab3a4..da3b5896ab2d3c65cf67c85f3ace9747c76d4497 100644 (file)
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -20,7 +20,7 @@ cvc4_LDADD = \
        @builddir@/../parser/libcvc4parser.la \
        @builddir@/../libcvc4.la \
        @builddir@/../lib/libreplacements.la \
-       $(READLINE_LDFLAGS)
+       $(READLINE_LIBS)
 
 BUILT_SOURCES = \
        $(TOKENS_FILES)