From 45fadafed080b6b7704ce635fc1c4276d0109f0b Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sat, 9 Mar 2019 03:00:48 +0000 Subject: [PATCH] add Z3 package (#5564) * add Z3 package * z3: don't assume python is installed * [z3] attempt to fix build failure due to path truncation patch already upstreamed * [z3] add support for static build * [z3] Fail preemptively on UWP --- ports/z3/CONTROL | 3 ++ ports/z3/LICENSE | 10 +++++ ports/z3/fix_cmake_long_dir.patch | 61 ++++++++++++++++++++++++++++++ ports/z3/portfile.cmake | 63 +++++++++++++++++++++++++++++++ 4 files changed, 137 insertions(+) create mode 100644 ports/z3/CONTROL create mode 100644 ports/z3/LICENSE create mode 100644 ports/z3/fix_cmake_long_dir.patch create mode 100644 ports/z3/portfile.cmake diff --git a/ports/z3/CONTROL b/ports/z3/CONTROL new file mode 100644 index 000000000..f06d776bb --- /dev/null +++ b/ports/z3/CONTROL @@ -0,0 +1,3 @@ +Source: z3 +Version: 4.8.4 +Description: An SMT solver diff --git a/ports/z3/LICENSE b/ports/z3/LICENSE new file mode 100644 index 000000000..cc90bed74 --- /dev/null +++ b/ports/z3/LICENSE @@ -0,0 +1,10 @@ +Z3 +Copyright (c) Microsoft Corporation +All rights reserved. +MIT License + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. \ No newline at end of file diff --git a/ports/z3/fix_cmake_long_dir.patch b/ports/z3/fix_cmake_long_dir.patch new file mode 100644 index 000000000..f7dc505d6 --- /dev/null +++ b/ports/z3/fix_cmake_long_dir.patch @@ -0,0 +1,61 @@ +diff --git a/cmake/z3_add_component.cmake b/cmake/z3_add_component.cmake +index 8ab6e045d..ac6d1ec06 100644 +--- a/cmake/z3_add_component.cmake ++++ b/cmake/z3_add_component.cmake +@@ -262,18 +262,20 @@ macro(z3_add_install_tactic_rule) + GLOBAL + PROPERTY Z3_${dependency}_TACTIC_HEADERS + ) +- list(APPEND _tactic_header_files ${_component_tactic_header_files}) ++ list(APPEND _tactic_header_files "${_component_tactic_header_files}") + endforeach() + unset(_component_tactic_header_files) + ++ string(REPLACE ";" "\n" _tactic_header_files "${_tactic_header_files}") ++ file(WRITE "${CMAKE_CURRENT_BINARY_DIR}/install_tactic.deps" ${_tactic_header_files}) + add_custom_command(OUTPUT "install_tactic.cpp" + COMMAND "${PYTHON_EXECUTABLE}" + "${CMAKE_SOURCE_DIR}/scripts/mk_install_tactic_cpp.py" + "${CMAKE_CURRENT_BINARY_DIR}" +- ${_tactic_header_files} ++ "${CMAKE_CURRENT_BINARY_DIR}/install_tactic.deps" + DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_install_tactic_cpp.py" + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} +- ${_tactic_header_files} ++ "${CMAKE_CURRENT_BINARY_DIR}/install_tactic.deps" + COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp\"" + ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} + VERBATIM +diff --git a/scripts/mk_install_tactic_cpp.py b/scripts/mk_install_tactic_cpp.py +index a152eff14..b82e71354 100755 +--- a/scripts/mk_install_tactic_cpp.py ++++ b/scripts/mk_install_tactic_cpp.py +@@ -14,19 +14,22 @@ def main(args): + logging.basicConfig(level=logging.INFO) + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("destination_dir", help="destination directory") +- parser.add_argument("header_files", nargs="+", +- help="One or more header files to parse") ++ parser.add_argument("deps", help="file with header file names to parse") + pargs = parser.parse_args(args) + + if not mk_genfile_common.check_dir_exists(pargs.destination_dir): + return 1 + +- if not mk_genfile_common.check_files_exist(pargs.header_files): ++ if not mk_genfile_common.check_files_exist([pargs.deps]): + return 1 + +- h_files_full_path = [] +- for header_file in pargs.header_files: +- h_files_full_path.append(os.path.abspath(header_file)) ++ with open(pargs.deps, 'r') as f: ++ lines = f.read().split('\n') ++ h_files_full_path = [os.path.abspath(header_file) ++ for header_file in lines if header_file] ++ ++ if not mk_genfile_common.check_files_exist(h_files_full_path): ++ return 1 + + output = mk_genfile_common.mk_install_tactic_cpp_internal( + h_files_full_path, diff --git a/ports/z3/portfile.cmake b/ports/z3/portfile.cmake new file mode 100644 index 000000000..46182793d --- /dev/null +++ b/ports/z3/portfile.cmake @@ -0,0 +1,63 @@ +if (VCPKG_TARGET_ARCHITECTURE STREQUAL "arm64") + message(FATAL_ERROR "Z3 doesn't currently support ARM64") +endif() + +if (VCPKG_CMAKE_SYSTEM_NAME STREQUAL "WindowsStore") + message(FATAL_ERROR "Z3 doesn't currently support UWP") +endif() + +include(vcpkg_common_functions) + +vcpkg_find_acquire_program(PYTHON2) +get_filename_component(PYTHON2_DIR "${PYTHON2}" DIRECTORY) +vcpkg_add_to_path("${PYTHON2_DIR}") + +vcpkg_from_github( + OUT_SOURCE_PATH SOURCE_PATH + REPO Z3Prover/z3 + REF z3-4.8.4 + SHA512 4660ba6ab33a6345b2e8396c332d4afcfc73eda66ceb2595a39f152df4d62a9ea0f349b0f9212389ba84ecba6bdae6ad9b62b376ba44dc4d9c74f80d7a818bf4 + HEAD_REF master + PATCHES fix_cmake_long_dir.patch +) + +if (VCPKG_LIBRARY_LINKAGE STREQUAL "static") + set(BUILD_STATIC "-DBUILD_LIBZ3_SHARED=OFF") +endif() + +vcpkg_configure_cmake( + SOURCE_PATH ${SOURCE_PATH} + PREFER_NINJA + OPTIONS + ${BUILD_STATIC} +) + +vcpkg_build_cmake() + + +function(install_z3 SHORT_BUILDTYPE DEBUG_DIR) + set(LIBS ".so" ".lib" ".dylib" ".a") + set(DLLS ".dll" ".pdb") + file(GLOB FILES ${CURRENT_BUILDTREES_DIR}/${TARGET_TRIPLET}-${SHORT_BUILDTYPE}/libz3.*) + + foreach (FILE in ${FILES}) + get_filename_component(FILEXT ${FILE} EXT) + if ("${FILEXT}" IN_LIST LIBS) + file(INSTALL ${FILE} DESTINATION ${CURRENT_PACKAGES_DIR}${DEBUG_DIR}/lib) + elseif ("${FILEXT}" IN_LIST DLLS) + file(INSTALL ${FILE} DESTINATION ${CURRENT_PACKAGES_DIR}${DEBUG_DIR}/bin) + endif() + endforeach() +endfunction() + +if (NOT DEFINED VCPKG_BUILD_TYPE OR VCPKG_BUILD_TYPE STREQUAL "release") + install_z3("dbg" "/debug") +endif() +if (NOT DEFINED VCPKG_BUILD_TYPE OR VCPKG_BUILD_TYPE STREQUAL "debug") + install_z3("rel" "") +endif() + +file(GLOB HEADERS ${SOURCE_PATH}/src/api/z3*.h) +file(INSTALL ${HEADERS} DESTINATION ${CURRENT_PACKAGES_DIR}/include) + +file(INSTALL ${SOURCE_PATH}/LICENSE.txt DESTINATION ${CURRENT_PACKAGES_DIR}/share/z3 RENAME copyright)