From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 19 Oct 2011 21:35:50 +0000 (+0000)
Subject: fix bug #264: competition / other static library builds when readline isn't available
X-Git-Tag: cvc5-1.0.0~8414
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=255d7e4140d5fee6edfe5c7233c8870f889b2a32;p=cvc5.git

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

diff --git a/config/readline.m4 b/config/readline.m4
index 70f36bc79..ce1d1deda 100644
--- 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 d53ae55a0..da3b5896a 100644
--- 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)