From e30f1a8f185d708ad0b29cac597dc195a7c2d064 Mon Sep 17 00:00:00 2001 From: Maciej Barć Date: Fri, 28 Jun 2024 00:39:22 +0200 Subject: sci-mathematics/stp: bump to 2.3.4 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Signed-off-by: Maciej Barć --- sci-mathematics/stp/Manifest | 1 + sci-mathematics/stp/files/stp-2.3.4-gtest.patch | 26 ++++++ sci-mathematics/stp/files/stp-2.3.4-lit-cfg.patch | 24 +++++ sci-mathematics/stp/stp-2.3.4.ebuild | 109 ++++++++++++++++++++++ 4 files changed, 160 insertions(+) create mode 100644 sci-mathematics/stp/files/stp-2.3.4-gtest.patch create mode 100644 sci-mathematics/stp/files/stp-2.3.4-lit-cfg.patch create mode 100644 sci-mathematics/stp/stp-2.3.4.ebuild (limited to 'sci-mathematics') diff --git a/sci-mathematics/stp/Manifest b/sci-mathematics/stp/Manifest index 0cbd33f52acc..71561cd0b0f9 100644 --- a/sci-mathematics/stp/Manifest +++ b/sci-mathematics/stp/Manifest @@ -1,3 +1,4 @@ DIST stp-2.3.3.tar.gz 2577550 BLAKE2B 9ebedf3cb8e6b50d037cfacbc14826bd4e6505d29a53b1fcc6580749f0637fe5f96619c166babdb3a52b18fb6337e49c02f5693e233effe84d0131d0e7402381 SHA512 a0b1bf419d8230e40ce0aee90d9c8c9d814aca300831c24b3576c75623362942abf20673c419f9f0ea1e0505bfae000dc65fdd818179f5759879b0b255f1b99a DIST stp-2.3.3_OutputCheck.tar.gz 12002 BLAKE2B f8fafba8f7957f3d0ee480b9e1e8c8923c373cf134512d6329adf84a96f3177ad07d00eae4dc6dd8d4b09ca82dfc8b425602f1926e3f88ccb2556b4b7121e5b9 SHA512 36012ae2b2aee1ff3f36ba1678a4bcbfeb590e01c2042ca35eb2f49b6a890b767c1809d1415e7b03f2118204361f834ad9caf70319b59fd14b2c140bf858d16e DIST stp-2.3.3_gtest.tar.gz 469100 BLAKE2B 386444657d3f23e54f01dac8e0ac36da4d97c3eebcc8cf79bfc754c474a5ed64765a0ad389fef358667e468469c47d02a407e13e6882d426a4defb0102e4a758 SHA512 2fc79fe9c8a4e0487e7e76db9508fd2207df0cfe3940a51aeac32e4440afab9e265bfe553b1cd66086cd5a574d8bf99dbb9e1d9c4a70fafd7b31f38825914aa1 +DIST stp-2.3.4.tar.gz 3543794 BLAKE2B 94813f76db3f1ba5ccdd226d5013c470ea0e265ffccc53050d49b1f7bd09bac87f1baf7d49325b106fd9a2bf934e78e879f58c913685176bcebf0f92a9b70168 SHA512 d4355698cd2d96199bd548d996f0c50788c0329b20e79ea0dd4d9e04b48417850041205d7d9efa342f8a362d203d434ec25aa22649f650f658acac2bfadb3ecf diff --git a/sci-mathematics/stp/files/stp-2.3.4-gtest.patch b/sci-mathematics/stp/files/stp-2.3.4-gtest.patch new file mode 100644 index 000000000000..25fb88b87ea9 --- /dev/null +++ b/sci-mathematics/stp/files/stp-2.3.4-gtest.patch @@ -0,0 +1,26 @@ +--- a/tests/CMakeLists.txt ++++ b/tests/CMakeLists.txt +@@ -55,10 +55,7 @@ set(LIT_ARGS -s CACHE STRING "Arguments to pass to lit") + # the location of GTest source code is probably error prone so using a copy in the + # repository seems like the easiest thing to do. This also has the added benefit that + # everyone uses the same version of GTest. +-set(GTEST_PREFIX ${PROJECT_SOURCE_DIR}/deps/gtest) +-if (NOT EXISTS "${GTEST_PREFIX}/CMakeLists.txt") +- message(FATAL_ERROR "Could not find GTest. Did you run scripts/deps/setup-gtest.sh?") +-endif() ++find_package(GTest REQUIRED) + + if (MSVC) + # STP is built with the shared version of the CRT, gtest defaults to the +@@ -68,11 +65,8 @@ endif() + + set(PREV_CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS}") + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-format-nonliteral -Wno-missing-field-initializers") +-add_subdirectory(${GTEST_PREFIX} gtest) + set(CMAKE_CXX_FLAGS "${PREV_CMAKE_CXX_FLAGS}") +-set(GTEST_BOTH_LIBRARIES gtest gtest_main) + +-include_directories(${GTEST_PREFIX}/include) + + # Add handy macros/functions + include(AddSTPGTest) diff --git a/sci-mathematics/stp/files/stp-2.3.4-lit-cfg.patch b/sci-mathematics/stp/files/stp-2.3.4-lit-cfg.patch new file mode 100644 index 000000000000..34f92feb28c9 --- /dev/null +++ b/sci-mathematics/stp/files/stp-2.3.4-lit-cfg.patch @@ -0,0 +1,24 @@ +--- a/tests/query-files/lit.cfg ++++ b/tests/query-files/lit.cfg +@@ -6,6 +6,7 @@ import os + import sys + import re + import platform ++import shutil + + import lit.util + import lit.formats +@@ -107,12 +108,7 @@ lit_config.note('Using solver: {solver}\n'.format(solver=solverExecutable)) + config.substitutions.append( ('%solver', solverExecutable) ) + + # Find OutputCheck +-OutputCheckTool = os.path.join( os.path.dirname( os.path.dirname( config.test_source_root ) ), +- 'deps', +- 'OutputCheck', +- 'bin', +- 'OutputCheck' +- ) ++OutputCheckTool = shutil.which("OutputCheck") + if not os.path.exists(OutputCheckTool): + lit_config.fatal('Cannot find OutputCheck executable: {OutputCheck}'.format(OutputCheck=OutputCheckTool)) + diff --git a/sci-mathematics/stp/stp-2.3.4.ebuild b/sci-mathematics/stp/stp-2.3.4.ebuild new file mode 100644 index 000000000000..ab1cbf96c2d2 --- /dev/null +++ b/sci-mathematics/stp/stp-2.3.4.ebuild @@ -0,0 +1,109 @@ +# Copyright 1999-2024 Gentoo Authors +# Distributed under the terms of the GNU General Public License v2 + +EAPI=8 + +PYTHON_COMPAT=( python3_{10..13} ) + +inherit flag-o-matic python-single-r1 cmake + +DESCRIPTION="Simple Theorem Prover, an efficient SMT solver for bitvectors" +HOMEPAGE="https://stp.github.io/ + https://github.com/stp/stp/" + +if [[ "${PV}" == *9999* ]] ; then + inherit git-r3 + + EGIT_REPO_URI="https://github.com/stp/stp.git" +else + SRC_URI="https://github.com/stp/stp/archive/${PV}.tar.gz + -> ${P}.tar.gz" + + KEYWORDS="~amd64 ~x86" +fi + +LICENSE="GPL-2+ MIT" +SLOT="0/${PV}" +IUSE="cryptominisat debug +python test" +REQUIRED_USE="python? ( ${PYTHON_REQUIRED_USE} ) test? ( python )" +RESTRICT="!test? ( test )" + +RDEPEND=" + dev-libs/boost:= + sci-mathematics/minisat:= + sys-libs/zlib:= + cryptominisat? ( + dev-db/sqlite:3 + dev-libs/icu:= + sci-mathematics/cryptominisat:= + ) + python? ( + ${PYTHON_DEPS} + ) +" +DEPEND=" + ${RDEPEND} +" +BDEPEND=" + sys-apps/help2man + test? ( + dev-cpp/gtest + dev-python/OutputCheck + dev-python/lit + ) +" + +PATCHES=( + "${FILESDIR}/${PN}-2.3.3-CMakeLists.txt-fix_cflags.patch" + "${FILESDIR}/${PN}-2.3.3-stp.py-library_path.patch" + "${FILESDIR}/${PN}-2.3.4-gtest.patch" + "${FILESDIR}/${PN}-2.3.4-lit-cfg.patch" +) + +pkg_setup() { + if use python ; then + python-single-r1_pkg_setup + fi +} + +src_configure() { + # -Werror=odr warnings, bug #863263 + filter-lto + + local CMAKE_BUILD_TYPE + if use debug ; then + CMAKE_BUILD_TYPE="Debug" + else + CMAKE_BUILD_TYPE="Release" + fi + + local -a mycmakeargs=( + # -DGTEST_PREFIX="${BROOT}/usr/$(get_libdir)/cmake/GTest" + + -DTEST_C_API=OFF # C API test fail + -DUSE_RISS=OFF + + # Cryptominisat switches + -DNOCRYPTOMINISAT=$(usex cryptominisat 'OFF' 'ON') # double negation + -DFORCE_CMS=$(usex cryptominisat) + + -DENABLE_PYTHON_INTERFACE=$(usex python) + -DENABLE_ASSERTIONS=$(usex test) + -DENABLE_TESTING=$(usex test) + ) + cmake_src_configure +} + +src_install() { + cmake_src_install + + # Because Python files for tests (in BUILD_DIR) and those installed on the + # system differ, and are generated upon install, we have to wait for CMake + # to install them into the temporary image. + if use python ; then + python_optimize "${D}/$(python_get_sitedir)/stp" + fi + + mv "${D}/usr/man" "${D}/usr/share/man" || die + dodoc -r papers +} -- cgit v1.2.3-65-gdbad