Fix shared library Windows builds with LibPoly (#8306)

This commit fixes two issues that prevented us from compiling a shared
build of cvc5 for Windows:

    The search path of LibPoly is fixed to /usr/x86_64-w64-mingw32 when
    cross-compiling for Windows
    (https://github.com/SRI-CSL/libpoly/blob/06d4e3c1a1c18a5253398889c296ef787a3ce1cd/cmake/x86_64-w64-mingw32.cmake#L10).
    As a result, LibPoly was not able to find the cross-compiled version
    of GMP in our deps folder. Instead of passing search paths to
    LibPoly, this commit changes the CMAKE_ARGS passed to LibPoly to
    directly contain GMP_INCLUDE_DIR and GMP_LIBRARY.
    LibPoly installs the generated .dll files into bin instead of
    lib
    (https://github.com/SRI-CSL/libpoly/blob/06d4e3c1a1c18a5253398889c296ef787a3ce1cd/src/CMakeLists.txt#L91).
    The commit changes the by-products and
    Poly_LIBRARIES/PolyXX_LIBRARIES to account for this.

diff --git a/cmake/FindPoly.cmake b/cmake/FindPoly.cmake
index 99a857d273cb7054299c8f460ec09fcf7d35206c..9c72afc239ea1487985b84a32eee423a21a271c7 100644 (file)
--- a/cmake/FindPoly.cmake
+++ b/cmake/FindPoly.cmake
@@ -49,39 +49,104 @@ if(NOT Poly_FOUND_SYSTEM)
 
   check_if_cross_compiling(CCWIN "Windows" "")
   if(CCWIN)
-    set(patchcmd COMMAND
+    set(POLY_PATCH_CMD COMMAND
       ${CMAKE_SOURCE_DIR}/cmake/deps-utils/Poly-windows-patch.sh <SOURCE_DIR>
     )
   else()
-    unset(patchcmd)
+    unset(POLY_PATCH_CMD)
   endif()
 
   get_target_property(GMP_INCLUDE_DIR GMP INTERFACE_INCLUDE_DIRECTORIES)
   get_target_property(GMP_LIBRARY GMP IMPORTED_LOCATION)
   get_filename_component(GMP_LIB_PATH "${GMP_LIBRARY}" DIRECTORY)
 
-  set(POLY_BYPRODUCTS
-    <INSTALL_DIR>/lib/libpicpoly.a
-    <INSTALL_DIR>/lib/libpicpolyxx.a
-    <INSTALL_DIR>/lib/libpoly${CMAKE_SHARED_LIBRARY_SUFFIX}
-    <INSTALL_DIR>/lib/libpolyxx${CMAKE_SHARED_LIBRARY_SUFFIX}
-  )
-  if(CMAKE_SYSTEM_NAME STREQUAL "Darwin")
-    list(APPEND POLY_BYPRODUCTS
-      <INSTALL_DIR>/lib/libpoly.0${CMAKE_SHARED_LIBRARY_SUFFIX}
-      <INSTALL_DIR>/lib/libpoly.0.1.11${CMAKE_SHARED_LIBRARY_SUFFIX}
-      <INSTALL_DIR>/lib/libpolyxx.0${CMAKE_SHARED_LIBRARY_SUFFIX}
-      <INSTALL_DIR>/lib/libpolyxx.0.1.11${CMAKE_SHARED_LIBRARY_SUFFIX}
+
+  set(Poly_INCLUDE_DIR "${DEPS_BASE}/include/")
+
+  if(BUILD_SHARED_LIBS)
+    set(POLY_BUILD_STATIC OFF)
+    set(POLY_TARGETS poly polyxx)
+    set(POLY_INSTALL_CMD
+      INSTALL_COMMAND 
+        ${CMAKE_MAKE_PROGRAM} install ${POLY_TARGETS}
+    )
+
+    if(CMAKE_SYSTEM_NAME STREQUAL "Darwin")
+      set(POLY_BYPRODUCTS
+        <INSTALL_DIR>/lib/libpoly.0${CMAKE_SHARED_LIBRARY_SUFFIX}
+        <INSTALL_DIR>/lib/libpoly.0.1.11${CMAKE_SHARED_LIBRARY_SUFFIX}
+        <INSTALL_DIR>/lib/libpolyxx.0${CMAKE_SHARED_LIBRARY_SUFFIX}
+        <INSTALL_DIR>/lib/libpolyxx.0.1.11${CMAKE_SHARED_LIBRARY_SUFFIX}
+        <INSTALL_DIR>/lib/libpoly${CMAKE_SHARED_LIBRARY_SUFFIX}
+        <INSTALL_DIR>/lib/libpolyxx${CMAKE_SHARED_LIBRARY_SUFFIX}
+      )
+      set(Poly_LIBRARIES "${DEPS_BASE}/lib/libpoly${CMAKE_SHARED_LIBRARY_SUFFIX}")
+      set(PolyXX_LIBRARIES "${DEPS_BASE}/lib/libpolyxx${CMAKE_SHARED_LIBRARY_SUFFIX}")
+    elseif(CMAKE_SYSTEM_NAME STREQUAL "Windows")
+      # For Windows builds, LibPoly installs the .dlls to the bin directory
+      set(POLY_BYPRODUCTS
+        <INSTALL_DIR>/bin/libpoly${CMAKE_SHARED_LIBRARY_SUFFIX}
+        <INSTALL_DIR>/bin/libpolyxx${CMAKE_SHARED_LIBRARY_SUFFIX}
+      )
+      set(Poly_LIBRARIES "${DEPS_BASE}/bin/libpoly${CMAKE_SHARED_LIBRARY_SUFFIX}")
+      set(PolyXX_LIBRARIES "${DEPS_BASE}/bin/libpolyxx${CMAKE_SHARED_LIBRARY_SUFFIX}")
+    else()
+      set(POLY_BYPRODUCTS
+        <INSTALL_DIR>/lib/libpoly${CMAKE_SHARED_LIBRARY_SUFFIX}.0
+        <INSTALL_DIR>/lib/libpoly${CMAKE_SHARED_LIBRARY_SUFFIX}.0.1.11
+        <INSTALL_DIR>/lib/libpolyxx${CMAKE_SHARED_LIBRARY_SUFFIX}.0
+        <INSTALL_DIR>/lib/libpolyxx${CMAKE_SHARED_LIBRARY_SUFFIX}.0.1.11
+        <INSTALL_DIR>/lib/libpoly${CMAKE_SHARED_LIBRARY_SUFFIX}
+        <INSTALL_DIR>/lib/libpolyxx${CMAKE_SHARED_LIBRARY_SUFFIX}
+      )
+      set(Poly_LIBRARIES "${DEPS_BASE}/lib/libpoly${CMAKE_SHARED_LIBRARY_SUFFIX}")
+      set(PolyXX_LIBRARIES "${DEPS_BASE}/lib/libpolyxx${CMAKE_SHARED_LIBRARY_SUFFIX}")
+    endif()
+  else()
+    # For static builds, we only build and install the `static_pic_poly` and
+    # `static_pic_polyxx` targets. We pass the full path of GMP to LibPoly
+    # below. If we are building a static version of cvc5, it is the static
+    # version of GMP, which does not work for building a shared version of
+    # LibPoly.
+    set(POLY_BUILD_STATIC ON)
+    set(POLY_TARGETS static_pic_poly static_pic_polyxx)
+    set(POLY_INSTALL_CMD
+      INSTALL_COMMAND 
+        ${CMAKE_MAKE_PROGRAM} install ${POLY_TARGETS}
+      COMMAND
+        ${CMAKE_COMMAND} -E copy
+          src/libpicpoly${CMAKE_STATIC_LIBRARY_SUFFIX}
+          <INSTALL_DIR>/lib/libpicpoly${CMAKE_STATIC_LIBRARY_SUFFIX}
+      COMMAND
+        ${CMAKE_COMMAND} -E copy
+          src/libpicpolyxx${CMAKE_STATIC_LIBRARY_SUFFIX}
+          <INSTALL_DIR>/lib/libpicpolyxx${CMAKE_STATIC_LIBRARY_SUFFIX}
     )
-  elseif(CMAKE_SYSTEM_NAME STREQUAL "Linux")
-    list(APPEND POLY_BYPRODUCTS
-      <INSTALL_DIR>/lib/libpoly${CMAKE_SHARED_LIBRARY_SUFFIX}.0
-      <INSTALL_DIR>/lib/libpoly${CMAKE_SHARED_LIBRARY_SUFFIX}.0.1.11
-      <INSTALL_DIR>/lib/libpolyxx${CMAKE_SHARED_LIBRARY_SUFFIX}.0
-      <INSTALL_DIR>/lib/libpolyxx${CMAKE_SHARED_LIBRARY_SUFFIX}.0.1.11
+
+    # We only want to install the headers and the position-independent version
+    # of the static libraries, so remove the installation targets for the other
+    # versions of LibPoly
+    set(POLY_PATCH_CMD ${POLY_PATCH_CMD}
+      COMMAND
+        sed -ri.orig
+          "/TARGETS (poly|polyxx|static_poly|static_polyxx) /d"
+          <SOURCE_DIR>/src/CMakeLists.txt
+    )
+
+    set(POLY_BYPRODUCTS
+      <INSTALL_DIR>/lib/libpicpoly${CMAKE_STATIC_LIBRARY_SUFFIX}
+      <INSTALL_DIR>/lib/libpicpolyxx${CMAKE_STATIC_LIBRARY_SUFFIX}
     )
+    set(Poly_LIBRARIES
+      "${DEPS_BASE}/lib/libpicpoly${CMAKE_STATIC_LIBRARY_SUFFIX}")
+    set(PolyXX_LIBRARIES
+      "${DEPS_BASE}/lib/libpicpolyxx${CMAKE_STATIC_LIBRARY_SUFFIX}")
   endif()
 
+  # We pass the full path of GMP to LibPoly, s.t. we can ensure that LibPoly is
+  # able to find the correct version of GMP if we built it locally. This is
+  # primarily important for cross-compiling cvc5, because LibPoly's search
+  # paths make it impossible to find the locally built GMP library otherwise.
   ExternalProject_Add(
     Poly-EP
     ${COMMON_EP_CONFIG}
@@ -90,22 +155,19 @@ if(NOT Poly_FOUND_SYSTEM)
     PATCH_COMMAND
       sed -i.orig
       "s,add_subdirectory(test/polyxx),add_subdirectory(test/polyxx EXCLUDE_FROM_ALL),g"
-      <SOURCE_DIR>/CMakeLists.txt ${patchcmd}
+      <SOURCE_DIR>/CMakeLists.txt
+      ${POLY_PATCH_CMD}
     CMAKE_ARGS -DCMAKE_BUILD_TYPE=Release
                -DCMAKE_INSTALL_PREFIX=<INSTALL_DIR>
                -DCMAKE_TOOLCHAIN_FILE=${CMAKE_TOOLCHAIN_FILE}
                -DLIBPOLY_BUILD_PYTHON_API=OFF
-               -DLIBPOLY_BUILD_STATIC=ON
-               -DLIBPOLY_BUILD_STATIC_PIC=ON
-               -DCMAKE_INCLUDE_PATH=${GMP_INCLUDE_DIR}
-               -DCMAKE_LIBRARY_PATH=${GMP_LIB_PATH}
-    BUILD_COMMAND ${CMAKE_MAKE_PROGRAM}
-    COMMAND ${CMAKE_MAKE_PROGRAM} static_pic_poly static_pic_polyxx
-    INSTALL_COMMAND ${CMAKE_MAKE_PROGRAM} install
-    COMMAND ${CMAKE_COMMAND} -E copy src/libpicpoly.a
-            <INSTALL_DIR>/lib/libpicpoly.a
-    COMMAND ${CMAKE_COMMAND} -E copy src/libpicpolyxx.a
-            <INSTALL_DIR>/lib/libpicpolyxx.a
+               -DLIBPOLY_BUILD_STATIC=${POLY_BUILD_STATIC}
+               -DLIBPOLY_BUILD_STATIC_PIC=${POLY_BUILD_STATIC}
+               -DGMP_INCLUDE_DIR=${GMP_INCLUDE_DIR}
+               -DGMP_LIBRARY=${GMP_LIBRARIES}
+               -DCMAKE_SKIP_INSTALL_ALL_DEPENDENCY=TRUE
+    BUILD_COMMAND ${CMAKE_MAKE_PROGRAM} ${POLY_TARGETS}
+    ${POLY_INSTALL_CMD}
     BUILD_BYPRODUCTS ${POLY_BYPRODUCTS}
   )
   ExternalProject_Add_Step(
@@ -114,15 +176,6 @@ if(NOT Poly_FOUND_SYSTEM)
     COMMAND ${CMAKE_COMMAND} -E remove_directory <BINARY_DIR>/test/
   )
   add_dependencies(Poly-EP GMP)
-
-  set(Poly_INCLUDE_DIR "${DEPS_BASE}/include/")
-  if(BUILD_SHARED_LIBS)
-    set(Poly_LIBRARIES "${DEPS_BASE}/lib/libpoly${CMAKE_SHARED_LIBRARY_SUFFIX}")
-    set(PolyXX_LIBRARIES "${DEPS_BASE}/lib/libpolyxx${CMAKE_SHARED_LIBRARY_SUFFIX}")
-  else()
-    set(Poly_LIBRARIES "${DEPS_BASE}/lib/libpicpoly.a")
-    set(PolyXX_LIBRARIES "${DEPS_BASE}/lib/libpicpolyxx.a")
-  endif()
 endif()
 
 set(Poly_FOUND TRUE)
@@ -158,9 +211,9 @@ mark_as_advanced(Poly_LIBRARIES)
 mark_as_advanced(PolyXX_LIBRARIES)
 
 if(Poly_FOUND_SYSTEM)
-  message(STATUS "Found Poly ${Poly_VERSION}: ${Poly_LIBRARIES}")
+  message(STATUS "Found Poly ${Poly_VERSION}: ${Poly_LIBRARIES}, ${PolyXX_LIBRARIES}")
 else()
-  message(STATUS "Building Poly ${Poly_VERSION}: ${Poly_LIBRARIES}")
+  message(STATUS "Building Poly ${Poly_VERSION}: ${Poly_LIBRARIES}, ${PolyXX_LIBRARIES}")
   add_dependencies(Poly Poly-EP)
   add_dependencies(Polyxx Poly-EP)