1 |
commit: 118ae495ef2e4f65f8c48245dc6367da28bb8035 |
2 |
Author: Michał Górny <mgorny <AT> gentoo <DOT> org> |
3 |
AuthorDate: Sat Sep 14 15:43:59 2019 +0000 |
4 |
Commit: Michał Górny <mgorny <AT> gentoo <DOT> org> |
5 |
CommitDate: Sat Sep 14 15:43:59 2019 +0000 |
6 |
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=118ae495 |
7 |
|
8 |
sci-mathematics/cvc3: Remove last-rited pkg |
9 |
|
10 |
Signed-off-by: Michał Górny <mgorny <AT> gentoo.org> |
11 |
|
12 |
profiles/package.mask | 1 - |
13 |
sci-mathematics/cvc3/Manifest | 1 - |
14 |
sci-mathematics/cvc3/cvc3-2.4.1-r1.ebuild | 141 --------------------- |
15 |
sci-mathematics/cvc3/files/50cvc3-gentoo.el | 3 - |
16 |
.../cvc3/files/cvc3-2.4.1-gccv6-fix.patch | 76 ----------- |
17 |
sci-mathematics/cvc3/metadata.xml | 45 ------- |
18 |
6 files changed, 267 deletions(-) |
19 |
|
20 |
diff --git a/profiles/package.mask b/profiles/package.mask |
21 |
index 5ff22066369..0de8a394f4f 100644 |
22 |
--- a/profiles/package.mask |
23 |
+++ b/profiles/package.mask |
24 |
@@ -1118,7 +1118,6 @@ dev-util/deskzilla |
25 |
media-sound/tuxguitar |
26 |
sci-mathematics/isabelle |
27 |
sci-chemistry/jmol |
28 |
-sci-mathematics/cvc3 |
29 |
|
30 |
# Michał Górny <mgorny@g.o> (2019-08-14) |
31 |
# No longer builds. Homepage is gone, and its keep-alive fork is also |
32 |
|
33 |
diff --git a/sci-mathematics/cvc3/Manifest b/sci-mathematics/cvc3/Manifest |
34 |
deleted file mode 100644 |
35 |
index 92a06778327..00000000000 |
36 |
--- a/sci-mathematics/cvc3/Manifest |
37 |
+++ /dev/null |
38 |
@@ -1 +0,0 @@ |
39 |
-DIST cvc3-2.4.1.tar.gz 1196616 BLAKE2B 8d3f7cbd24a1ba7e558fa8f91f9dd8f3fdc1aee3dd0d0e460bfb6e7922ae54cebaad3696912d3d0fb735ce1f6d00ac32a7d65c0b01af870124e48d9c96855aac SHA512 48e5cd82b3eb7506d762c2abc8db0c8fbc548575a1362dda53888075ac105a5bc0f0d58dfe01b60f207bc00ff8dfc39a5b3d9317784fe551658c884bb02e1ff2 |
40 |
|
41 |
diff --git a/sci-mathematics/cvc3/cvc3-2.4.1-r1.ebuild b/sci-mathematics/cvc3/cvc3-2.4.1-r1.ebuild |
42 |
deleted file mode 100644 |
43 |
index b51969ee713..00000000000 |
44 |
--- a/sci-mathematics/cvc3/cvc3-2.4.1-r1.ebuild |
45 |
+++ /dev/null |
46 |
@@ -1,141 +0,0 @@ |
47 |
-# Copyright 1999-2016 Gentoo Foundation |
48 |
-# Distributed under the terms of the GNU General Public License v2 |
49 |
- |
50 |
-EAPI=6 |
51 |
- |
52 |
-inherit elisp-common |
53 |
- |
54 |
-DESCRIPTION="CVC3 is a theorem prover for Satisfiability Modulo Theories (SMT) problems" |
55 |
-HOMEPAGE="http://www.cs.nyu.edu/acsys/cvc3/index.html" |
56 |
-SRC_URI="http://www.cs.nyu.edu/acsys/cvc3/releases/2.4.1/${P}.tar.gz" |
57 |
- |
58 |
-LICENSE="BSD MIT HPND zchaff? ( zchaff )" |
59 |
-RESTRICT="mirror zchaff? ( bindist )" |
60 |
-SLOT="0/${PV}" |
61 |
-KEYWORDS="~amd64 ~x86" |
62 |
-IUSE="doc emacs isabelle test zchaff" |
63 |
- |
64 |
-RDEPEND="dev-libs/gmp:0= |
65 |
- isabelle? ( >=sci-mathematics/isabelle-2011.1-r1:= )" |
66 |
-DEPEND="${RDEPEND} |
67 |
- doc? ( |
68 |
- app-doc/doxygen |
69 |
- media-gfx/graphviz |
70 |
- ) |
71 |
- emacs? ( |
72 |
- virtual/emacs |
73 |
- )" |
74 |
- |
75 |
-SITEFILE="50${PN}-gentoo.el" |
76 |
- |
77 |
-PATCHES=( "${FILESDIR}/${P}-gccv6-fix.patch" ) |
78 |
- |
79 |
-src_prepare() { |
80 |
- default |
81 |
- |
82 |
- sed -e 's#prefix=@prefix@#prefix=$(patsubst %/,%,$(DESTDIR))@prefix@#' \ |
83 |
- -e 's#libdir=@libdir@#libdir=$(patsubst %/,%,$(DESTDIR))@libdir@#' \ |
84 |
- -e 's#mandir=@mandir@#mandir=$(patsubst %/,%,$(DESTDIR))@mandir@#' \ |
85 |
- -i "${S}/Makefile.local.in" \ |
86 |
- || die "Could not set DESTDIR in Makefile.local.in" |
87 |
-} |
88 |
- |
89 |
-src_configure() { |
90 |
- # --enable-static disables building of shared libraries, statically |
91 |
- # links /usr/bin/cvc3 and installs static libraries. |
92 |
- # --enable-static --enable-sharedlibs behaves the same as just --enable-static |
93 |
- econf \ |
94 |
- --enable-dynamic \ |
95 |
- $(use_enable zchaff) |
96 |
- |
97 |
- if use test; then |
98 |
- sed -e 's@LD_LIBS = @LD_LIBS = -L'"${S}"'/lib -Wl,-R'"${S}"'/lib @' \ |
99 |
- -i "${S}/test/Makefile" \ |
100 |
- || die "Could not set library paths in test/Makefile" |
101 |
- fi |
102 |
-} |
103 |
- |
104 |
-src_compile() { |
105 |
- emake |
106 |
- |
107 |
- use doc && emake -C doc |
108 |
- |
109 |
- if use emacs; then |
110 |
- pushd emacs >/dev/null || die |
111 |
- elisp-compile *.el || die "emacs elisp compile failed" |
112 |
- popd >/dev/null || die |
113 |
- fi |
114 |
- |
115 |
- use test && emake -C test |
116 |
-} |
117 |
- |
118 |
-src_test() { |
119 |
- pushd test >/dev/null || die |
120 |
- ./bin/test || die "Testsuite failed" |
121 |
- popd >/dev/null || die |
122 |
-} |
123 |
- |
124 |
-src_install() { |
125 |
- use doc && local HTML_DOCS=( doc/html/*.{html,gif,png,css} ) |
126 |
- default |
127 |
- |
128 |
- if use emacs; then |
129 |
- elisp-install ${PN} emacs/*.{el,elc} |
130 |
- cp "${FILESDIR}"/${SITEFILE} "${S}" || die "Failed to copy Emacs files" |
131 |
- elisp-site-file-install ${SITEFILE} |
132 |
- fi |
133 |
- |
134 |
- if use isabelle; then |
135 |
- ISABELLE_HOME="$(isabelle getenv ISABELLE_HOME | cut -d'=' -f 2)" \ |
136 |
- || die "isabelle getenv ISABELLE_HOME failed" |
137 |
- [[ -n "${ISABELLE_HOME}" ]] || die "ISABELLE_HOME empty" |
138 |
- dodir "${ISABELLE_HOME}/contrib/${PN}-${PV}/etc" |
139 |
- cat >> settings <<- EOF || die "Failed to create Isabelle configuration for CVC3" |
140 |
- CVC3_COMPONENT="\$COMPONENT" |
141 |
- CVC3_HOME="${EPREFIX}/usr/bin" |
142 |
- CVC3_SOLVER="\$CVC3_HOME/cvc3" |
143 |
- CVC3_REMOTE_SOLVER="cvc3" |
144 |
- CVC3_INSTALLED="yes" |
145 |
- EOF |
146 |
- insinto "${ISABELLE_HOME}/contrib/${PN}-${PV}/etc" |
147 |
- doins settings |
148 |
- fi |
149 |
-} |
150 |
- |
151 |
-pkg_postinst() { |
152 |
- use emacs && elisp-site-regen |
153 |
- if use isabelle; then |
154 |
- if [[ -f "${EROOT%/}/etc/isabelle/components" ]]; then |
155 |
- if egrep "contrib/${PN}-[0-9.]*" "${EROOT%/}/etc/isabelle/components"; then |
156 |
- sed -e "/contrib\/${PN}-[0-9.]*/d" \ |
157 |
- -i "${EROOT%/}/etc/isabelle/components" || die "Failed to remove old CVC3 registrations in Isabelle" |
158 |
- fi |
159 |
- cat >> "${EROOT%/}/etc/isabelle/components" <<- EOF || die "Failed to register CVC3 with Isabelle" |
160 |
- contrib/${PN}-${PV} |
161 |
- EOF |
162 |
- fi |
163 |
- fi |
164 |
- if use zchaff; then |
165 |
- einfo "This copy of CVC3 is also configured to use the SAT solver zchaff whose" |
166 |
- einfo "copyright is owned by Princeton University and is more restrictive." |
167 |
- einfo "Specifically, it may be used for internal, noncommercial, research purposes" |
168 |
- einfo "only. See the copyright notices from the zchaff source files which are" |
169 |
- einfo "included in the LICENSE file." |
170 |
- einfo "To build CVC3 without these files, please build cvc3 without the zchaff" |
171 |
- einfo "use flag (note: zchaff is disabled by default):" |
172 |
- einfo "USE=-zchaff emerge sci-mathemathematics/cvc3" |
173 |
- fi |
174 |
-} |
175 |
- |
176 |
-pkg_postrm() { |
177 |
- use emacs && elisp-site-regen |
178 |
- if use isabelle; then |
179 |
- if [[ ! -f "${EROOT%/}/usr/bin/cvc3" && -f "${EROOT%/}/etc/isabelle/components" ]]; then |
180 |
- # Note: this sed should only match the version of this ebuild |
181 |
- # Which is what we want as we do not want to remove the line |
182 |
- # of a new CVC3 being installed during an upgrade. |
183 |
- sed -e "/contrib\/${PN}-${PV}/d" \ |
184 |
- -i "${EROOT%/}/etc/isabelle/components" || die "Failed to unregister CVC3 from Isabelle" |
185 |
- fi |
186 |
- fi |
187 |
-} |
188 |
|
189 |
diff --git a/sci-mathematics/cvc3/files/50cvc3-gentoo.el b/sci-mathematics/cvc3/files/50cvc3-gentoo.el |
190 |
deleted file mode 100644 |
191 |
index 8e046edf7ad..00000000000 |
192 |
--- a/sci-mathematics/cvc3/files/50cvc3-gentoo.el |
193 |
+++ /dev/null |
194 |
@@ -1,3 +0,0 @@ |
195 |
-(add-to-list 'load-path "@SITELISP@") |
196 |
-(add-to-list 'auto-mode-alist '("\\.cvc\\'" . cvc-mode)) |
197 |
-(autoload 'cvc-mode "cvc-mode" "CVC specifications editing mode." t) |
198 |
|
199 |
diff --git a/sci-mathematics/cvc3/files/cvc3-2.4.1-gccv6-fix.patch b/sci-mathematics/cvc3/files/cvc3-2.4.1-gccv6-fix.patch |
200 |
deleted file mode 100644 |
201 |
index 1fb3516b8c2..00000000000 |
202 |
--- a/sci-mathematics/cvc3/files/cvc3-2.4.1-gccv6-fix.patch |
203 |
+++ /dev/null |
204 |
@@ -1,76 +0,0 @@ |
205 |
-commit 4eb28b907e89be05d92eb704115f821b9b848e60 |
206 |
-Author: Matthew Dawson <matthew@××××××××××.ca> |
207 |
-Date: Sun Oct 16 22:06:03 2016 -0400 |
208 |
- |
209 |
- Fix gcc v6 compile failures. |
210 |
- |
211 |
- * Use std::hash<const char*> over std::hash<char *>, as throwing away the const is not allowed. |
212 |
- * Use Hash::hash by default in CDMap over std::hash, to get Hash::hash<CVC3::expr> |
213 |
- |
214 |
-diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp |
215 |
-index 0c85ff6..e4dd251 100644 |
216 |
---- a/src/expr/expr_value.cpp |
217 |
-+++ b/src/expr/expr_value.cpp |
218 |
-@@ -29,7 +29,7 @@ namespace CVC3 { |
219 |
- // Class ExprValue static members |
220 |
- //////////////////////////////////////////////////////////////////////// |
221 |
- |
222 |
--std::hash<char*> ExprValue::s_charHash; |
223 |
-+std::hash<const char*> ExprValue::s_charHash; |
224 |
- std::hash<long int> ExprValue::s_intHash; |
225 |
- |
226 |
- //////////////////////////////////////////////////////////////////////// |
227 |
-diff --git a/src/include/cdmap.h b/src/include/cdmap.h |
228 |
-index faf682a..c3b094c 100644 |
229 |
---- a/src/include/cdmap.h |
230 |
-+++ b/src/include/cdmap.h |
231 |
-@@ -43,9 +43,9 @@ namespace CVC3 { |
232 |
- // Auxiliary class: almost the same as CDO (see cdo.h), but on |
233 |
- // setNull() call it erases itself from the map. |
234 |
- |
235 |
--template <class Key, class Data, class HashFcn = std::hash<Key> > class CDMap; |
236 |
-+template <class Key, class Data, class HashFcn = Hash::hash<Key> > class CDMap; |
237 |
- |
238 |
--template <class Key, class Data, class HashFcn = std::hash<Key> > |
239 |
-+template <class Key, class Data, class HashFcn = Hash::hash<Key> > |
240 |
- class CDOmap :public ContextObj { |
241 |
- Key d_key; |
242 |
- Data d_data; |
243 |
-diff --git a/src/include/expr_hash.h b/src/include/expr_hash.h |
244 |
-index b2107d7..baa2eab 100644 |
245 |
---- a/src/include/expr_hash.h |
246 |
-+++ b/src/include/expr_hash.h |
247 |
-@@ -20,7 +20,6 @@ |
248 |
- * hash_set over Expr class. |
249 |
- */ |
250 |
- /*****************************************************************************/ |
251 |
-- |
252 |
- #ifndef _cvc3__expr_h_ |
253 |
- #include "expr.h" |
254 |
- #endif |
255 |
-diff --git a/src/include/expr_value.h b/src/include/expr_value.h |
256 |
-index 95102b2..f53aa4d 100644 |
257 |
---- a/src/include/expr_value.h |
258 |
-+++ b/src/include/expr_value.h |
259 |
-@@ -179,7 +179,7 @@ protected: |
260 |
- // Static hash functions. They don't depend on the context |
261 |
- // (ExprManager and such), so it is still thread-safe to have them |
262 |
- // static. |
263 |
-- static std::hash<char*> s_charHash; |
264 |
-+ static std::hash<const char*> s_charHash; |
265 |
- static std::hash<long int> s_intHash; |
266 |
- |
267 |
- static size_t pointerHash(void* p) { return s_intHash((long int)p); } |
268 |
-diff --git a/src/theory_core/theory_core.cpp b/src/theory_core/theory_core.cpp |
269 |
-index df5289f..37ccab9 100644 |
270 |
---- a/src/theory_core/theory_core.cpp |
271 |
-+++ b/src/theory_core/theory_core.cpp |
272 |
-@@ -710,7 +710,7 @@ TheoryCore::TheoryCore(ContextManager* cm, |
273 |
- // d_termTheorems(cm->getCurrentContext()), |
274 |
- d_predicates(cm->getCurrentContext()), |
275 |
- d_solver(NULL), |
276 |
-- d_simplifyInPlace(false), |
277 |
-+ d_simplifyInPlace(NULL), |
278 |
- d_currentRecursiveSimplifier(NULL), |
279 |
- d_resourceLimit(0), |
280 |
- d_timeBase(0), |
281 |
|
282 |
diff --git a/sci-mathematics/cvc3/metadata.xml b/sci-mathematics/cvc3/metadata.xml |
283 |
deleted file mode 100644 |
284 |
index cb6781b3e6d..00000000000 |
285 |
--- a/sci-mathematics/cvc3/metadata.xml |
286 |
+++ /dev/null |
287 |
@@ -1,45 +0,0 @@ |
288 |
-<?xml version="1.0" encoding="UTF-8"?> |
289 |
-<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd"> |
290 |
-<pkgmetadata> |
291 |
-<maintainer type="person"> |
292 |
- <email>gienah@g.o</email> |
293 |
- <name>Mark Wright</name> |
294 |
-</maintainer> |
295 |
-<maintainer type="project"> |
296 |
- <email>sci-mathematics@g.o</email> |
297 |
- <name>Gentoo Mathematics Project</name> |
298 |
-</maintainer> |
299 |
-<longdescription lang="en"> |
300 |
-CVC3 is an automatic theorem prover for Satisfiability Modulo Theories |
301 |
-(SMT) problems. It can be used to prove the validity (or, dually, the |
302 |
-satisfiability) of first-order formulas in a large number of built-in |
303 |
-logical theories and their combination. |
304 |
- |
305 |
-CVC3 is the last offspring of a series of popular SMT provers, which |
306 |
-originated at Stanford University with the SVC system. In particular, |
307 |
-it builds on the code base of CVC Lite, its most recent |
308 |
-predecessor. Its high level design follows that of the Sammy prover. |
309 |
- |
310 |
-CVC3 works with a version of first-order logic with polymorphic types |
311 |
-and has a wide variety of features including: |
312 |
- |
313 |
- several built-in base theories: rational and integer linear |
314 |
- arithmetic, arrays, tuples, records, inductive data types, bit |
315 |
- vectors, and equality over uninterpreted function symbols; |
316 |
- support for quantifiers; |
317 |
- an interactive text-based interface; |
318 |
- a rich C and C++ API for embedding in other systems; |
319 |
- proof and model generation abilities; |
320 |
- predicate subtyping; |
321 |
- essentially no limit on its use for research or commercial |
322 |
- purposes (see license). |
323 |
-</longdescription> |
324 |
-<use> |
325 |
- <flag name="isabelle">Add integration support for the Isabelle/HOL |
326 |
- theorem prover.</flag> |
327 |
- <flag name="zchaff">Use the SAT solver zchaff whose copyright is |
328 |
- owned by Princeton University and is more restrictive (see zchaff |
329 |
- license). |
330 |
- </flag> |
331 |
-</use> |
332 |
-</pkgmetadata> |