libyices: with --enable-static and --with-pic, enforce PIC libgmp.a

One problem I came across was that most of the time, when I was doing

    ./configure --enable-static --with-pic

the produced libyices.a would still contain non-PIC libgmp.a, although
being itself PIC. In this commit, I enforce that if --with-pic is given,
then:

1) either --with-pic-gmp has been given, in this case we use that for
   creating the PIC libyices.a;
2) or --with-pic-gmp has not been given and thus we try to simply use the
   shared gmp through -lgmp.

Reminder: we also check that the system libgmp.a or the libgmp.a given with
--with-static-gmp is PIC. If it is the case, the PIC libgmp.a will be used
for --with-pic.

ext/yices/configure

@@ -14069,7 +14069,7 @@ $SHELL libtool --mode=clean $RM -f conftest.* lib.la 2>&5 >&5
 
     # If shared library is enabled and --with-pic-gmp is given, test that
     # it is in fact PIC.
-    if test $enable_shared = yes -a "x$pic_libgmp" != x; then
+    if test "x$pic_libgmp" != x; then
 
 testincludedir=""
 for incldir in $pic_includegmp "$(dirname $pic_libgmp)" "$(dirname $pic_libgmp)/../include"; do
@@ -14246,6 +14246,14 @@ $SHELL libtool --mode=clean $RM -f conftest.* lib.la 2>&5 >&5
       fi
       PIC_GMP=$testlib
       PIC_GMP_INCLUDE_DIR=$testincludedir
+      # If the PIC mode is enabled, we want the produced libyices.a to be
+      # built against a PIC version of libgmp.a.
+      if test $pic_mode = yes; then
+        STATIC_GMP=$PIC_GMP
+        STATIC_GMP_INCLUDE_DIR=$PIC_GMP_INCLUDE_DIR
+        STATIC_GMP_HAS_PIC=yes
+        PIC_GMP_HAS_PIC=yes
+      fi
     fi
     ;;
   mingw* | cygwin*)
@@ -15531,13 +15539,44 @@ fi
 LIBS=$previous_libs
 
 STATIC_YICES_USES_SHARED_GMP=no
-if test $enable_static = yes -a "$HAS_STATIC_GMP" != yes; then
-  if test "$HAS_SHARED_GMP" != yes; then
-    as_fn_error $? "*** You have --enable-static but no static or shared libgmp found." "$LINENO" 5
-    as_fn_error $? "*** Try giving --with-static-gmp= or setting LDFLAGS." "$LINENO" 5
-  else
-    STATIC_LIBS+=" -lgmp"
-    STATIC_YICES_USES_SHARED_GMP=yes
+if test $enable_static = yes; then
+  if test $pic_mode != yes; then
+    # A) Normal static mode: libyices.a is built against either
+    #      1) a non-pic libgmp.a
+    #   or 2) a shared libgmp
+    if test "$HAS_STATIC_GMP" != yes; then
+      if test "$HAS_SHARED_GMP" != yes; then
+        as_fn_error $? "*** You have --enable-static but no static or shared libgmp found." "$LINENO" 5
+        as_fn_error $? "*** Try giving --with-static-gmp= or setting LDFLAGS." "$LINENO" 5
+      else
+        { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: *** You have --enable-static and no static libgmp.a found." >&5
+$as_echo "$as_me: WARNING: *** You have --enable-static and no static libgmp.a found." >&2;}
+        { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: *** You can give --with-static-gmp= or pass LDFLAGS. Defaulting to shared gmp -lgmp." >&5
+$as_echo "$as_me: WARNING: *** You can give --with-static-gmp= or pass LDFLAGS. Defaulting to shared gmp -lgmp." >&2;}
+        STATIC_LIBS+=" -lgmp"
+        STATIC_YICES_USES_SHARED_GMP=yes
+      fi
+    fi
+  else # $pic_mode = yes
+    # B) PIC static mode: libyices.a is built against either
+    #      1) a pic libgmp.a
+    #   or 2) a shared libgmp
+    if test "$HAS_PIC_GMP" != yes; then
+      if test "$HAS_SHARED_GMP" != yes; then
+        as_fn_error $? "*** You have --enable-static and --with-pic but no PIC libgmp.a or shared libgmp found." "$LINENO" 5
+        as_fn_error $? "*** Try giving --with-pic-gmp= or setting LDFLAGS." "$LINENO" 5
+      else
+        { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: *** You have --enable-static and --with-pic and no static PIC libgmp.a found." >&5
+$as_echo "$as_me: WARNING: *** You have --enable-static and --with-pic and no static PIC libgmp.a found." >&2;}
+        { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: *** You can give --with-pic-gmp= or pass LDFLAGS. Defaulting to shared gmp -lgmp." >&5
+$as_echo "$as_me: WARNING: *** You can give --with-pic-gmp= or pass LDFLAGS. Defaulting to shared gmp -lgmp." >&2;}
+        STATIC_LIBS+=" -lgmp"
+        STATIC_YICES_USES_SHARED_GMP=yes
+      fi
+    else
+      STATIC_GMP=$PIC_GMP
+      STATIC_GMP_INCLUDE_DIR=$PIC_GMP_INCLUDE_DIR
+    fi
   fi
 fi
 
@@ -17776,7 +17815,8 @@ For static library          $libyices_a:
   STATIC_LIBS:              $STATIC_LIBS
   Libgmp.a found:           $HAS_STATIC_GMP
   Libgmp.a path:            $STATIC_GMP
