Refactors GMP and libpoly to also use external projects and be available within cmake as proper targets.
- name: Setup Dependencies
if: steps.restore-deps.outputs.cache-hit != 'true'
run: |
- ./contrib/get-poly
./contrib/get-lfsc-checker
- - name: List dependencies
- run: |
- find deps/install -type f
-
# GitHub actions currently does not support modifying an already existing
# cache. Hence, we create a new cache for each commit with key
# cache-${{ runner.os }}-${{ matrix.cache-key }}-${{ github.sha }}. This
## directory for licensing information.
##
# Find GMP
-# GMP_FOUND - system has GMP lib
-# GMP_INCLUDE_DIR - the GMP include directory
-# GMP_LIBRARIES - Libraries needed to use GMP
+# GMP_FOUND - should always be true
+# GMP - target for the GMP library
+
+include(deps-helper)
find_path(GMP_INCLUDE_DIR NAMES gmp.h gmpxx.h)
find_library(GMP_LIBRARIES NAMES gmp)
-include(FindPackageHandleStandardArgs)
-find_package_handle_standard_args(GMP DEFAULT_MSG GMP_INCLUDE_DIR GMP_LIBRARIES)
+set(GMP_FOUND_SYSTEM FALSE)
+if(GMP_INCLUDE_DIR AND GMP_LIBRARIES)
+ set(GMP_FOUND_SYSTEM TRUE)
+
+ function(getversionpart OUTPUT FILENAME DESC)
+ file(STRINGS ${FILENAME} RES REGEX "^#define __GNU_MP_${DESC}[ \\t]+.*")
+ string(REGEX MATCH "[0-9]+" RES "${RES}")
+ set(${OUTPUT}
+ "${RES}"
+ PARENT_SCOPE
+ )
+ endfunction()
+ getversionpart(MAJOR "${GMP_INCLUDE_DIR}/gmp.h" "VERSION")
+ getversionpart(MINOR "${GMP_INCLUDE_DIR}/gmp.h" "VERSION_MINOR")
+ getversionpart(PATCH "${GMP_INCLUDE_DIR}/gmp.h" "VERSION_PATCHLEVEL")
+ set(GMP_VERSION
+ "${MAJOR}.${MINOR}.${PATCH}"
+ PARENT_SCOPE
+ )
+
+ check_system_version("GMP")
+endif()
+
+if(NOT GMP_FOUND_SYSTEM)
+ include(ExternalProject)
+
+ set(GMP_VERSION "6.2.1")
+
+ ExternalProject_Add(
+ GMP-EP
+ PREFIX ${DEPS_PREFIX}
+ URL https://gmplib.org/download/gmp/gmp-${GMP_VERSION}.tar.bz2
+ URL_HASH SHA1=2dcf34d4a432dbe6cce1475a835d20fe44f75822
+ CONFIGURE_COMMAND
+ <SOURCE_DIR>/configure --prefix=<INSTALL_DIR> --enable-cxx --with-pic
+ --disable-shared --enable-static --host=${TOOLCHAIN_PREFIX}
+ BUILD_BYPRODUCTS <INSTALL_DIR>/lib/libgmp.a
+ )
+
+ set(GMP_INCLUDE_DIR "${DEPS_BASE}/include/")
+ set(GMP_LIBRARIES "${DEPS_BASE}/lib/libgmp.a")
+endif()
+
+set(GMP_FOUND TRUE)
+
+add_library(GMP STATIC IMPORTED GLOBAL)
+set_target_properties(GMP PROPERTIES IMPORTED_LOCATION "${GMP_LIBRARIES}")
+set_target_properties(
+ GMP PROPERTIES INTERFACE_INCLUDE_DIRECTORIES "${GMP_INCLUDE_DIR}"
+)
+
+mark_as_advanced(GMP_FOUND)
+mark_as_advanced(GMP_FOUND_SYSTEM)
+mark_as_advanced(GMP_INCLUDE_DIR)
+mark_as_advanced(GMP_LIBRARIES)
-mark_as_advanced(GMP_INCLUDE_DIR GMP_LIBRARIES)
-if(GMP_LIBRARIES)
- message(STATUS "Found GMP libs: ${GMP_LIBRARIES}")
+if(GMP_FOUND_SYSTEM)
+ message(STATUS "Found GMP ${GMP_VERSION}: ${GMP_LIBRARIES}")
+else()
+ message(STATUS "Building GMP ${GMP_VERSION}: ${GMP_LIBRARIES}")
+ add_dependencies(GMP GMP-EP)
endif()
## directory for licensing information.
##
# Find LibPoly
-# POLY_FOUND - system has LibPoly
-# POLY_INCLUDE_DIR - the LibPoly include directory
-# POLY_LIBRARIES - Libraries needed to use LibPoly
-
-# Note: contrib/get-poly copies header files to deps/install/include/poly.
-# However, includes in LibPoly headers are not prefixed with "poly/" and therefore
-# we have to look for headers in include/poly instead of include/.
-find_path(POLY_INCLUDE_DIR NAMES poly/poly.h PATH_SUFFIXES poly)
-find_library(POLY_LIB NAMES poly)
-find_library(POLY_LIBXX NAMES polyxx)
-set(POLY_LIBRARIES "${POLY_LIBXX};${POLY_LIB}")
-unset(POLY_LIB CACHE)
-unset(POLY_LIBXX CACHE)
-
-include(FindPackageHandleStandardArgs)
-find_package_handle_standard_args(Poly
- DEFAULT_MSG
- POLY_INCLUDE_DIR POLY_LIBRARIES)
-
-mark_as_advanced(POLY_INCLUDE_DIR POLY_LIBRARIES)
-if(POLY_LIBRARIES)
- message(STATUS "Found LibPoly: ${POLY_LIBRARIES}")
+# Poly_FOUND - should always be true
+# Poly - target for the libpoly library
+# Polyxx - target for the C++ interface of libpoly, also links Poly
+
+include(deps-helper)
+
+find_path(Poly_INCLUDE_DIR NAMES poly/poly.h)
+find_library(Poly_LIBRARIES NAMES poly)
+find_library(PolyXX_LIBRARIES NAMES polyxx)
+
+set(Dummy_FOUND_SYSTEM FALSE)
+if(Poly_INCLUDE_DIR
+ AND Poly_LIBRARIES
+ AND PolyXX_LIBRARIES
+)
+ set(Poly_FOUND_SYSTEM TRUE)
+
+ file(STRINGS ${Poly_INCLUDE_DIR}/poly/version.h Poly_VERSION
+ REGEX "^#define[\t ]+LIBPOLY_VERSION [0-9+]+"
+ )
+ string(REGEX MATCH "[0-9.]+" Poly_VERSION "${Poly_VERSION}")
+
+ check_system_version("Poly")
+endif()
+
+if(NOT Poly_FOUND_SYSTEM)
+ include(ExternalProject)
+
+ # TODO(#4706): Use proper release, after the next release
+ set(Poly_VERSION "bae67639726f63ed508a30845108bfdac4a77546")
+
+ check_if_cross_compiling(CCWIN "Windows" "")
+ if(CCWIN)
+ # Roughly following https://stackoverflow.com/a/44383330/2375725
+ set(patchcmd
+ PATCH_COMMAND
+ patch
+ <SOURCE_DIR>/src/CMakeLists.txt
+ ${CMAKE_CURRENT_LIST_DIR}/deps-utils/Poly-patch-cmake.patch
+ # Avoid %z and %llu format specifiers
+ COMMAND find <SOURCE_DIR>/ -type f -exec
+ sed -i.orig "s/%z[diu]/%\" PRIu64 \"/g" {} +
+ COMMAND find <SOURCE_DIR>/ -type f -exec
+ sed -i.orig "s/%ll[du]/%\" PRIu64 \"/g" {} +
+ # Make sure the new macros are available
+ COMMAND find <SOURCE_DIR>/ -type f -exec
+ sed -i.orig "s/#include <stdio.h>/#include <stdio.h>\\n#include <inttypes.h>/" {} +
+ COMMAND find <SOURCE_DIR>/ -type f -exec
+ sed -i.orig "s/#include <cstdio>/#include <cstdio>\\n#include <inttypes.h>/" {} +
+ )
+ else()
+ unset(patchcmd)
+ endif()
+
+ ExternalProject_Add(
+ Poly-EP
+ PREFIX ${DEPS_PREFIX}
+ URL https://github.com/SRI-CSL/libpoly/archive/${Poly_VERSION}.tar.gz
+ URL_HASH SHA1=2e79d5220d3ecbb40811463fcf12c5ddbd4b9f30
+ DOWNLOAD_NAME libpoly.tar.gz
+ ${patchcmd}
+ 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
+ BUILD_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
+ BUILD_BYPRODUCTS <INSTALL_DIR>/lib/libpicpoly.a
+ <INSTALL_DIR>/lib/libpicpolyxx.a
+ )
+ ExternalProject_Add_Step(
+ Poly-EP cleanup
+ DEPENDEES install
+ COMMAND ${CMAKE_COMMAND} -E remove_directory <SOURCE_DIR>/test/
+ COMMAND ${CMAKE_COMMAND} -E remove_directory <BINARY_DIR>/test/
+ )
+ add_dependencies(Poly-EP GMP)
+
+ set(Poly_INCLUDE_DIR "${DEPS_BASE}/include/")
+ set(Poly_LIBRARIES "${DEPS_BASE}/lib/libpicpoly.a")
+ set(PolyXX_LIBRARIES "${DEPS_BASE}/lib/libpicpolyxx.a")
+endif()
+
+set(Poly_FOUND TRUE)
+
+add_library(Poly STATIC IMPORTED GLOBAL)
+set_target_properties(Poly PROPERTIES IMPORTED_LOCATION "${Poly_LIBRARIES}")
+set_target_properties(
+ Poly PROPERTIES INTERFACE_INCLUDE_DIRECTORIES "${Poly_INCLUDE_DIR}"
+)
+
+add_library(Polyxx STATIC IMPORTED GLOBAL)
+set_target_properties(Polyxx PROPERTIES IMPORTED_LOCATION "${PolyXX_LIBRARIES}")
+set_target_properties(
+ Polyxx PROPERTIES INTERFACE_INCLUDE_DIRECTORIES "${Poly_INCLUDE_DIR}"
+)
+set_target_properties(Polyxx PROPERTIES INTERFACE_LINK_LIBRARIES Poly)
+
+mark_as_advanced(Poly_FOUND)
+mark_as_advanced(Poly_FOUND_SYSTEM)
+mark_as_advanced(Poly_INCLUDE_DIR)
+mark_as_advanced(Poly_LIBRARIES)
+mark_as_advanced(PolyXX_LIBRARIES)
+
+if(Poly_FOUND_SYSTEM)
+ message(STATUS "Found Poly ${Poly_VERSION}: ${Poly_LIBRARIES}")
+else()
+ message(STATUS "Building Poly ${Poly_VERSION}: ${Poly_LIBRARIES}")
+ add_dependencies(Poly Poly-EP)
+ add_dependencies(Polyxx Poly-EP)
endif()
# we are cross compiling if
# - CMAKE_SYSTEM_NAME has been changed to ${name}
# - CMAKE_SYSTEM_PROCESSOR has been changed to ${processor}
-function(fail_if_cross_compiling name processor target error)
- set(FAIL FALSE)
+function(check_if_cross_compiling OUT name processor)
if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "${CMAKE_HOST_SYSTEM_NAME}")
if(NOT "${name}" STREQUAL "")
if("${CMAKE_SYSTEM_NAME}" STREQUAL "${name}")
- set(FAIL TRUE)
+ set(${OUT} TRUE PARENT_SCOPE)
+ return()
endif()
endif()
endif()
if(NOT "${CMAKE_SYSTEM_PROCESSOR}" STREQUAL "${CMAKE_HOST_SYSTEM_PROCESSOR}")
if(NOT "${processor}" STREQUAL "")
if("${CMAKE_SYSTEM_PROCESSOR}" STREQUAL "${processor}")
- set(FAIL TRUE)
+ set(${OUT} TRUE PARENT_SCOPE)
+ return()
endif()
endif()
endif()
+ set(${OUT} FALSE PARENT_SCOPE)
+endfunction(check_if_cross_compiling)
+
+# fail if we are cross compiling as indicated by name and processor
+# we are cross compiling if
+# - CMAKE_SYSTEM_NAME has been changed to ${name}
+# - CMAKE_SYSTEM_PROCESSOR has been changed to ${processor}
+function(fail_if_cross_compiling name processor target error)
+ check_if_cross_compiling(FAIL "${name}" "${processor}")
if(FAIL)
message(SEND_ERROR
- "We are cross compiling from \
+ "We are cross compiling from \
${CMAKE_HOST_SYSTEM_NAME}-${CMAKE_HOST_SYSTEM_PROCESSOR} to \
${CMAKE_SYSTEM_NAME}-${CMAKE_SYSTEM_PROCESSOR}.\n"
- "This is not supported by ${target}:\n"
- "${error}")
+ "This is not supported by ${target}:\n"
+ "${error}")
endif()
endfunction(fail_if_cross_compiling)
+
+function(fail_if_include_missing include target)
+ include(CheckIncludeFileCXX)
+ check_include_file_cxx(${include} HAVE_INCLUDE)
+ if(NOT HAVE_INCLUDE)
+ message(SEND_ERROR "${target} requires ${include} header, but it is not available.")
+ endif()
+endfunction(fail_if_include_missing)
+++ /dev/null
-#!/usr/bin/env bash
-#
-# This script should only be used if your distribution does not ship with the
-# GMP configuration you need. For example, for cross-compiling GMP for Windows
-# or Linux ARM platforms. You can also use the script if your
-# distribution does not ship with static GMP libraries (e.g., Arch Linux) and
-# you want to build CVC4 statically.
-# In most of the cases the GMP version installed on your system is the one you
-# want and should use.
-#
-
-source "$(dirname "$0")/get-script-header.sh"
-
-CONFIG=
-while :; do
- case $1 in
- --host=?*)
- host=${1#*=}
- CONFIG="--host=$host"
- ;;
- --host=)
- echo "Error: empty --host="
- exit 1
- ;;
- *)
- break
- esac
- shift
-done
-
-[ -z "${BUILD_TYPE}" ] && BUILD_TYPE="--disable-shared --enable-static"
-[ -z "$GMPVERSION" ] && GMPVERSION=6.2.1
-
-GMP_DIR="$DEPS_DIR/gmp-$GMPVERSION"
-rm -rf "$GMP_DIR"
-
-echo =============================================================================
-echo
-echo "This script should only be used if your distribution does not ship with the"
-echo "GMP configuration you need. For example, for cross-compiling GMP for"
-echo "Windows or Linux ARM platforms. You can also use the script if your Linux"
-echo "distribution does not ship with static GMP libraries (e.g., Arch Linux)"
-echo "and you want to build CVC4 statically."
-echo
-echo "In most of the cases the GMP version installed on your system is the one you"
-echo "want and should use."
-echo
-echo =============================================================================
-echo
-echo "Setting up GMP $GMPVERSION..."
-echo
-setup_dep "https://gmplib.org/download/gmp/gmp-$GMPVERSION.tar.bz2" "$GMP_DIR"
-cd "$GMP_DIR"
-./configure ${CONFIG} --prefix="$INSTALL_DIR" --enable-cxx ${BUILD_TYPE}
-make \
- CFLAGS="${MAKE_CFLAGS}" \
- CXXFLAGS="${MAKE_CXXFLAGS}" \
- LDFLAGS="${MAKE_LDFLAGS}" \
- -j$(nproc)
-make install
-echo
+++ /dev/null
-#!/usr/bin/env bash
-#
-source "$(dirname "$0")/get-script-header.sh"
-
-POLY_DIR="$DEPS_DIR/poly"
-version="v0.1.8"
-
-setup_dep \
- "https://github.com/SRI-CSL/libpoly/archive/master.tar.gz" "$POLY_DIR"
-# TODO(Gereon, #4706): Go back to fixed version with the next release
-
-pwd
-cd "$POLY_DIR/build/"
-
-CMAKEFLAGS="\
- -DCMAKE_BUILD_TYPE=Release \
- -DLIBPOLY_BUILD_PYTHON_API=OFF \
- -DLIBPOLY_BUILD_STATIC=ON \
- -DLIBPOLY_BUILD_STATIC_PIC=ON \
-"
-
-echo "Installing to $INSTALL_DIR"
-
-cmake -DCMAKE_INSTALL_PREFIX="$INSTALL_DIR" $CMAKEFLAGS ../ && make -j${NPROC} install
-
-echo
-echo "Using poly version $version"
-echo
-echo ===================== Now configure CVC4 with =====================
-echo ./configure.sh --poly
target_include_directories(cvc4 PRIVATE ${GLPK_INCLUDE_DIR})
endif()
if(USE_POLY)
- target_link_libraries(cvc4 PRIVATE ${POLY_LIBRARIES})
- target_include_directories(cvc4 PRIVATE ${POLY_INCLUDE_DIR})
+ target_link_libraries(cvc4 PRIVATE Polyxx)
endif()
if(USE_SYMFPU)
target_link_libraries(cvc4 PRIVATE SymFPU)
# Note: When linked statically GMP needs to be linked after CLN since CLN
# depends on GMP.
-target_link_libraries(cvc4 PRIVATE ${GMP_LIBRARIES})
-target_include_directories(cvc4 PRIVATE $<BUILD_INTERFACE:${GMP_INCLUDE_DIR}>)
+target_link_libraries(cvc4 PRIVATE GMP)
# Add rt library
# Note: For glibc < 2.17 we have to additionally link against rt (man clock_gettime).
add_dependencies(main cvc4 cvc4parser gen-tokens)
get_target_property(LIBCVC4_INCLUDES cvc4 INCLUDE_DIRECTORIES)
target_include_directories(main PRIVATE ${LIBCVC4_INCLUDES})
+if(USE_CLN)
+ target_link_libraries(main ${CLN_LIBRARIES})
+ target_include_directories(main PRIVATE $<BUILD_INTERFACE:${CLN_INCLUDE_DIR}>)
+endif()
+target_link_libraries(main GMP)
# main-test library is only used for linking against api and unit tests so
# that we don't have to include all object files of main into each api/unit
target_link_libraries(main-test ${CLN_LIBRARIES})
target_include_directories(main-test PRIVATE $<BUILD_INTERFACE:${CLN_INCLUDE_DIR}>)
endif()
-target_link_libraries(main-test ${GMP_LIBRARIES})
-target_include_directories(main-test PRIVATE $<BUILD_INTERFACE:${GMP_INCLUDE_DIR}>)
+target_link_libraries(main-test GMP)
#-----------------------------------------------------------------------------#
# cvc4 binary configuration
target_link_libraries(cvc4-bin ${CLN_LIBRARIES})
target_include_directories(cvc4-bin PRIVATE $<BUILD_INTERFACE:${CLN_INCLUDE_DIR}>)
endif()
-target_link_libraries(cvc4-bin ${GMP_LIBRARIES})
-target_include_directories(cvc4-bin PRIVATE $<BUILD_INTERFACE:${GMP_INCLUDE_DIR}>)
+target_link_libraries(cvc4-bin GMP)
if(PROGRAM_PREFIX)
install(PROGRAMS
$<TARGET_FILE:cvc4-bin>
target_link_libraries(cvc4parser PRIVATE ${CLN_LIBRARIES})
target_include_directories(cvc4parser PRIVATE $<BUILD_INTERFACE:${CLN_INCLUDE_DIR}>)
endif()
-target_link_libraries(cvc4parser PRIVATE ${GMP_LIBRARIES})
-target_include_directories(cvc4parser PRIVATE $<BUILD_INTERFACE:${GMP_INCLUDE_DIR}>)
+target_link_libraries(cvc4parser PRIVATE GMP)
install(TARGETS cvc4parser
EXPORT cvc4-targets
target_link_libraries(${name} ${CLN_LIBRARIES})
target_include_directories(${name} PRIVATE $<BUILD_INTERFACE:${CLN_INCLUDE_DIR}>)
endif()
- target_link_libraries(${name} ${GMP_LIBRARIES})
- target_include_directories(${name} PRIVATE $<BUILD_INTERFACE:${GMP_INCLUDE_DIR}>)
+ target_link_libraries(${name} GMP)
set_target_properties(${name}
PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${test_bin_dir})
add_test(api/${name} ${test_bin_dir}/${name})
target_include_directories(${name} PRIVATE $<BUILD_INTERFACE:${CLN_INCLUDE_DIR}>)
endif()
if(USE_POLY)
- target_link_libraries(${name} ${POLY_LIBRARIES})
- target_include_directories(${name} PRIVATE ${POLY_INCLUDE_DIR})
+ target_link_libraries(${name} Polyxx)
endif()
- target_link_libraries(${name} ${GMP_LIBRARIES})
- target_include_directories(${name} PRIVATE ${GMP_INCLUDE_DIR})
+ target_link_libraries(${name} GMP)
if(${is_white})
target_compile_options(${name} PRIVATE -fno-access-control)
endif()
projects / cvc5.git / commitdiff