From d87015b18670336a75b94da76e6b47bf8858bbf5 Mon Sep 17 00:00:00 2001 From: Anonymous Maarten Date: Sat, 25 Apr 2020 05:25:52 +0200 Subject: [PATCH 1/9] z3: add z3/4.8.7 recipe --- recipes/z3/all/CMakeLists.txt | 7 + recipes/z3/all/conandata.yml | 4 + recipes/z3/all/conanfile.py | 78 +++++++++++ recipes/z3/all/test_package/CMakeLists.txt | 10 ++ recipes/z3/all/test_package/conanfile.py | 17 +++ recipes/z3/all/test_package/test_package.c | 144 +++++++++++++++++++++ recipes/z3/config.yml | 3 + 7 files changed, 263 insertions(+) create mode 100644 recipes/z3/all/CMakeLists.txt create mode 100644 recipes/z3/all/conandata.yml create mode 100644 recipes/z3/all/conanfile.py create mode 100644 recipes/z3/all/test_package/CMakeLists.txt create mode 100644 recipes/z3/all/test_package/conanfile.py create mode 100644 recipes/z3/all/test_package/test_package.c create mode 100644 recipes/z3/config.yml diff --git a/recipes/z3/all/CMakeLists.txt b/recipes/z3/all/CMakeLists.txt new file mode 100644 index 0000000000000..a69305eb3971f --- /dev/null +++ b/recipes/z3/all/CMakeLists.txt @@ -0,0 +1,7 @@ +cmake_minimum_required(VERSION 2.8.12) +project(cmake_wrapper) + +include(conanbuildinfo.cmake) +conan_basic_setup() + +add_subdirectory(source_subfolder) diff --git a/recipes/z3/all/conandata.yml b/recipes/z3/all/conandata.yml new file mode 100644 index 0000000000000..03b571cecacc4 --- /dev/null +++ b/recipes/z3/all/conandata.yml @@ -0,0 +1,4 @@ +sources: + "4.8.7": + url: "https://github.com/Z3Prover/z3/archive/z3-4.8.7.tar.gz" + sha256: "8c1c49a1eccf5d8b952dadadba3552b0eac67482b8a29eaad62aa7343a0732c3" diff --git a/recipes/z3/all/conanfile.py b/recipes/z3/all/conanfile.py new file mode 100644 index 0000000000000..2dad27f1b0d19 --- /dev/null +++ b/recipes/z3/all/conanfile.py @@ -0,0 +1,78 @@ +from conans import CMake, ConanFile, tools +import os + + +class Z3Conan(ConanFile): + name = "z3" + description = "The Z3 Theorem Prover" + topics = ("conan", "z3", "theorem", "SMT", "satisfiability", "prover", "solver") + url = "https://github.com/conan-io/conan-center-index" + homepage = "https://github.com/Z3Prover/z3" + exports_sources = "CMakeLists.txt" + generators = "cmake" + license = "MIT" + settings = "os", "arch", "compiler", "build_type" + options = { + "shared": [True, False], + "fPIC": [True, False], + "multithreaded": [True, False], + } + default_options = { + "shared": False, + "fPIC": True, + "multithreaded": True, + } + + _cmake = None + + @property + def _source_subfolder(self): + return "source_subfolder" + + @property + def _build_subfolder(self): + return "build_subfolder" + + def config_options(self): + if self.settings.os == "Windows": + del self.options.fPIC + + def configure(self): + if self.options.shared: + del self.options.fPIC + + def requirements(self): + self.requires("mpir/3.0.0") + + def source(self): + tools.get(**self.conan_data["sources"][self.version]) + os.rename("{0}-{0}-{1}".format(self.name, self.version), self._source_subfolder) + + def _configure_cmake(self): + if self._cmake: + return self._cmake + self._cmake = CMake(self) + self._cmake.definitions["Z3_USE_LIB_GMP"] = True + self._cmake.definitions["SINGLE_THREADED"] = not self.options.multithreaded + self._cmake.definitions["Z3_BUILD_LIBZ3_SHARED"] = self.options.shared + self._cmake.definitions["Z3_INCLUDE_GIT_HASH"] = False + self._cmake.definitions["Z3_INCLUDE_GIT_DESCRIBE"] = False + self._cmake.definitions["Z3_ENABLE_EXAMPLE_TARGETS"] = False + self._cmake.definitions["Z3_BUILD_DOCUMENTATION"] = False + self._cmake.configure(build_folder=self._build_subfolder) + return self._cmake + + def build(self): + cmake = self._configure_cmake() + cmake.build() + + def package(self): + self.copy("LICENSE.txt", src=self._source_subfolder, dst="licenses") + cmake = self._configure_cmake() + cmake.install() + + def package_info(self): + self.cpp_info.libs = ["libz3"] + # FIXME: name of imported CMake target is z3::libz3 (no capitals) + self.cpp_info.names["cmake_find_package"] = "Z3" + self.cpp_info.names["cmake_find_package_multi"] = "Z3" diff --git a/recipes/z3/all/test_package/CMakeLists.txt b/recipes/z3/all/test_package/CMakeLists.txt new file mode 100644 index 0000000000000..2653136b1d808 --- /dev/null +++ b/recipes/z3/all/test_package/CMakeLists.txt @@ -0,0 +1,10 @@ +cmake_minimum_required(VERSION 2.8.12) +project(test_package) + +set(CMAKE_VERBOSE_MAKEFILE TRUE) + +include(${CMAKE_BINARY_DIR}/conanbuildinfo.cmake) +conan_basic_setup() + +add_executable(${PROJECT_NAME} test_package.c) +target_link_libraries(${PROJECT_NAME} ${CONAN_LIBS}) diff --git a/recipes/z3/all/test_package/conanfile.py b/recipes/z3/all/test_package/conanfile.py new file mode 100644 index 0000000000000..bd7165a553cf4 --- /dev/null +++ b/recipes/z3/all/test_package/conanfile.py @@ -0,0 +1,17 @@ +from conans import ConanFile, CMake, tools +import os + + +class TestPackageConan(ConanFile): + settings = "os", "compiler", "build_type", "arch" + generators = "cmake" + + def build(self): + cmake = CMake(self) + cmake.configure() + cmake.build() + + def test(self): + if not tools.cross_building(self.settings): + bin_path = os.path.join("bin", "test_package") + self.run(bin_path, run_environment=True) diff --git a/recipes/z3/all/test_package/test_package.c b/recipes/z3/all/test_package/test_package.c new file mode 100644 index 0000000000000..f2edd106bb1f5 --- /dev/null +++ b/recipes/z3/all/test_package/test_package.c @@ -0,0 +1,144 @@ +#include "z3.h" + +#include + +/* Adapted from z3/examples/c/test_capi.c */ + +/** + \brief Simpler error handler. + */ +static void error_handler(Z3_context c, Z3_error_code e) +{ + fprintf(stderr, "Error code: %d\n", e); + fprintf(stderr, "incorrect use of Z3\n"); + exit(1); +} + +/** + \brief Create a logical context. + + Enable model construction. Other configuration parameters can be passed in the cfg variable. + + Also enable tracing to stderr and register custom error handler. +*/ +static Z3_context mk_context_custom(Z3_config cfg, Z3_error_handler err) +{ + Z3_context ctx; + + Z3_set_param_value(cfg, "model", "true"); + ctx = Z3_mk_context(cfg); + Z3_set_error_handler(ctx, err); + + return ctx; +} + +/** + \brief Create a logical context. + + Enable model construction only. + + Also enable tracing to stderr and register standard error handler. +*/ +static Z3_context mk_context() +{ + Z3_config cfg; + Z3_context ctx; + cfg = Z3_mk_config(); + ctx = mk_context_custom(cfg, error_handler); + Z3_del_config(cfg); + return ctx; +} + +Z3_solver mk_solver(Z3_context ctx) +{ + Z3_solver s = Z3_mk_solver(ctx); + Z3_solver_inc_ref(ctx, s); + return s; +} + +static void del_solver(Z3_context ctx, Z3_solver s) +{ + Z3_solver_dec_ref(ctx, s); +} + +/** + @name Examples +*/ +/*@{*/ +/** + \brief "Hello world" example: create a Z3 logical context, and delete it. +*/ +void simple_example() +{ + Z3_context ctx; + printf("\nsimple_example\n"); + + ctx = mk_context(); + + /* delete logical context */ + Z3_del_context(ctx); +} + +/** + Demonstration of how Z3 can be used to prove validity of + De Morgan's Duality Law: {e not(x and y) <-> (not x) or ( not y) } +*/ +void demorgan() +{ + Z3_config cfg; + Z3_context ctx; + Z3_solver s; + Z3_sort bool_sort; + Z3_symbol symbol_x, symbol_y; + Z3_ast x, y, not_x, not_y, x_and_y, ls, rs, conjecture, negated_conjecture; + Z3_ast args[2]; + + printf("\nDeMorgan\n"); + + cfg = Z3_mk_config(); + ctx = Z3_mk_context(cfg); + Z3_del_config(cfg); + bool_sort = Z3_mk_bool_sort(ctx); + symbol_x = Z3_mk_int_symbol(ctx, 0); + symbol_y = Z3_mk_int_symbol(ctx, 1); + x = Z3_mk_const(ctx, symbol_x, bool_sort); + y = Z3_mk_const(ctx, symbol_y, bool_sort); + + /* De Morgan - with a negation around */ + /* !(!(x && y) <-> (!x || !y)) */ + not_x = Z3_mk_not(ctx, x); + not_y = Z3_mk_not(ctx, y); + args[0] = x; + args[1] = y; + x_and_y = Z3_mk_and(ctx, 2, args); + ls = Z3_mk_not(ctx, x_and_y); + args[0] = not_x; + args[1] = not_y; + rs = Z3_mk_or(ctx, 2, args); + conjecture = Z3_mk_iff(ctx, ls, rs); + negated_conjecture = Z3_mk_not(ctx, conjecture); + + s = mk_solver(ctx); + Z3_solver_assert(ctx, s, negated_conjecture); + switch (Z3_solver_check(ctx, s)) { + case Z3_L_FALSE: + /* The negated conjecture was unsatisfiable, hence the conjecture is valid */ + printf("DeMorgan is valid\n"); + break; + case Z3_L_UNDEF: + /* Check returned undef */ + printf("Undef\n"); + break; + case Z3_L_TRUE: + /* The negated conjecture was satisfiable, hence the conjecture is not valid */ + printf("DeMorgan is not valid\n"); + break; + } + del_solver(ctx, s); + Z3_del_context(ctx); +} + +int main() { + simple_example(); + demorgan(); +} diff --git a/recipes/z3/config.yml b/recipes/z3/config.yml new file mode 100644 index 0000000000000..f26e613872b7c --- /dev/null +++ b/recipes/z3/config.yml @@ -0,0 +1,3 @@ +versions: + "4.8.7": + folder: "all" From 485010332417cc485f4990303dbfd50499696f0c Mon Sep 17 00:00:00 2001 From: Anonymous Maarten Date: Sat, 25 Apr 2020 21:27:44 +0200 Subject: [PATCH 2/9] z3: compile test_package as c++ + add pthread + remove cmake dirs --- recipes/z3/all/conanfile.py | 7 ++++++- recipes/z3/all/test_package/CMakeLists.txt | 2 +- .../all/test_package/{test_package.c => test_package.cpp} | 3 ++- 3 files changed, 9 insertions(+), 3 deletions(-) rename recipes/z3/all/test_package/{test_package.c => test_package.cpp} (98%) diff --git a/recipes/z3/all/conanfile.py b/recipes/z3/all/conanfile.py index 2dad27f1b0d19..878f395b9d4a1 100644 --- a/recipes/z3/all/conanfile.py +++ b/recipes/z3/all/conanfile.py @@ -71,8 +71,13 @@ def package(self): cmake = self._configure_cmake() cmake.install() + tools.rmdir(os.path.join(self.package_folder, "lib", "cmake")) + def package_info(self): - self.cpp_info.libs = ["libz3"] + self.cpp_info.libs = ["libz3" if self.settings.os == "Windows" else "z3"] + if self.settings.os in ("Linux",): + self.cpp_info.system_libs.append("pthread") + # FIXME: name of imported CMake target is z3::libz3 (no capitals) self.cpp_info.names["cmake_find_package"] = "Z3" self.cpp_info.names["cmake_find_package_multi"] = "Z3" diff --git a/recipes/z3/all/test_package/CMakeLists.txt b/recipes/z3/all/test_package/CMakeLists.txt index 2653136b1d808..56a1bba89a19d 100644 --- a/recipes/z3/all/test_package/CMakeLists.txt +++ b/recipes/z3/all/test_package/CMakeLists.txt @@ -6,5 +6,5 @@ set(CMAKE_VERBOSE_MAKEFILE TRUE) include(${CMAKE_BINARY_DIR}/conanbuildinfo.cmake) conan_basic_setup() -add_executable(${PROJECT_NAME} test_package.c) +add_executable(${PROJECT_NAME} test_package.cpp) target_link_libraries(${PROJECT_NAME} ${CONAN_LIBS}) diff --git a/recipes/z3/all/test_package/test_package.c b/recipes/z3/all/test_package/test_package.cpp similarity index 98% rename from recipes/z3/all/test_package/test_package.c rename to recipes/z3/all/test_package/test_package.cpp index f2edd106bb1f5..952704555d235 100644 --- a/recipes/z3/all/test_package/test_package.c +++ b/recipes/z3/all/test_package/test_package.cpp @@ -1,6 +1,7 @@ #include "z3.h" -#include +#include +#include /* Adapted from z3/examples/c/test_capi.c */ From cc92a49a7db7f46264dabaf3959dedfc9174ff3c Mon Sep 17 00:00:00 2001 From: Anonymous Maarten Date: Sat, 25 Apr 2020 22:18:51 +0200 Subject: [PATCH 3/9] z3: require a shared mpir library --- recipes/z3/all/conanfile.py | 1 + 1 file changed, 1 insertion(+) diff --git a/recipes/z3/all/conanfile.py b/recipes/z3/all/conanfile.py index 878f395b9d4a1..d8aefb74cd184 100644 --- a/recipes/z3/all/conanfile.py +++ b/recipes/z3/all/conanfile.py @@ -21,6 +21,7 @@ class Z3Conan(ConanFile): "shared": False, "fPIC": True, "multithreaded": True, + "mpir:shared": True, # https://github.com/wbhart/mpir/issues/286 } _cmake = None From 7eb4f2f7c1a08aed559dcec5953888be4d5e2f7e Mon Sep 17 00:00:00 2001 From: Anonymous Maarten Date: Tue, 28 Apr 2020 20:20:02 +0200 Subject: [PATCH 4/9] z3: disallow shared mpir dependency and static runtime at the same time --- recipes/z3/all/conanfile.py | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/recipes/z3/all/conanfile.py b/recipes/z3/all/conanfile.py index d8aefb74cd184..72bef0dacac28 100644 --- a/recipes/z3/all/conanfile.py +++ b/recipes/z3/all/conanfile.py @@ -1,4 +1,5 @@ from conans import CMake, ConanFile, tools +from conans.errors import ConanInvalidConfiguration import os @@ -64,6 +65,9 @@ def _configure_cmake(self): return self._cmake def build(self): + if self.settings.compiler == "Visual Studio": + if self.options["mpir"].shared and "MT" in str(self.settings.compiler.runtime): + raise ConanInvalidConfiguration("Cannot link to a shared mpir library and a static {} runtime at the same time".format(self.settings.compiler.runtime)) cmake = self._configure_cmake() cmake.build() From df073543e09328c7bf14e297ba8a7a7cab3154f0 Mon Sep 17 00:00:00 2001 From: Anonymous Maarten Date: Fri, 14 Aug 2020 01:15:27 +0200 Subject: [PATCH 5/9] z3: bump z3 version to 4.8.8 --- recipes/z3/all/CMakeLists.txt | 2 +- recipes/z3/all/conandata.yml | 6 +++--- recipes/z3/all/conanfile.py | 21 ++++++++++++--------- recipes/z3/all/test_package/CMakeLists.txt | 4 +--- recipes/z3/config.yml | 2 +- 5 files changed, 18 insertions(+), 17 deletions(-) diff --git a/recipes/z3/all/CMakeLists.txt b/recipes/z3/all/CMakeLists.txt index a69305eb3971f..bd3083b512cb9 100644 --- a/recipes/z3/all/CMakeLists.txt +++ b/recipes/z3/all/CMakeLists.txt @@ -1,4 +1,4 @@ -cmake_minimum_required(VERSION 2.8.12) +cmake_minimum_required(VERSION 3.1) project(cmake_wrapper) include(conanbuildinfo.cmake) diff --git a/recipes/z3/all/conandata.yml b/recipes/z3/all/conandata.yml index 03b571cecacc4..cfe72a18d1994 100644 --- a/recipes/z3/all/conandata.yml +++ b/recipes/z3/all/conandata.yml @@ -1,4 +1,4 @@ sources: - "4.8.7": - url: "https://github.com/Z3Prover/z3/archive/z3-4.8.7.tar.gz" - sha256: "8c1c49a1eccf5d8b952dadadba3552b0eac67482b8a29eaad62aa7343a0732c3" + "4.8.8": + url: "https://github.com/Z3Prover/z3/archive/z3-4.8.8.tar.gz" + sha256: "6962facdcdea287c5eeb1583debe33ee23043144d0e5308344e6a8ee4503bcff" diff --git a/recipes/z3/all/conanfile.py b/recipes/z3/all/conanfile.py index 72bef0dacac28..173b1296ad3e1 100644 --- a/recipes/z3/all/conanfile.py +++ b/recipes/z3/all/conanfile.py @@ -22,7 +22,6 @@ class Z3Conan(ConanFile): "shared": False, "fPIC": True, "multithreaded": True, - "mpir:shared": True, # https://github.com/wbhart/mpir/issues/286 } _cmake = None @@ -65,9 +64,6 @@ def _configure_cmake(self): return self._cmake def build(self): - if self.settings.compiler == "Visual Studio": - if self.options["mpir"].shared and "MT" in str(self.settings.compiler.runtime): - raise ConanInvalidConfiguration("Cannot link to a shared mpir library and a static {} runtime at the same time".format(self.settings.compiler.runtime)) cmake = self._configure_cmake() cmake.build() @@ -79,10 +75,17 @@ def package(self): tools.rmdir(os.path.join(self.package_folder, "lib", "cmake")) def package_info(self): - self.cpp_info.libs = ["libz3" if self.settings.os == "Windows" else "z3"] - if self.settings.os in ("Linux",): - self.cpp_info.system_libs.append("pthread") - - # FIXME: name of imported CMake target is z3::libz3 (no capitals) + # z3 generates a Z3Config.cmake file self.cpp_info.names["cmake_find_package"] = "Z3" self.cpp_info.names["cmake_find_package_multi"] = "Z3" + + self.cpp_info.components["libz3"].libs = ["libz3" if self.settings.os == "Windows" else "z3"] + self.cpp_info.components["libz3"].requires = ["mpir::mpir"] + # Z3COnfig.cmake generates a z3::libz3 target + self.cpp_info.components["libz3"].names["cmake_find_package"] = "libz3" + self.cpp_info.components["libz3"].names["cmake_find_package_multi"] = "libz3" + if not self.options.shared: + if self.settings.os =="Linux": + self.cpp_info.components.system_libs.append("pthread") + # FIXME: this generates a Z3::libz3 target instead of z3::libz3. + diff --git a/recipes/z3/all/test_package/CMakeLists.txt b/recipes/z3/all/test_package/CMakeLists.txt index 56a1bba89a19d..196188113685c 100644 --- a/recipes/z3/all/test_package/CMakeLists.txt +++ b/recipes/z3/all/test_package/CMakeLists.txt @@ -1,8 +1,6 @@ -cmake_minimum_required(VERSION 2.8.12) +cmake_minimum_required(VERSION 3.1) project(test_package) -set(CMAKE_VERBOSE_MAKEFILE TRUE) - include(${CMAKE_BINARY_DIR}/conanbuildinfo.cmake) conan_basic_setup() diff --git a/recipes/z3/config.yml b/recipes/z3/config.yml index f26e613872b7c..60dbf68790135 100644 --- a/recipes/z3/config.yml +++ b/recipes/z3/config.yml @@ -1,3 +1,3 @@ versions: - "4.8.7": + "4.8.8": folder: "all" From 62693c275d5cb99d8649b39e33472a7c869e96ba Mon Sep 17 00:00:00 2001 From: Anonymous Maarten Date: Fri, 14 Aug 2020 15:33:28 +0200 Subject: [PATCH 6/9] z3: fix error in package_info --- recipes/z3/all/conanfile.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/recipes/z3/all/conanfile.py b/recipes/z3/all/conanfile.py index 173b1296ad3e1..0cb5baf2dd41a 100644 --- a/recipes/z3/all/conanfile.py +++ b/recipes/z3/all/conanfile.py @@ -86,6 +86,6 @@ def package_info(self): self.cpp_info.components["libz3"].names["cmake_find_package_multi"] = "libz3" if not self.options.shared: if self.settings.os =="Linux": - self.cpp_info.components.system_libs.append("pthread") + self.cpp_info.components["libz3"].system_libs.append("pthread") # FIXME: this generates a Z3::libz3 target instead of z3::libz3. From 2bc47dd2ad94ee90c027eb43a066bd3af6bb3deb Mon Sep 17 00:00:00 2001 From: Anonymous Maarten Date: Sat, 15 Aug 2020 00:58:41 +0200 Subject: [PATCH 7/9] z3: patch cmake to use mpir --- recipes/z3/all/CMakeLists.txt | 2 +- recipes/z3/all/conandata.yml | 4 ++++ recipes/z3/all/conanfile.py | 10 ++++++++-- .../all/patches/0001-cmake-use-conan-mpir.patch | 16 ++++++++++++++++ 4 files changed, 29 insertions(+), 3 deletions(-) create mode 100644 recipes/z3/all/patches/0001-cmake-use-conan-mpir.patch diff --git a/recipes/z3/all/CMakeLists.txt b/recipes/z3/all/CMakeLists.txt index bd3083b512cb9..e4233e81e86f0 100644 --- a/recipes/z3/all/CMakeLists.txt +++ b/recipes/z3/all/CMakeLists.txt @@ -2,6 +2,6 @@ cmake_minimum_required(VERSION 3.1) project(cmake_wrapper) include(conanbuildinfo.cmake) -conan_basic_setup() +conan_basic_setup(TARGETS) add_subdirectory(source_subfolder) diff --git a/recipes/z3/all/conandata.yml b/recipes/z3/all/conandata.yml index cfe72a18d1994..5970617a4411d 100644 --- a/recipes/z3/all/conandata.yml +++ b/recipes/z3/all/conandata.yml @@ -2,3 +2,7 @@ sources: "4.8.8": url: "https://github.com/Z3Prover/z3/archive/z3-4.8.8.tar.gz" sha256: "6962facdcdea287c5eeb1583debe33ee23043144d0e5308344e6a8ee4503bcff" +patches: + "4.8.8": + - patch_file: "patches/0001-cmake-use-conan-mpir.patch" + base_path: "source_subfolder" diff --git a/recipes/z3/all/conanfile.py b/recipes/z3/all/conanfile.py index 0cb5baf2dd41a..f872457f169b6 100644 --- a/recipes/z3/all/conanfile.py +++ b/recipes/z3/all/conanfile.py @@ -1,6 +1,6 @@ from conans import CMake, ConanFile, tools -from conans.errors import ConanInvalidConfiguration import os +import textwrap class Z3Conan(ConanFile): @@ -9,7 +9,7 @@ class Z3Conan(ConanFile): topics = ("conan", "z3", "theorem", "SMT", "satisfiability", "prover", "solver") url = "https://github.com/conan-io/conan-center-index" homepage = "https://github.com/Z3Prover/z3" - exports_sources = "CMakeLists.txt" + exports_sources = "CMakeLists.txt", "patches/**" generators = "cmake" license = "MIT" settings = "os", "arch", "compiler", "build_type" @@ -64,6 +64,12 @@ def _configure_cmake(self): return self._cmake def build(self): + for patch in self.conan_data.get("patches", {}).get(self.version, []): + tools.patch(**patch) + tools.save(os.path.join(self._build_subfolder, "gmp.h"), textwrap.dedent("""\ + #pragma once + #include + """)) cmake = self._configure_cmake() cmake.build() diff --git a/recipes/z3/all/patches/0001-cmake-use-conan-mpir.patch b/recipes/z3/all/patches/0001-cmake-use-conan-mpir.patch new file mode 100644 index 0000000000000..8b8656042fa3f --- /dev/null +++ b/recipes/z3/all/patches/0001-cmake-use-conan-mpir.patch @@ -0,0 +1,16 @@ +--- CMakeLists.txt ++++ CMakeLists.txt +@@ -246,10 +246,10 @@ + if (Z3_USE_LIB_GMP) + # Because this is off by default we will make the configure fail if libgmp + # can't be found +- find_package(GMP REQUIRED) ++ #find_package(GMP REQUIRED) + message(STATUS "Using libgmp") +- list(APPEND Z3_DEPENDENT_LIBS ${GMP_C_LIBRARIES}) +- list(APPEND Z3_COMPONENT_EXTRA_INCLUDE_DIRS ${GMP_INCLUDE_DIRS}) ++ list(APPEND Z3_DEPENDENT_LIBS CONAN_PKG::mpir) ++ list(APPEND Z3_COMPONENT_EXTRA_INCLUDE_DIRS "${CMAKE_BINARY_DIR}" ${CONAN_INCLUDE_DIRS}) + list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_MP_GMP") + else() + list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_MP_INTERNAL") From 4fce55708c7f86610f5caab3ce8cc211487e7d17 Mon Sep 17 00:00:00 2001 From: Anonymous Maarten Date: Tue, 18 Aug 2020 14:47:50 +0200 Subject: [PATCH 8/9] z3: create correct imported target in correct filename for generator --- recipes/z3/all/conanfile.py | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/recipes/z3/all/conanfile.py b/recipes/z3/all/conanfile.py index f872457f169b6..bc60bbe1437d0 100644 --- a/recipes/z3/all/conanfile.py +++ b/recipes/z3/all/conanfile.py @@ -82,16 +82,17 @@ def package(self): def package_info(self): # z3 generates a Z3Config.cmake file - self.cpp_info.names["cmake_find_package"] = "Z3" - self.cpp_info.names["cmake_find_package_multi"] = "Z3" + self.cpp_info.names["cmake_find_package"] = "z3" + self.cpp_info.names["cmake_find_package_multi"] = "z3" self.cpp_info.components["libz3"].libs = ["libz3" if self.settings.os == "Windows" else "z3"] self.cpp_info.components["libz3"].requires = ["mpir::mpir"] # Z3COnfig.cmake generates a z3::libz3 target self.cpp_info.components["libz3"].names["cmake_find_package"] = "libz3" self.cpp_info.components["libz3"].names["cmake_find_package_multi"] = "libz3" + self.cpp_info.components["libz3"].filenames["cmake_find_package"] = "Z3" + self.cpp_info.components["libz3"].filenames["cmake_find_package_multi"] = "Z3" if not self.options.shared: if self.settings.os =="Linux": self.cpp_info.components["libz3"].system_libs.append("pthread") # FIXME: this generates a Z3::libz3 target instead of z3::libz3. - From 51c3420f43c40302dd952fb52a81076fb1b03116 Mon Sep 17 00:00:00 2001 From: Anonymous Maarten Date: Tue, 18 Aug 2020 18:18:35 +0200 Subject: [PATCH 9/9] z3: self.cpp_info.components[..].filenames does not exist + test exported target Co-authored-by: Javier G. Sogo --- recipes/z3/all/conanfile.py | 4 ++-- recipes/z3/all/test_package/CMakeLists.txt | 6 ++++-- recipes/z3/all/test_package/conanfile.py | 2 +- 3 files changed, 7 insertions(+), 5 deletions(-) diff --git a/recipes/z3/all/conanfile.py b/recipes/z3/all/conanfile.py index bc60bbe1437d0..d2348a4fb9164 100644 --- a/recipes/z3/all/conanfile.py +++ b/recipes/z3/all/conanfile.py @@ -84,14 +84,14 @@ def package_info(self): # z3 generates a Z3Config.cmake file self.cpp_info.names["cmake_find_package"] = "z3" self.cpp_info.names["cmake_find_package_multi"] = "z3" + self.cpp_info.filenames["cmake_find_package"] = "Z3" + self.cpp_info.filenames["cmake_find_package_multi"] = "Z3" self.cpp_info.components["libz3"].libs = ["libz3" if self.settings.os == "Windows" else "z3"] self.cpp_info.components["libz3"].requires = ["mpir::mpir"] # Z3COnfig.cmake generates a z3::libz3 target self.cpp_info.components["libz3"].names["cmake_find_package"] = "libz3" self.cpp_info.components["libz3"].names["cmake_find_package_multi"] = "libz3" - self.cpp_info.components["libz3"].filenames["cmake_find_package"] = "Z3" - self.cpp_info.components["libz3"].filenames["cmake_find_package_multi"] = "Z3" if not self.options.shared: if self.settings.os =="Linux": self.cpp_info.components["libz3"].system_libs.append("pthread") diff --git a/recipes/z3/all/test_package/CMakeLists.txt b/recipes/z3/all/test_package/CMakeLists.txt index 196188113685c..a54155858a95e 100644 --- a/recipes/z3/all/test_package/CMakeLists.txt +++ b/recipes/z3/all/test_package/CMakeLists.txt @@ -2,7 +2,9 @@ cmake_minimum_required(VERSION 3.1) project(test_package) include(${CMAKE_BINARY_DIR}/conanbuildinfo.cmake) -conan_basic_setup() +conan_basic_setup(TARGETS) + +find_package(Z3 REQUIRED) add_executable(${PROJECT_NAME} test_package.cpp) -target_link_libraries(${PROJECT_NAME} ${CONAN_LIBS}) +target_link_libraries(${PROJECT_NAME} PRIVATE z3::libz3) diff --git a/recipes/z3/all/test_package/conanfile.py b/recipes/z3/all/test_package/conanfile.py index bd7165a553cf4..1d0bdd3779793 100644 --- a/recipes/z3/all/test_package/conanfile.py +++ b/recipes/z3/all/test_package/conanfile.py @@ -4,7 +4,7 @@ class TestPackageConan(ConanFile): settings = "os", "compiler", "build_type", "arch" - generators = "cmake" + generators = "cmake", "cmake_find_package" def build(self): cmake = CMake(self)