summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAlfredo Tupone <tupone@gentoo.org>2021-05-27 18:45:43 +0200
committerAlfredo Tupone <tupone@gentoo.org>2021-05-27 18:45:43 +0200
commitf156562b157e5e59722065a39c5264413fcde2f1 (patch)
tree582f1605bcd0c0aa6fe302e38469ac73d730c5a0 /sci-mathematics/cvc4
parentsys-auth/solo-python: support python3_10 (diff)
downloadgentoo-f156562b157e5e59722065a39c5264413fcde2f1.tar.gz
gentoo-f156562b157e5e59722065a39c5264413fcde2f1.tar.bz2
gentoo-f156562b157e5e59722065a39c5264413fcde2f1.zip
sci-mathematics/cvc4: version bump to 1.8
Package-Manager: Portage-3.0.18, Repoman-3.0.2 Signed-off-by: Alfredo Tupone <tupone@gentoo.org>
Diffstat (limited to 'sci-mathematics/cvc4')
-rw-r--r--sci-mathematics/cvc4/Manifest1
-rw-r--r--sci-mathematics/cvc4/cvc4-1.8.ebuild55
-rw-r--r--sci-mathematics/cvc4/files/cvc4-1.8-gentoo.patch42
3 files changed, 98 insertions, 0 deletions
diff --git a/sci-mathematics/cvc4/Manifest b/sci-mathematics/cvc4/Manifest
index bf26cdb9e5e1..fe5e434767b8 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 000000000000..347dbda0a248
--- /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 000000000000..372bea03fb72
--- /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})")