[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/cvc4/files/, sci-mathematics/cvc4/

[Alfredo Tupone]

commit:     f156562b157e5e59722065a39c5264413fcde2f1
Author:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
AuthorDate: Thu May 27 16:45:43 2021 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Thu May 27 16:45:43 2021 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=f156562b

sci-mathematics/cvc4: version bump to 1.8

Package-Manager: Portage-3.0.18, Repoman-3.0.2
Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>

 sci-mathematics/cvc4/Manifest                    |  1 +
 sci-mathematics/cvc4/cvc4-1.8.ebuild             | 55 ++++++++++++++++++++++++
 sci-mathematics/cvc4/files/cvc4-1.8-gentoo.patch | 42 ++++++++++++++++++
 3 files changed, 98 insertions(+)

diff --git a/sci-mathematics/cvc4/Manifest b/sci-mathematics/cvc4/Manifest
index bf26cdb9e5e..fe5e434767b 100644
--- a/sci-mathematics/cvc4/Manifest
+++ b/sci-mathematics/cvc4/Manifest
@@ -1 +1,2 @@
 DIST cvc4-1.7.tar.gz 6969953 BLAKE2B 3a64db14a734e0314fb7d7b8dbed79e067c9bbf1723343dac1e9c47b3f09811b1a32ff0116412667bd0afefda2489c6c1679bf109710402a67bee0d91b62dd94 SHA512 b91dfac7ddf979a3474f562eb98f2d6f17a53efa38c1be5502429309a0c059e1f2b0d85ee95e5aee17d35f34c825f01f879ec4aaf26025b1fcac835c33a867c6
+DIST cvc4-1.8.tar.gz 7554297 BLAKE2B f4d2b223ba2c01ef745520d8874381a1873358fbc7eca12559656512ffeefccec4eca3d73a26debf34110ca14a3bccf35ca87e2a49575b8b67484bed79df081c SHA512 d6b0153b0f5c4e615c995a8eecfbfd783cfc1004c5134c6880230044081c71d638fee39cceb987eb8d72e91b2b6596b184dc0daacec8880cfc176c6dee8aa445

diff --git a/sci-mathematics/cvc4/cvc4-1.8.ebuild b/sci-mathematics/cvc4/cvc4-1.8.ebuild
new file mode 100644
index 00000000000..347dbda0a24
--- /dev/null
+++ b/sci-mathematics/cvc4/cvc4-1.8.ebuild
@@ -0,0 +1,55 @@
+# Copyright 1999-2021 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=7
+
+CMAKE_MAKEFILE_GENERATOR=emake
+PYTHON_COMPAT=( python3_{7,8,9} )
+inherit cmake python-any-r1
+
+DESCRIPTION="Automatic theorem prover for satisfiability modulo theories (SMT) problems"
+HOMEPAGE="https://cvc4.github.io/"
+SRC_URI="https://github.com/CVC4/CVC4-archived/archive/refs/tags/${PV}.tar.gz -> ${P}.tar.gz"
+
+LICENSE="GPL-2"
+SLOT="0"
+KEYWORDS="~amd64 ~x86"
+IUSE="+cln proofs readline replay +statistics"
+
+RDEPEND="dev-libs/antlr-c
+	dev-java/antlr:3
+	dev-libs/boost
+	readline? ( sys-libs/readline:0= )
+	cln? ( sci-libs/cln )
+	!cln? ( dev-libs/gmp:= )"
+DEPEND="${RDEPEND}"
+BDEPEND="${PYTHON_DEPS}"
+
+S="${WORKDIR}"/${PN^^}-archived-${PV}
+
+PATCHES=( "${FILESDIR}"/${P}-gentoo.patch )
+
+src_configure() {
+	local mycmakeargs=(
+		-DANTLR_BINARY=/usr/bin/antlr3
+		-DENABLE_GPL=ON
+		-DENABLE_OPTIMIZED=ON
+		-DUSE_CLN="$(usex cln ON OFF)"
+		-DUSE_READLINE="$(usex readline ON OFF)"
+		-DENABLE_STATISTICS="$(usex statistics ON OFF)"
+		-DENABLE_PROOFS="$(usex proofs ON OFF)"
+		-DENABLE_REPLAY="$(usex replay ON OFF)"
+	)
+	cmake_src_configure
+}
+
+src_test() {
+	emake -C "${BUILD_DIR}" \
+		systemtests
+	cmake_src_test
+}
+
+src_install() {
+	cmake_src_install
+	mv "${D}"/usr/{lib,$(get_libdir)}
+}

diff --git a/sci-mathematics/cvc4/files/cvc4-1.8-gentoo.patch b/sci-mathematics/cvc4/files/cvc4-1.8-gentoo.patch
new file mode 100644
index 00000000000..372bea03fb7
--- /dev/null
+++ b/sci-mathematics/cvc4/files/cvc4-1.8-gentoo.patch
@@ -0,0 +1,42 @@
+--- 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
+@@ -2155,7 +2155,6 @@
+   regress4/C880mul.miter.shuffled-as.sat03-348.smtv1.smt2
+   regress4/NEQ016_size5.smtv1.smt2
+   regress4/bug143.smtv1.smt2
+-  regress4/comb2.shuffled-as.sat03-420.smtv1.smt2
+   regress4/hole10.cvc
+   regress4/instance_1151.smtv1.smt2
+ )
+--- 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})")