1 |
commit: 317c9f66693a8341a07ba45fe158e8699cc1cd19 |
2 |
Author: Maciej Barć <xgqt <AT> gentoo <DOT> org> |
3 |
AuthorDate: Mon Dec 27 13:08:03 2021 +0000 |
4 |
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org> |
5 |
CommitDate: Mon Dec 27 13:08:10 2021 +0000 |
6 |
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=317c9f66 |
7 |
|
8 |
sci-mathematics/stp: multiple fixes |
9 |
|
10 |
- add missing test submodules |
11 |
- add optional cryptominisat dependency (USE=dependency) |
12 |
- add the Gentoo Mathematics Project to co-maintainers |
13 |
- change python to optional dependency (USE=python) |
14 |
- install PDF documentation |
15 |
- patch CMakeLists.txt to fix CFLAGS |
16 |
- patch stp.py to fix python module |
17 |
|
18 |
Closes: https://bugs.gentoo.org/759457 |
19 |
Package-Manager: Portage-3.0.28, Repoman-3.0.3 |
20 |
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org> |
21 |
|
22 |
sci-mathematics/stp/Manifest | 2 + |
23 |
.../stp/files/stp-CMakeLists.txt-fix_cflags.patch | 21 +++++ |
24 |
.../stp/files/stp-stp.py-library_path.patch | 15 ++++ |
25 |
sci-mathematics/stp/metadata.xml | 51 +++++++----- |
26 |
sci-mathematics/stp/stp-2.3.3-r1.ebuild | 94 ++++++++++++++++++++++ |
27 |
sci-mathematics/stp/stp-2.3.3.ebuild | 45 ----------- |
28 |
6 files changed, 161 insertions(+), 67 deletions(-) |
29 |
|
30 |
diff --git a/sci-mathematics/stp/Manifest b/sci-mathematics/stp/Manifest |
31 |
index e41280980dc7..0cbd33f52acc 100644 |
32 |
--- a/sci-mathematics/stp/Manifest |
33 |
+++ b/sci-mathematics/stp/Manifest |
34 |
@@ -1 +1,3 @@ |
35 |
DIST stp-2.3.3.tar.gz 2577550 BLAKE2B 9ebedf3cb8e6b50d037cfacbc14826bd4e6505d29a53b1fcc6580749f0637fe5f96619c166babdb3a52b18fb6337e49c02f5693e233effe84d0131d0e7402381 SHA512 a0b1bf419d8230e40ce0aee90d9c8c9d814aca300831c24b3576c75623362942abf20673c419f9f0ea1e0505bfae000dc65fdd818179f5759879b0b255f1b99a |
36 |
+DIST stp-2.3.3_OutputCheck.tar.gz 12002 BLAKE2B f8fafba8f7957f3d0ee480b9e1e8c8923c373cf134512d6329adf84a96f3177ad07d00eae4dc6dd8d4b09ca82dfc8b425602f1926e3f88ccb2556b4b7121e5b9 SHA512 36012ae2b2aee1ff3f36ba1678a4bcbfeb590e01c2042ca35eb2f49b6a890b767c1809d1415e7b03f2118204361f834ad9caf70319b59fd14b2c140bf858d16e |
37 |
+DIST stp-2.3.3_gtest.tar.gz 469100 BLAKE2B 386444657d3f23e54f01dac8e0ac36da4d97c3eebcc8cf79bfc754c474a5ed64765a0ad389fef358667e468469c47d02a407e13e6882d426a4defb0102e4a758 SHA512 2fc79fe9c8a4e0487e7e76db9508fd2207df0cfe3940a51aeac32e4440afab9e265bfe553b1cd66086cd5a574d8bf99dbb9e1d9c4a70fafd7b31f38825914aa1 |
38 |
|
39 |
diff --git a/sci-mathematics/stp/files/stp-CMakeLists.txt-fix_cflags.patch b/sci-mathematics/stp/files/stp-CMakeLists.txt-fix_cflags.patch |
40 |
new file mode 100644 |
41 |
index 000000000000..93817e209376 |
42 |
--- /dev/null |
43 |
+++ b/sci-mathematics/stp/files/stp-CMakeLists.txt-fix_cflags.patch |
44 |
@@ -0,0 +1,21 @@ |
45 |
+index f6224a6..8c7c45e 100644 |
46 |
+--- a/CMakeLists.txt |
47 |
++++ b/CMakeLists.txt |
48 |
+@@ -203,17 +203,9 @@ if (NOT MSVC) |
49 |
+ add_compile_options( -g) |
50 |
+ add_compile_options( -pthread ) |
51 |
+ |
52 |
+- add_compile_options("$<$<CONFIG:RELWITHDEBINFO>:-O2>") |
53 |
+- |
54 |
+- add_compile_options("$<$<CONFIG:RELEASE>:-O2>") |
55 |
+ add_compile_options("$<$<CONFIG:RELEASE>:-g0>") |
56 |
+ |
57 |
+ add_compile_options("$<$<CONFIG:DEBUG>:-O0>") |
58 |
+- |
59 |
+- if(NOT CMAKE_BUILD_TYPE STREQUAL "Debug") |
60 |
+- set(CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -O2") |
61 |
+- set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -O2") |
62 |
+- endif() |
63 |
+ else() |
64 |
+ # see https://msdn.microsoft.com/en-us/library/fwkeyyhe.aspx for details |
65 |
+ # /ZI = include debug info |
66 |
|
67 |
diff --git a/sci-mathematics/stp/files/stp-stp.py-library_path.patch b/sci-mathematics/stp/files/stp-stp.py-library_path.patch |
68 |
new file mode 100644 |
69 |
index 000000000000..60b54aa2c1da |
70 |
--- /dev/null |
71 |
+++ b/sci-mathematics/stp/files/stp-stp.py-library_path.patch |
72 |
@@ -0,0 +1,15 @@ |
73 |
+index 61aef6d..16633e8 100644 |
74 |
+--- a/bindings/python/stp/stp.py.in |
75 |
++++ b/bindings/python/stp/stp.py.in |
76 |
+@@ -42,7 +42,10 @@ Py3 = sys.version_info >= (3, 0, 0) |
77 |
+ if Py3: |
78 |
+ long = int |
79 |
+ |
80 |
+-from library_path import PATHS |
81 |
++try: |
82 |
++ from .library_path import PATHS |
83 |
++except ImportError: |
84 |
++ from library_path import PATHS |
85 |
+ |
86 |
+ for path in PATHS: |
87 |
+ if not os.path.exists(path): |
88 |
|
89 |
diff --git a/sci-mathematics/stp/metadata.xml b/sci-mathematics/stp/metadata.xml |
90 |
index 511b06e39e35..5054ed8fec27 100644 |
91 |
--- a/sci-mathematics/stp/metadata.xml |
92 |
+++ b/sci-mathematics/stp/metadata.xml |
93 |
@@ -1,26 +1,33 @@ |
94 |
<?xml version="1.0" encoding="UTF-8"?> |
95 |
<!DOCTYPE pkgmetadata SYSTEM "https://www.gentoo.org/dtd/metadata.dtd"> |
96 |
+ |
97 |
<pkgmetadata> |
98 |
- <maintainer type="person" proxied="yes"> |
99 |
- <email>jeffrey@××××××.nl</email> |
100 |
- <name>Jeffrey Lin</name> |
101 |
- </maintainer> |
102 |
- <maintainer type="project" proxied="proxy"> |
103 |
- <email>proxy-maint@g.o</email> |
104 |
- <name>Proxy Maintainers</name> |
105 |
- </maintainer> |
106 |
- <longdescription lang="en"> |
107 |
- STP is a constraint solver (or SMT solver) aimed at solving |
108 |
- constraints of bitvectors and arrays. These types of |
109 |
- constraints can be generated by program analysis tools, theorem |
110 |
- provers, automated bug finders, cryptographic attack tools, |
111 |
- intelligent fuzzers, model checkers, and by many other |
112 |
- applications. |
113 |
- </longdescription> |
114 |
- <upstream> |
115 |
- <remote-id type="github">stp/stp</remote-id> |
116 |
- </upstream> |
117 |
- <use> |
118 |
- <flag name="python">Enable building the Python interface</flag> |
119 |
- </use> |
120 |
+ <maintainer type="person" proxied="yes"> |
121 |
+ <email>jeffrey@××××××.nl</email> |
122 |
+ <name>Jeffrey Lin</name> |
123 |
+ </maintainer> |
124 |
+ <maintainer type="project"> |
125 |
+ <email>sci-mathematics@g.o</email> |
126 |
+ <name>Gentoo Mathematics Project</name> |
127 |
+ </maintainer> |
128 |
+ <longdescription> |
129 |
+ STP is a constraint solver (or SMT solver) aimed at solving |
130 |
+ constraints of bitvectors and arrays. These types of |
131 |
+ constraints can be generated by program analysis tools, theorem |
132 |
+ provers, automated bug finders, cryptographic attack tools, |
133 |
+ intelligent fuzzers, model checkers, and by many other |
134 |
+ applications. |
135 |
+ </longdescription> |
136 |
+ <upstream> |
137 |
+ <bugs-to>https://github.com/stp/stp/issues/</bugs-to> |
138 |
+ <remote-id type="github">stp/stp</remote-id> |
139 |
+ </upstream> |
140 |
+ <use> |
141 |
+ <flag name="cryptominisat"> |
142 |
+ Enable <pkg>sci-mathematics/cryptominisat</pkg> support |
143 |
+ </flag> |
144 |
+ <flag name="python"> |
145 |
+ Enable building the Python interface |
146 |
+ </flag> |
147 |
+ </use> |
148 |
</pkgmetadata> |
149 |
|
150 |
diff --git a/sci-mathematics/stp/stp-2.3.3-r1.ebuild b/sci-mathematics/stp/stp-2.3.3-r1.ebuild |
151 |
new file mode 100644 |
152 |
index 000000000000..367251ea5f8f |
153 |
--- /dev/null |
154 |
+++ b/sci-mathematics/stp/stp-2.3.3-r1.ebuild |
155 |
@@ -0,0 +1,94 @@ |
156 |
+# Copyright 1999-2021 Gentoo Authors |
157 |
+# Distributed under the terms of the GNU General Public License v2 |
158 |
+ |
159 |
+EAPI=8 |
160 |
+ |
161 |
+OC_H=119fe41a83bc455a24a11ecc9b78e7b13fcfcc45 |
162 |
+GT_H=2ad076167a676e3ed62f90b754b30fac5caa1f88 |
163 |
+ |
164 |
+PYTHON_COMPAT=( python3_{8,9,10} ) |
165 |
+ |
166 |
+inherit python-single-r1 cmake |
167 |
+ |
168 |
+DESCRIPTION="Simple Theorem Prover, an efficient SMT solver for bitvectors" |
169 |
+HOMEPAGE="https://stp.github.io/" |
170 |
+SRC_URI="https://github.com/stp/stp/archive/${PV}.tar.gz -> ${P}.tar.gz |
171 |
+ test? ( |
172 |
+ https://github.com/stp/OutputCheck/archive/${OC_H}.tar.gz -> ${P}_OutputCheck.tar.gz |
173 |
+ https://github.com/stp/googletest/archive/${GT_H}.tar.gz -> ${P}_gtest.tar.gz |
174 |
+ )" |
175 |
+ |
176 |
+LICENSE="GPL-2+ MIT" |
177 |
+SLOT="0/${PV}" |
178 |
+KEYWORDS="~amd64 ~x86" |
179 |
+IUSE="cryptominisat debug +python test" |
180 |
+REQUIRED_USE="python? ( ${PYTHON_REQUIRED_USE} )" |
181 |
+RESTRICT="!test? ( test )" |
182 |
+ |
183 |
+RDEPEND=" |
184 |
+ dev-libs/boost:= |
185 |
+ sci-mathematics/minisat:= |
186 |
+ sys-libs/zlib:= |
187 |
+ cryptominisat? ( |
188 |
+ dev-db/sqlite:3 |
189 |
+ dev-libs/icu:= |
190 |
+ sci-mathematics/cryptominisat:= |
191 |
+ ) |
192 |
+ python? ( ${PYTHON_DEPS} ) |
193 |
+" |
194 |
+DEPEND="${RDEPEND}" |
195 |
+BDEPEND="test? ( dev-python/lit )" |
196 |
+ |
197 |
+PATCHES=( |
198 |
+ "${FILESDIR}"/stp-CMakeLists.txt-fix_cflags.patch |
199 |
+ "${FILESDIR}"/stp-stp.py-library_path.patch |
200 |
+) |
201 |
+ |
202 |
+pkg_setup() { |
203 |
+ use python && python-single-r1_pkg_setup |
204 |
+} |
205 |
+ |
206 |
+src_unpack() { |
207 |
+ unpack ${P}.tar.gz |
208 |
+ |
209 |
+ if use test ; then |
210 |
+ local i |
211 |
+ for i in OutputCheck gtest ; do |
212 |
+ tar xf "${DISTDIR}"/${P}_${i}.tar.gz --strip-components=1 \ |
213 |
+ -C "${S}"/utils/${i} || die "failed to unpack ${i}" |
214 |
+ done |
215 |
+ fi |
216 |
+} |
217 |
+ |
218 |
+src_prepare() { |
219 |
+ # Replace static lib with get_libdir |
220 |
+ sed -i "s/set(LIBDIR lib/set(LIBDIR $(get_libdir)/" CMakeLists.txt || die |
221 |
+ |
222 |
+ # Remove problematic test |
223 |
+ rm "${S}"/tests/query-files/misc-tests/no-query.cvc || die |
224 |
+ |
225 |
+ cmake_src_prepare |
226 |
+} |
227 |
+ |
228 |
+src_configure() { |
229 |
+ local CMAKE_BUILD_TYPE |
230 |
+ if use debug ; then |
231 |
+ CMAKE_BUILD_TYPE=Debug |
232 |
+ else |
233 |
+ CMAKE_BUILD_TYPE=Release |
234 |
+ fi |
235 |
+ local mycmakeargs=( |
236 |
+ -DNOCRYPTOMINISAT=$(usex cryptominisat 'OFF' 'ON') # double negation |
237 |
+ -DENABLE_PYTHON_INTERFACE=$(usex python) |
238 |
+ -DENABLE_ASSERTIONS=$(usex test) |
239 |
+ -DENABLE_TESTING=$(usex test) |
240 |
+ ) |
241 |
+ cmake_src_configure |
242 |
+} |
243 |
+ |
244 |
+src_install() { |
245 |
+ cmake_src_install |
246 |
+ mv "${D}"/usr/man "${D}"/usr/share/man || die |
247 |
+ |
248 |
+ dodoc -r papers |
249 |
+} |
250 |
|
251 |
diff --git a/sci-mathematics/stp/stp-2.3.3.ebuild b/sci-mathematics/stp/stp-2.3.3.ebuild |
252 |
deleted file mode 100644 |
253 |
index c88151911bae..000000000000 |
254 |
--- a/sci-mathematics/stp/stp-2.3.3.ebuild |
255 |
+++ /dev/null |
256 |
@@ -1,45 +0,0 @@ |
257 |
-# Copyright 1999-2020 Gentoo Authors |
258 |
-# Distributed under the terms of the GNU General Public License v2 |
259 |
- |
260 |
-EAPI=7 |
261 |
- |
262 |
-inherit cmake |
263 |
- |
264 |
-DESCRIPTION="Simple Theorem Prover, an efficient SMT solver for bitvectors" |
265 |
-HOMEPAGE="https://stp.github.io/" |
266 |
-SRC_URI="https://github.com/stp/${PN}/archive/${PV}.tar.gz -> ${P}.tar.gz" |
267 |
-LICENSE="GPL-2+ MIT" |
268 |
-SLOT="0" |
269 |
-KEYWORDS="~amd64 ~x86" |
270 |
-IUSE="python test" |
271 |
-RESTRICT="!test? ( test )" |
272 |
- |
273 |
-DEPEND=" |
274 |
- dev-libs/boost:= |
275 |
- sci-mathematics/minisat |
276 |
-" |
277 |
-RDEPEND="${DEPEND}" |
278 |
- |
279 |
-src_prepare() { |
280 |
- # replace static lib with $(get_libdir) |
281 |
- sed -i "s/set(LIBDIR lib/set(LIBDIR $(get_libdir)/" CMakeLists.txt || die |
282 |
- |
283 |
- cmake_src_prepare |
284 |
-} |
285 |
- |
286 |
-src_configure() { |
287 |
- local mycmakeargs=( |
288 |
- -DENABLE_ASSERTIONS="$(usex test)" |
289 |
- -DENABLE_TESTING="$(usex test)" |
290 |
- -DENABLE_PYTHON_INTERFACE="$(usex python)" |
291 |
- ) |
292 |
- cmake_src_configure |
293 |
-} |
294 |
- |
295 |
-src_install() { |
296 |
- cmake_src_install |
297 |
- |
298 |
- # don't install to /usr/man |
299 |
- doman "${D}/usr/man/man1/stp.1" |
300 |
- rm -r "${D}/usr/man" || die |
301 |
-} |