From: Andres Noetzli Date: Wed, 16 Mar 2022 01:44:42 +0000 (-0700) Subject: Fix shared library Windows builds with LibPoly (#8306) X-Git-Tag: cvc5-1.0.0~244 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b90a6d149ecf65013f9e1c54a053a666aa651dd8;p=cvc5.git 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 99a857d27..9c72afc23 100644 --- 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 ) 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 - /lib/libpicpoly.a - /lib/libpicpolyxx.a - /lib/libpoly${CMAKE_SHARED_LIBRARY_SUFFIX} - /lib/libpolyxx${CMAKE_SHARED_LIBRARY_SUFFIX} - ) - if(CMAKE_SYSTEM_NAME STREQUAL "Darwin") - list(APPEND POLY_BYPRODUCTS - /lib/libpoly.0${CMAKE_SHARED_LIBRARY_SUFFIX} - /lib/libpoly.0.1.11${CMAKE_SHARED_LIBRARY_SUFFIX} - /lib/libpolyxx.0${CMAKE_SHARED_LIBRARY_SUFFIX} - /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 + /lib/libpoly.0${CMAKE_SHARED_LIBRARY_SUFFIX} + /lib/libpoly.0.1.11${CMAKE_SHARED_LIBRARY_SUFFIX} + /lib/libpolyxx.0${CMAKE_SHARED_LIBRARY_SUFFIX} + /lib/libpolyxx.0.1.11${CMAKE_SHARED_LIBRARY_SUFFIX} + /lib/libpoly${CMAKE_SHARED_LIBRARY_SUFFIX} + /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 + /bin/libpoly${CMAKE_SHARED_LIBRARY_SUFFIX} + /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 + /lib/libpoly${CMAKE_SHARED_LIBRARY_SUFFIX}.0 + /lib/libpoly${CMAKE_SHARED_LIBRARY_SUFFIX}.0.1.11 + /lib/libpolyxx${CMAKE_SHARED_LIBRARY_SUFFIX}.0 + /lib/libpolyxx${CMAKE_SHARED_LIBRARY_SUFFIX}.0.1.11 + /lib/libpoly${CMAKE_SHARED_LIBRARY_SUFFIX} + /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} + /lib/libpicpoly${CMAKE_STATIC_LIBRARY_SUFFIX} + COMMAND + ${CMAKE_COMMAND} -E copy + src/libpicpolyxx${CMAKE_STATIC_LIBRARY_SUFFIX} + /lib/libpicpolyxx${CMAKE_STATIC_LIBRARY_SUFFIX} ) - elseif(CMAKE_SYSTEM_NAME STREQUAL "Linux") - list(APPEND POLY_BYPRODUCTS - /lib/libpoly${CMAKE_SHARED_LIBRARY_SUFFIX}.0 - /lib/libpoly${CMAKE_SHARED_LIBRARY_SUFFIX}.0.1.11 - /lib/libpolyxx${CMAKE_SHARED_LIBRARY_SUFFIX}.0 - /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" + /src/CMakeLists.txt + ) + + set(POLY_BYPRODUCTS + /lib/libpicpoly${CMAKE_STATIC_LIBRARY_SUFFIX} + /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" - /CMakeLists.txt ${patchcmd} + /CMakeLists.txt + ${POLY_PATCH_CMD} CMAKE_ARGS -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX= -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 - /lib/libpicpoly.a - COMMAND ${CMAKE_COMMAND} -E copy src/libpicpolyxx.a - /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 /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)