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@gentoo.org>

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>jeffrey@icurse.nl</email>
-		<name>Jeffrey Lin</name>
-	</maintainer>
-	<maintainer type="project" proxied="proxy">
-		<email>proxy-maint@gentoo.org</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>jeffrey@icurse.nl</email>
+    <name>Jeffrey Lin</name>
+  </maintainer>
+  <maintainer type="project">
+    <email>sci-mathematics@gentoo.org</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
-}