-  Libgmp.a is pic:          $STATIC_GMP_HAS_PIC (non-PIC is faster for the static library)
+  Libgmp.a is pic:          $STATIC_GMP_HAS_PIC     (non-PIC is faster for the static library)
+  PIC mode for libyices.a:  $pic_mode
   Use shared gmp instead of libgmp.a:  $STATIC_YICES_USES_SHARED_GMP
   Embed gmp in libyices.a:  $GMP_EMBEDDED
 

ext/yices/configure.ac

@@ -387,7 +387,7 @@ case $host_os,$FORCE_SHARED_GMP in
 
     # If shared library is enabled and --with-pic-gmp is given, test that
     # it is in fact PIC.
-    if test $enable_shared = yes -a "x$pic_libgmp" != x; then
+    if test "x$pic_libgmp" != x; then
       CSL_CHECK_HEADER([gmp.h],[$pic_includegmp "$(dirname $pic_libgmp)" "$(dirname $pic_libgmp)/../include"],--with-pic-gmp-include-dir)
       CSL_CHECK_LIB_PATH($pic_libgmp,--with-pic-gmp)
       CSL_CHECK_GMP($testlib,$testincludedir)
@@ -405,6 +405,14 @@ case $host_os,$FORCE_SHARED_GMP in
       fi
       PIC_GMP=$testlib
       PIC_GMP_INCLUDE_DIR=$testincludedir
+      # If the PIC mode is enabled, we want the produced libyices.a to be
+      # built against a PIC version of libgmp.a.
+      if test $pic_mode = yes; then
+        STATIC_GMP=$PIC_GMP
+        STATIC_GMP_INCLUDE_DIR=$PIC_GMP_INCLUDE_DIR
+        STATIC_GMP_HAS_PIC=yes
+        PIC_GMP_HAS_PIC=yes
+      fi
     fi
     ;;
   mingw* | cygwin*)
@@ -709,13 +717,40 @@ AC_SUBST(HAS_SHARED_GMP)
 LIBS=$previous_libs
 
 STATIC_YICES_USES_SHARED_GMP=no
-if test $enable_static = yes -a "$HAS_STATIC_GMP" != yes; then
-  if test "$HAS_SHARED_GMP" != yes; then
-    AC_MSG_ERROR([*** You have --enable-static but no static or shared libgmp found.])
-    AC_MSG_ERROR([*** Try giving --with-static-gmp= or setting LDFLAGS.])
-  else
-    STATIC_LIBS+=" -lgmp"
-    STATIC_YICES_USES_SHARED_GMP=yes
+if test $enable_static = yes; then
+  if test $pic_mode != yes; then
+    # A) Normal static mode: libyices.a is built against either
+    #      1) a non-pic libgmp.a
+    #   or 2) a shared libgmp
+    if test "$HAS_STATIC_GMP" != yes; then
+      if test "$HAS_SHARED_GMP" != yes; then
+        AC_MSG_ERROR([*** You have --enable-static but no static or shared libgmp found.])
+        AC_MSG_ERROR([*** Try giving --with-static-gmp= or setting LDFLAGS.])
+      else
+        AC_MSG_WARN([*** You have --enable-static and no static libgmp.a found.])
+        AC_MSG_WARN([*** You can give --with-static-gmp= or pass LDFLAGS. Defaulting to shared gmp -lgmp.])
+        STATIC_LIBS+=" -lgmp"
+        STATIC_YICES_USES_SHARED_GMP=yes
+      fi
+    fi
+  else # $pic_mode = yes
+    # B) PIC static mode: libyices.a is built against either
+    #      1) a pic libgmp.a
+    #   or 2) a shared libgmp
+    if test "$HAS_PIC_GMP" != yes; then
+      if test "$HAS_SHARED_GMP" != yes; then
+        AC_MSG_ERROR([*** You have --enable-static and --with-pic but no PIC libgmp.a or shared libgmp found.])
+        AC_MSG_ERROR([*** Try giving --with-pic-gmp= or setting LDFLAGS.])
+      else
+        AC_MSG_WARN([*** You have --enable-static and --with-pic and no static PIC libgmp.a found.])
+        AC_MSG_WARN([*** You can give --with-pic-gmp= or pass LDFLAGS. Defaulting to shared gmp -lgmp.])
+        STATIC_LIBS+=" -lgmp"
+        STATIC_YICES_USES_SHARED_GMP=yes
+      fi
+    else
+      STATIC_GMP=$PIC_GMP
+      STATIC_GMP_INCLUDE_DIR=$PIC_GMP_INCLUDE_DIR
+    fi
   fi
 fi
 AC_SUBST(STATIC_LIBS)
@@ -862,7 +897,8 @@ For static library          $libyices_a:
   STATIC_LIBS:              $STATIC_LIBS
   Libgmp.a found:           $HAS_STATIC_GMP
   Libgmp.a path:            $STATIC_GMP
-  Libgmp.a is pic:          $STATIC_GMP_HAS_PIC (non-PIC is faster for the static library)
+  Libgmp.a is pic:          $STATIC_GMP_HAS_PIC     (non-PIC is faster for the static library)
+  PIC mode for libyices.a:  $pic_mode
   Use shared gmp instead of libgmp.a:  $STATIC_YICES_USES_SHARED_GMP
   Embed gmp in libyices.a:  $GMP_EMBEDDED