* Clean up some options documentation

* Remove defunct --no-theory-registration option
* Point people to Wiki tutorial
* Modernize the cut-release script
* Misc cleanup, documentation

(this commit was certified error- and warning-free by the test-and-commit script.)

1 files changed, 44 insertions, 17 deletions

diff --git a/config/readline.m4 b/config/readline.m4
index 30d285b29..90785c7a0 100644
--- a/config/readline.m4
+++ b/config/readline.m4
@@ -14,11 +14,16 @@ else
   else
     AC_MSG_RESULT([yes, readline enabled by user])
   fi
+  dnl Try a bunch of combinations until something works :-/
   READLINE_LIBS=
   CVC4_TRY_READLINE_WITH([])
   CVC4_TRY_READLINE_WITH([-ltinfo])
+  CVC4_TRY_READLINE_WITH([-ltermcap])
+  CVC4_TRY_READLINE_WITH([-ltermcap -ltinfo])
   CVC4_TRY_READLINE_WITH([-lncurses -ltermcap])
   CVC4_TRY_READLINE_WITH([-lncurses -ltermcap -ltinfo])
+  CVC4_TRY_READLINE_WITH([-lcurses -ltermcap])
+  CVC4_TRY_READLINE_WITH([-lcurses -ltermcap -ltinfo])
   if test -z "$READLINE_LIBS"; then
     if test "$with_readline" != check; then
       AC_MSG_FAILURE([cannot find libreadline! (or can't get it to work)])
@@ -27,24 +32,26 @@ else
   else
     # make sure it works in static builds, too
     if test "$enable_static_binary" = yes; then
+      READLINE_LIBS=
       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++])
+      CVC4_TRY_STATIC_READLINE_WITH([])
+      CVC4_TRY_STATIC_READLINE_WITH([-ltinfo])
+      CVC4_TRY_STATIC_READLINE_WITH([-ltermcap])
+      CVC4_TRY_STATIC_READLINE_WITH([-ltermcap -ltinfo])
+      CVC4_TRY_STATIC_READLINE_WITH([-lncurses -ltermcap])
+      CVC4_TRY_STATIC_READLINE_WITH([-lncurses -ltermcap -ltinfo])
+      CVC4_TRY_STATIC_READLINE_WITH([-lcurses -ltermcap])
+      CVC4_TRY_STATIC_READLINE_WITH([-lcurses -ltermcap -ltinfo])
+      if test -n "$READLINE_LIBS"; then
+        AC_MSG_RESULT([yes, it works])
+        with_readline=yes
+      else
+        AC_MSG_RESULT([no])
+        if test "$with_readline" != check; then
+          AC_MSG_FAILURE([readline installation appears incompatible with static-binary])
+        fi
+        with_readline=no
+      fi
     else
       with_readline=yes
     fi
@@ -70,3 +77,23 @@ if test -z "$READLINE_LIBS"; then
                [], [$1])
 fi
 ])# CVC4_TRY_READLINE_WITH
+
+# CVC4_TRY_STATIC_READLINE_WITH(LIBS)
+# -----------------------------------
+# Try AC_CHECK_LIB(readline) with the given linking libraries
+AC_DEFUN([CVC4_TRY_STATIC_READLINE_WITH], [
+if test -z "$READLINE_LIBS"; then
+  AC_LANG_PUSH([C++])
+  cvc4_save_LIBS="$LIBS"
+  cvc4_save_LDFLAGS="$LDFLAGS"
+  LDFLAGS="-static $LDFLAGS"
+  LIBS="-lreadline $1"
+  AC_LINK_IFELSE([AC_LANG_PROGRAM([#include <readline/readline.h>],
+                                  [readline("")])],
+    [READLINE_LIBS="-lreadline $1"],
+    [])
+  LIBS="$cvc4_save_LIBS"
+  LDFLAGS="$cvc4_save_LDFLAGS"
+  AC_LANG_POP([C++])
+fi
+])# CVC4_TRY_STATIC_READLINE_WITH