diff options
author | V3n3RiX <venerix@redcorelinux.org> | 2019-07-19 22:05:27 +0100 |
---|---|---|
committer | V3n3RiX <venerix@redcorelinux.org> | 2019-07-19 22:05:27 +0100 |
commit | 121ed4eec41fbf03e1998d09eede1bf449da63b9 (patch) | |
tree | ce9341d77d1507f67d4a3a1472da9011b5baa0a8 /sci-mathematics/cvc4 | |
parent | dd762ff83c330186ee2ede002e08b2f780cddd51 (diff) |
gentoo resync : 19.07.2019
Diffstat (limited to 'sci-mathematics/cvc4')
-rw-r--r-- | sci-mathematics/cvc4/Manifest | 3 | ||||
-rw-r--r-- | sci-mathematics/cvc4/cvc4-1.7.ebuild | 54 | ||||
-rw-r--r-- | sci-mathematics/cvc4/files/cvc4-1.7-gentoo.patch | 43 |
3 files changed, 100 insertions, 0 deletions
diff --git a/sci-mathematics/cvc4/Manifest b/sci-mathematics/cvc4/Manifest index 364d3cb09511..5a86e7bb1ddf 100644 --- a/sci-mathematics/cvc4/Manifest +++ b/sci-mathematics/cvc4/Manifest @@ -1,3 +1,6 @@ +AUX cvc4-1.7-gentoo.patch 1665 BLAKE2B db98e67fb3b152e0c78019b21b32c99d06377f1b1c1cc6a3ac2edea5e27d6f8ba082fc209c3694e1144a94d9d3b1897418af250252ff40a26e521bbf72d7da0f SHA512 b6b7af8c48c0398375343c8fa72f3e15d8f9031848cf94e6e2880f04b5e8d695691dcf67b84daa1706464289f7db0300046af4c93adcf278f7951eccc734af89 DIST cvc4-1.6.tar.gz 7815893 BLAKE2B 626e0dd49f911384e64d7e8ecf635aa12dad32830b2032bdcb96afd1a17c3566f56df51f75e9193cf365b562855733d0ea4ff3311ac99fc86e928a956298d2ad SHA512 0887b3f74a4b9e51e634591c7cf39d730110ca5d930149bab4816a49e383eeea8ccadf8474d22f5529cc03ddd045acacf8a2b92434b882adf352f4de4075fcd4 +DIST cvc4-1.7.tar.gz 6969953 BLAKE2B 3a64db14a734e0314fb7d7b8dbed79e067c9bbf1723343dac1e9c47b3f09811b1a32ff0116412667bd0afefda2489c6c1679bf109710402a67bee0d91b62dd94 SHA512 b91dfac7ddf979a3474f562eb98f2d6f17a53efa38c1be5502429309a0c059e1f2b0d85ee95e5aee17d35f34c825f01f879ec4aaf26025b1fcac835c33a867c6 EBUILD cvc4-1.6.ebuild 556 BLAKE2B 2943590af801614ea64b26ff72ee9d445c544dacc62b93428c60e8e80a8fea9884f646d3d3680c89d246c34f42215998aadbc39618ee5334d5ee3503e179543b SHA512 bd9ed1c3e2c635ba47667d77fb0929a2681ec6bc09570e74b0e093b76208746e804b7dd04852bb00c44d3b69f31385346ab838ef8e058d701eaf2dd5aabe4d17 +EBUILD cvc4-1.7.ebuild 1072 BLAKE2B f310aefde818c98368dc49cd6ab03c86d64984b3048ef508f2da8b13457e5574eecd32aa595b3cded6918702878afca2baadf30240f141385e4fbc88d4292cb3 SHA512 b731c2b4895167ab9f02ba3120294f964825361fabed861b8692006b317c376eeaca55e21b7ba45404d861f0f33146df685687f9be37e2aa28750ee564b9060e MISC metadata.xml 635 BLAKE2B 96c8a55b5e69e6f52bb5b66ac46361b07bee92c72216d73837a4644ea139b3fc9375f8e8ca68db04975675d6520d7275c02c0cfd27957c77b3506e90b332cc8d SHA512 166da2a33b4d8d33ee237d6175973e382399e1864317fd585395f1f3c78b1487ef4e95c866bfc8e9928fc10f648c45b6f95d0803b608cd8a8b9040c1054f2538 diff --git a/sci-mathematics/cvc4/cvc4-1.7.ebuild b/sci-mathematics/cvc4/cvc4-1.7.ebuild new file mode 100644 index 000000000000..0b192f127391 --- /dev/null +++ b/sci-mathematics/cvc4/cvc4-1.7.ebuild @@ -0,0 +1,54 @@ +# Copyright 1999-2019 Gentoo Authors +# Distributed under the terms of the GNU General Public License v2 + +EAPI=7 + +inherit cmake-utils + +DESCRIPTION="automatic theorem prover for satisfiability modulo theories (SMT) problems" +HOMEPAGE="http://cvc4.cs.stanford.edu/web/" +SRC_URI="https://github.com/CVC4/CVC4/archive/${PV}.tar.gz -> ${P}.tar.gz" + +LICENSE="GPL-2" +SLOT="0" +KEYWORDS="~amd64 ~x86" +IUSE="+cln" + +RDEPEND="dev-libs/antlr-c + dev-java/antlr:3 + dev-libs/boost + cln? ( sci-libs/cln ) + !cln? ( dev-libs/gmp:= )" +DEPEND="${RDEPEND}" + +S="${WORKDIR}"/CVC4-${PV} + +PATCHES=( "${FILESDIR}"/${P}-gentoo.patch ) + +src_configure() { + CMAKE_MAKEFILE_GENERATOR=emake + local mycmakeargs=( + -DANTLR_BINARY=/usr/bin/antlr3 + -DENABLE_GPL=ON + -DUSE_CLN="$(usex cln ON OFF)" + ) + cmake-utils_src_configure +} + +src_test() { + emake -C "${BUILD_DIR}" \ + examples \ + boilerplate \ + ouroborous \ + reset_assertions \ + sep_log_api \ + smt2_compliance \ + two_smt_engines \ + statistics + cmake-utils_src_test +} + +src_install() { + cmake-utils_src_install + mv "${D}"/usr/{lib,$(get_libdir)} +} diff --git a/sci-mathematics/cvc4/files/cvc4-1.7-gentoo.patch b/sci-mathematics/cvc4/files/cvc4-1.7-gentoo.patch new file mode 100644 index 000000000000..55331f6c39b8 --- /dev/null +++ b/sci-mathematics/cvc4/files/cvc4-1.7-gentoo.patch @@ -0,0 +1,43 @@ +--- a/CMakeLists.txt 2019-07-09 14:47:12.552425226 +0200 ++++ b/CMakeLists.txt 2019-07-09 14:50:02.595001358 +0200 +@@ -143,7 +143,7 @@ + + # Note: Module CodeCoverage requires the name of the debug build to conform + # to cmake standards (first letter uppercase). +-set(BUILD_TYPES Production Debug Testing Competition) ++set(BUILD_TYPES Production Debug Testing Competition Gentoo) + + if(ENABLE_ASAN) + #_cmake_modify_IGNORE set(CMAKE_BUILD_TYPE Debug) +@@ -166,12 +166,10 @@ + endif() + + message(STATUS "Building ${CMAKE_BUILD_TYPE} build") +-include(Config${CMAKE_BUILD_TYPE}) + + #-----------------------------------------------------------------------------# + # Compiler flags + +-add_check_c_cxx_flag("-O${OPTIMIZATION_LEVEL}") + add_check_c_cxx_flag("-Wall") + add_check_c_flag("-fexceptions") + add_check_c_cxx_flag("-Wno-deprecated") +--- a/test/regress/CMakeLists.txt 2019-07-14 09:49:38.429990489 +0200 ++++ b/test/regress/CMakeLists.txt 2019-07-14 09:50:28.854234838 +0200 +@@ -1810,7 +1810,7 @@ + regress4/C880mul.miter.shuffled-as.sat03-348.smt + regress4/NEQ016_size5.smt + regress4/bug143.smt +- regress4/comb2.shuffled-as.sat03-420.smt ++ #regress4/comb2.shuffled-as.sat03-420.smt + regress4/hole10.cvc + regress4/instance_1151.smt + ) +--- a/src/CMakeLists.txt 2019-07-18 08:56:47.923025745 +0200 ++++ b/src/CMakeLists.txt 2019-07-18 08:58:10.584750385 +0200 +@@ -915,4 +915,4 @@ + # Note: This is a temporary fix until the new C++ API is in place. + install(CODE "execute_process(COMMAND + ${CMAKE_CURRENT_LIST_DIR}/fix-install-headers.sh +- ${CMAKE_INSTALL_PREFIX})") ++ \$ENV{DESTDIR}${CMAKE_INSTALL_PREFIX})") |