gentoo resync : 19.07.2019

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})")