commit: 317c9f66693a8341a07ba45fe158e8699cc1cd19 Author: Maciej Barć <xgqt <AT> gentoo <DOT> org> AuthorDate: Mon Dec 27 13:08:03 2021 +0000 Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org> CommitDate: Mon Dec 27 13:08:10 2021 +0000 URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=317c9f66
sci-mathematics/stp: multiple fixes - add missing test submodules - add optional cryptominisat dependency (USE=dependency) - add the Gentoo Mathematics Project to co-maintainers - change python to optional dependency (USE=python) - install PDF documentation - patch CMakeLists.txt to fix CFLAGS - patch stp.py to fix python module Closes: https://bugs.gentoo.org/759457 Package-Manager: Portage-3.0.28, Repoman-3.0.3 Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org> sci-mathematics/stp/Manifest | 2 + .../stp/files/stp-CMakeLists.txt-fix_cflags.patch | 21 +++++ .../stp/files/stp-stp.py-library_path.patch | 15 ++++ sci-mathematics/stp/metadata.xml | 51 +++++++----- sci-mathematics/stp/stp-2.3.3-r1.ebuild | 94 ++++++++++++++++++++++ sci-mathematics/stp/stp-2.3.3.ebuild | 45 ----------- 6 files changed, 161 insertions(+), 67 deletions(-) diff --git a/sci-mathematics/stp/Manifest b/sci-mathematics/stp/Manifest index e41280980dc7..0cbd33f52acc 100644 --- a/sci-mathematics/stp/Manifest +++ b/sci-mathematics/stp/Manifest @@ -1 +1,3 @@ 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 diff --git a/sci-mathematics/stp/files/stp-CMakeLists.txt-fix_cflags.patch b/sci-mathematics/stp/files/stp-CMakeLists.txt-fix_cflags.patch new file mode 100644 index 000000000000..93817e209376 --- /dev/null +++ b/sci-mathematics/stp/files/stp-CMakeLists.txt-fix_cflags.patch @@ -0,0 +1,21 @@ +index f6224a6..8c7c45e 100644 +--- a/CMakeLists.txt ++++ b/CMakeLists.txt +@@ -203,17 +203,9 @@ if (NOT MSVC) + add_compile_options( -g) + add_compile_options( -pthread ) + +- add_compile_options("$<$<CONFIG:RELWITHDEBINFO>:-O2>") +- +- add_compile_options("$<$<CONFIG:RELEASE>:-O2>") + add_compile_options("$<$<CONFIG:RELEASE>:-g0>") + + add_compile_options("$<$<CONFIG:DEBUG>:-O0>") +- +- if(NOT CMAKE_BUILD_TYPE STREQUAL "Debug") +- set(CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -O2") +- set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -O2") +- endif() + else() + # see https://msdn.microsoft.com/en-us/library/fwkeyyhe.aspx for details + # /ZI = include debug info diff --git a/sci-mathematics/stp/files/stp-stp.py-library_path.patch b/sci-mathematics/stp/files/stp-stp.py-library_path.patch new file mode 100644 index 000000000000..60b54aa2c1da --- /dev/null +++ b/sci-mathematics/stp/files/stp-stp.py-library_path.patch @@ -0,0 +1,15 @@ +index 61aef6d..16633e8 100644 +--- a/bindings/python/stp/stp.py.in ++++ b/bindings/python/stp/stp.py.in +@@ -42,7 +42,10 @@ Py3 = sys.version_info >= (3, 0, 0) + if Py3: + long = int + +-from library_path import PATHS ++try: ++ from .library_path import PATHS ++except ImportError: ++ from library_path import PATHS + + for path in PATHS: + if not os.path.exists(path): diff --git a/sci-mathematics/stp/metadata.xml b/sci-mathematics/stp/metadata.xml index 511b06e39e35..5054ed8fec27 100644 --- a/sci-mathematics/stp/metadata.xml +++ b/sci-mathematics/stp/metadata.xml @@ -1,26 +1,33 @@ <?xml version="1.0" encoding="UTF-8"?> <!DOCTYPE pkgmetadata SYSTEM "https://www.gentoo.org/dtd/metadata.dtd";> + <pkgmetadata> - <maintainer type="person" proxied="yes"> - <email>[email protected]</email> - <name>Jeffrey Lin</name> - </maintainer> - <maintainer type="project" proxied="proxy"> - <email>[email protected]</email> - <name>Proxy Maintainers</name> - </maintainer> - <longdescription lang="en"> - STP is a constraint solver (or SMT solver) aimed at solving - constraints of bitvectors and arrays. These types of - constraints can be generated by program analysis tools, theorem - provers, automated bug finders, cryptographic attack tools, - intelligent fuzzers, model checkers, and by many other - applications. - </longdescription> - <upstream> - <remote-id type="github">stp/stp</remote-id> - </upstream> - <use> - <flag name="python">Enable building the Python interface</flag> - </use> + <maintainer type="person" proxied="yes"> + <email>[email protected]</email> + <name>Jeffrey Lin</name> + </maintainer> + <maintainer type="project"> + <email>[email protected]</email> + <name>Gentoo Mathematics Project</name> + </maintainer> + <longdescription> + STP is a constraint solver (or SMT solver) aimed at solving + constraints of bitvectors and arrays. These types of + constraints can be generated by program analysis tools, theorem + provers, automated bug finders, cryptographic attack tools, + intelligent fuzzers, model checkers, and by many other + applications. + </longdescription> + <upstream> + <bugs-to>https://github.com/stp/stp/issues/</bugs-to> + <remote-id type="github">stp/stp</remote-id> + </upstream> + <use> + <flag name="cryptominisat"> + Enable <pkg>sci-mathematics/cryptominisat</pkg> support + </flag> + <flag name="python"> + Enable building the Python interface + </flag> + </use> </pkgmetadata> diff --git a/sci-mathematics/stp/stp-2.3.3-r1.ebuild b/sci-mathematics/stp/stp-2.3.3-r1.ebuild new file mode 100644 index 000000000000..367251ea5f8f --- /dev/null +++ b/sci-mathematics/stp/stp-2.3.3-r1.ebuild @@ -0,0 +1,94 @@ +# Copyright 1999-2021 Gentoo Authors +# Distributed under the terms of the GNU General Public License v2 + +EAPI=8 + +OC_H=119fe41a83bc455a24a11ecc9b78e7b13fcfcc45 +GT_H=2ad076167a676e3ed62f90b754b30fac5caa1f88 + +PYTHON_COMPAT=( python3_{8,9,10} ) + +inherit python-single-r1 cmake + +DESCRIPTION="Simple Theorem Prover, an efficient SMT solver for bitvectors" +HOMEPAGE="https://stp.github.io/"; +SRC_URI="https://github.com/stp/stp/archive/${PV}.tar.gz -> ${P}.tar.gz + test? ( + https://github.com/stp/OutputCheck/archive/${OC_H}.tar.gz -> ${P}_OutputCheck.tar.gz + https://github.com/stp/googletest/archive/${GT_H}.tar.gz -> ${P}_gtest.tar.gz + )" + +LICENSE="GPL-2+ MIT" +SLOT="0/${PV}" +KEYWORDS="~amd64 ~x86" +IUSE="cryptominisat debug +python test" +REQUIRED_USE="python? ( ${PYTHON_REQUIRED_USE} )" +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="test? ( dev-python/lit )" + +PATCHES=( + "${FILESDIR}"/stp-CMakeLists.txt-fix_cflags.patch + "${FILESDIR}"/stp-stp.py-library_path.patch +) + +pkg_setup() { + use python && python-single-r1_pkg_setup +} + +src_unpack() { + unpack ${P}.tar.gz + + if use test ; then + local i + for i in OutputCheck gtest ; do + tar xf "${DISTDIR}"/${P}_${i}.tar.gz --strip-components=1 \ + -C "${S}"/utils/${i} || die "failed to unpack ${i}" + done + fi +} + +src_prepare() { + # Replace static lib with get_libdir + sed -i "s/set(LIBDIR lib/set(LIBDIR $(get_libdir)/" CMakeLists.txt || die + + # Remove problematic test + rm "${S}"/tests/query-files/misc-tests/no-query.cvc || die + + cmake_src_prepare +} + +src_configure() { + local CMAKE_BUILD_TYPE + if use debug ; then + CMAKE_BUILD_TYPE=Debug + else + CMAKE_BUILD_TYPE=Release + fi + local mycmakeargs=( + -DNOCRYPTOMINISAT=$(usex cryptominisat 'OFF' 'ON') # double negation + -DENABLE_PYTHON_INTERFACE=$(usex python) + -DENABLE_ASSERTIONS=$(usex test) + -DENABLE_TESTING=$(usex test) + ) + cmake_src_configure +} + +src_install() { + cmake_src_install + mv "${D}"/usr/man "${D}"/usr/share/man || die + + dodoc -r papers +} diff --git a/sci-mathematics/stp/stp-2.3.3.ebuild b/sci-mathematics/stp/stp-2.3.3.ebuild deleted file mode 100644 index c88151911bae..000000000000 --- a/sci-mathematics/stp/stp-2.3.3.ebuild +++ /dev/null @@ -1,45 +0,0 @@ -# Copyright 1999-2020 Gentoo Authors -# Distributed under the terms of the GNU General Public License v2 - -EAPI=7 - -inherit cmake - -DESCRIPTION="Simple Theorem Prover, an efficient SMT solver for bitvectors" -HOMEPAGE="https://stp.github.io/"; -SRC_URI="https://github.com/stp/${PN}/archive/${PV}.tar.gz -> ${P}.tar.gz" -LICENSE="GPL-2+ MIT" -SLOT="0" -KEYWORDS="~amd64 ~x86" -IUSE="python test" -RESTRICT="!test? ( test )" - -DEPEND=" - dev-libs/boost:= - sci-mathematics/minisat -" -RDEPEND="${DEPEND}" - -src_prepare() { - # replace static lib with $(get_libdir) - sed -i "s/set(LIBDIR lib/set(LIBDIR $(get_libdir)/" CMakeLists.txt || die - - cmake_src_prepare -} - -src_configure() { - local mycmakeargs=( - -DENABLE_ASSERTIONS="$(usex test)" - -DENABLE_TESTING="$(usex test)" - -DENABLE_PYTHON_INTERFACE="$(usex python)" - ) - cmake_src_configure -} - -src_install() { - cmake_src_install - - # don't install to /usr/man - doman "${D}/usr/man/man1/stp.1" - rm -r "${D}/usr/man" || die -}
