commit: 0165d1484b0c9ad0f2272960c80703e2c0b231f2 Author: Tupone Alfredo <tupone <AT> gentoo <DOT> org> AuthorDate: Sun Jul 14 19:48:18 2019 +0000 Commit: Alfredo Tupone <tupone <AT> gentoo <DOT> org> CommitDate: Sun Jul 14 19:48:18 2019 +0000 URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=0165d148
sci-mathematics/cvc4: Bump to 1.7 Closes: https://bugs.gentoo.org/688652 Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org> Package-Manager: Portage-2.3.66, Repoman-2.3.11 sci-mathematics/cvc4/Manifest | 1 + sci-mathematics/cvc4/cvc4-1.7.ebuild | 54 ++++++++++++++++++++++++ sci-mathematics/cvc4/files/cvc4-1.7-gentoo.patch | 35 +++++++++++++++ 3 files changed, 90 insertions(+) diff --git a/sci-mathematics/cvc4/Manifest b/sci-mathematics/cvc4/Manifest index 2b268f2188b..daaafcc4d44 100644 --- a/sci-mathematics/cvc4/Manifest +++ b/sci-mathematics/cvc4/Manifest @@ -1 +1,2 @@ DIST cvc4-1.6.tar.gz 7815893 BLAKE2B 626e0dd49f911384e64d7e8ecf635aa12dad32830b2032bdcb96afd1a17c3566f56df51f75e9193cf365b562855733d0ea4ff3311ac99fc86e928a956298d2ad SHA512 0887b3f74a4b9e51e634591c7cf39d730110ca5d930149bab4816a49e383eeea8ccadf8474d22f5529cc03ddd045acacf8a2b92434b882adf352f4de4075fcd4 +DIST cvc4-1.7.tar.gz 6969953 BLAKE2B 3a64db14a734e0314fb7d7b8dbed79e067c9bbf1723343dac1e9c47b3f09811b1a32ff0116412667bd0afefda2489c6c1679bf109710402a67bee0d91b62dd94 SHA512 b91dfac7ddf979a3474f562eb98f2d6f17a53efa38c1be5502429309a0c059e1f2b0d85ee95e5aee17d35f34c825f01f879ec4aaf26025b1fcac835c33a867c6 diff --git a/sci-mathematics/cvc4/cvc4-1.7.ebuild b/sci-mathematics/cvc4/cvc4-1.7.ebuild new file mode 100644 index 00000000000..0b192f12739 --- /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 00000000000..849b4a8a429 --- /dev/null +++ b/sci-mathematics/cvc4/files/cvc4-1.7-gentoo.patch @@ -0,0 +1,35 @@ +--- 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 + )
