1 |
commit: 71d6af007ea0f4ed26ab0233600401fdb3bfcc6b |
2 |
Author: Mark Wright <gienah <AT> gentoo <DOT> org> |
3 |
AuthorDate: Mon Jan 2 23:07:12 2017 +0000 |
4 |
Commit: Mark Wright <gienah <AT> gentoo <DOT> org> |
5 |
CommitDate: Mon Jan 2 23:07:12 2017 +0000 |
6 |
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=71d6af00 |
7 |
|
8 |
sci-mathematics/spass: Bump to 3.9 |
9 |
|
10 |
Package-Manager: portage-2.3.3 |
11 |
|
12 |
sci-mathematics/spass/Manifest | 1 + |
13 |
sci-mathematics/spass/spass-3.7.ebuild | 3 +- |
14 |
sci-mathematics/spass/spass-3.9.ebuild | 146 +++++++++++++++++++++++++++++++++ |
15 |
3 files changed, 149 insertions(+), 1 deletion(-) |
16 |
|
17 |
diff --git a/sci-mathematics/spass/Manifest b/sci-mathematics/spass/Manifest |
18 |
index 5fb1372..f1d7eaa 100644 |
19 |
--- a/sci-mathematics/spass/Manifest |
20 |
+++ b/sci-mathematics/spass/Manifest |
21 |
@@ -1 +1,2 @@ |
22 |
DIST spass37.tgz 1340925 SHA256 13c67e5e09b814ba50f38a391fe653661ba714e7541ffd4951efef91274aaacc SHA512 5b4efd7b767dfee3f24e7917a6ec58ac240ab33bf601722eabd50af57637d8fdd62de9e34e7cd1cd98b8b7e371c9e2d47c8fa3e07c6e7ce2fa616a76646a4e12 WHIRLPOOL 2fa8881b08a0fcdb9f1a6e7d27849f5c900a32f2cb27d878fbdae4986d0854608fd137e4608349c4eb612f4e1981142e63af8462ab904f7d08c3e2758f319835 |
23 |
+DIST spass39.tgz 554633 SHA256 1797c3fbd1954189c812fbab7927880bad964ded400bae733a9938c7e6b09e85 SHA512 d7ea0697426c476f2e03b2f9078b7e060671067a67fad7144bb5887a2dd3f39e19e1888f121fce546b5d6ea9a4dc458d1cbec56b59c93507e7dc2d0afa25a89b WHIRLPOOL ad69c2e3714c5c640898a71a47ad6ab8370d3dd568372d492e82e6ba17312e84d3885016db3f923a4d7b3967cb0ac65c8e9dd8f0c8ce93f9de0534be01a371aa |
24 |
|
25 |
diff --git a/sci-mathematics/spass/spass-3.7.ebuild b/sci-mathematics/spass/spass-3.7.ebuild |
26 |
index 30967c7..7556028 100644 |
27 |
--- a/sci-mathematics/spass/spass-3.7.ebuild |
28 |
+++ b/sci-mathematics/spass/spass-3.7.ebuild |
29 |
@@ -1,4 +1,4 @@ |
30 |
-# Copyright 1999-2012 Gentoo Foundation |
31 |
+# Copyright 1999-2017 Gentoo Foundation |
32 |
# Distributed under the terms of the GNU General Public License v2 |
33 |
# $Id$ |
34 |
|
35 |
@@ -40,6 +40,7 @@ src_install() { |
36 |
fi |
37 |
|
38 |
if use isabelle; then |
39 |
+ ewarn "All open source versions of spass are broken with Isabelle 2016.1" |
40 |
ISABELLE_HOME="$(isabelle getenv ISABELLE_HOME | cut -d'=' -f 2)" |
41 |
[[ -n "${ISABELLE_HOME}" ]] || die "ISABELLE_HOME empty" |
42 |
dodir "${ISABELLE_HOME}/contrib/${PN}-${PV}/etc" |
43 |
|
44 |
diff --git a/sci-mathematics/spass/spass-3.9.ebuild b/sci-mathematics/spass/spass-3.9.ebuild |
45 |
new file mode 100644 |
46 |
index 00000000..1804581 |
47 |
--- /dev/null |
48 |
+++ b/sci-mathematics/spass/spass-3.9.ebuild |
49 |
@@ -0,0 +1,146 @@ |
50 |
+# Copyright 1999-2017 Gentoo Foundation |
51 |
+# Distributed under the terms of the GNU General Public License v2 |
52 |
+# $Id$ |
53 |
+ |
54 |
+EAPI=6 |
55 |
+ |
56 |
+inherit versionator |
57 |
+ |
58 |
+MY_PV=$(delete_all_version_separators "${PV}") |
59 |
+MY_P="${PN}${MY_PV}" |
60 |
+ |
61 |
+DESCRIPTION="An Automated Theorem Prover for First-Order Logic with Equality" |
62 |
+HOMEPAGE="http://www.spass-prover.org/" |
63 |
+SRC_URI="http://www.spass-prover.org/download/sources/${MY_P}.tgz" |
64 |
+ |
65 |
+LICENSE="BSD-2" |
66 |
+SLOT="0/${PV}" |
67 |
+KEYWORDS="~amd64 ~x86" |
68 |
+IUSE="isabelle" |
69 |
+ |
70 |
+RDEPEND="isabelle? ( |
71 |
+ sci-mathematics/isabelle:= |
72 |
+ )" |
73 |
+DEPEND="${RDEPEND}" |
74 |
+ |
75 |
+src_unpack() { |
76 |
+ mkdir -p "${P}" || die |
77 |
+ cd "${S}" || die |
78 |
+ unpack "${MY_P}.tgz" |
79 |
+} |
80 |
+ |
81 |
+src_compile() { |
82 |
+ einfo "generating parsers" |
83 |
+ bison -d -p pro_ -o proparser.c proparser.y || die |
84 |
+ bison -d -p tptp_ -o tptpparser.c tptpparser.y || die |
85 |
+ bison -d -p ia_ -o iaparser.c iaparser.y || die |
86 |
+ |
87 |
+ einfo "generating lexers" |
88 |
+ flex -Ppro_ -o proscanner.c proscanner.l || die |
89 |
+ flex -Ptptp_ -o tptpscanner.c tptpscanner.l || die |
90 |
+ flex -Pia_ -o iascanner.c iascanner.l || die |
91 |
+ |
92 |
+ einfo "compiling sources" |
93 |
+ local x |
94 |
+ for x in *.c |
95 |
+ do |
96 |
+ $(tc-getCC) \ |
97 |
+ ${CPPFLAGS} ${CFLAGS} \ |
98 |
+ -c -o ${x/.c/.o} ${x} || die "compile ${x} failed" |
99 |
+ done |
100 |
+ |
101 |
+ einfo "linking tptp2dfg" |
102 |
+ $(tc-getCC) \ |
103 |
+ ${LDFLAGS} -o tptp2dfg \ |
104 |
+ array.o clause.o cmdline.o context.o description.o dfg_diagnostic.o \ |
105 |
+ dfg_string_table.o dfg_token.o dfgparser.o dfglexer.o \ |
106 |
+ tptpparser.o tptpscanner.o eml.o flags.o foldfg.o hashmap.o kbo.o \ |
107 |
+ list.o memory.o misc.o order.o rpos.o sharing.o st.o stack.o \ |
108 |
+ strings.o subst.o symbol.o term.o unify.o tptp2dfg.o -lm \ |
109 |
+ || die "link tptp2dfg failed" |
110 |
+ |
111 |
+ einfo "linking dfg2ascii" |
112 |
+ $(tc-getCC) \ |
113 |
+ ${LDFLAGS} -o dfg2ascii \ |
114 |
+ array.o clause.o cmdline.o context.o description.o dfg_diagnostic.o \ |
115 |
+ dfg_string_table.o dfg_token.o dfgparser.o dfglexer.o \ |
116 |
+ tptpparser.o tptpscanner.o eml.o flags.o foldfg.o hashmap.o kbo.o \ |
117 |
+ list.o memory.o misc.o order.o rpos.o sharing.o st.o stack.o \ |
118 |
+ strings.o subst.o symbol.o term.o unify.o dfg2ascii.o -lm \ |
119 |
+ || die "link dfg2ascii failed" |
120 |
+ |
121 |
+ einfo "linking dfg2dfg" |
122 |
+ $(tc-getCC) \ |
123 |
+ ${LDFLAGS} -o dfg2dfg \ |
124 |
+ array.o clause.o cmdline.o context.o description.o dfg_diagnostic.o \ |
125 |
+ dfg_string_table.o dfg_token.o dfgparser.o dfglexer.o \ |
126 |
+ tptpparser.o tptpscanner.o eml.o flags.o foldfg.o hashmap.o kbo.o \ |
127 |
+ list.o memory.o misc.o order.o rpos.o sharing.o st.o stack.o \ |
128 |
+ strings.o subst.o symbol.o term.o unify.o approx.o dfg2dfg.o -lm \ |
129 |
+ || die "link dfg2dfg failed" |
130 |
+ |
131 |
+ einfo "linking SPASS" |
132 |
+ $(tc-getCC) \ |
133 |
+ ${LDFLAGS} -o SPASS \ |
134 |
+ array.o clause.o cmdline.o context.o description.o dfg_diagnostic.o \ |
135 |
+ dfg_string_table.o dfg_token.o dfgparser.o dfglexer.o \ |
136 |
+ tptpparser.o tptpscanner.o eml.o flags.o foldfg.o hashmap.o kbo.o \ |
137 |
+ list.o memory.o misc.o order.o rpos.o sharing.o st.o stack.o \ |
138 |
+ strings.o subst.o symbol.o term.o unify.o analyze.o clock.o \ |
139 |
+ closure.o cnf.o component.o condensing.o defs.o doc-proof.o graph.o \ |
140 |
+ hash.o hasharray.o iaparser.o iascanner.o partition.o proofcheck.o \ |
141 |
+ ras.o renaming.o resolution.o rules-inf.o rules-red.o rules-sort.o \ |
142 |
+ rules-split.o rules-ur.o search.o sort.o subsumption.o table.o \ |
143 |
+ tableau.o terminator.o top.o vector.o -lm \ |
144 |
+ || die "link SPASS failed" |
145 |
+} |
146 |
+ |
147 |
+src_install() { |
148 |
+ exeinto /usr/bin |
149 |
+ local x |
150 |
+ for x in tptp2dfg dfg2ascii dfg2dfg SPASS |
151 |
+ do |
152 |
+ doexe ${x} |
153 |
+ done |
154 |
+ |
155 |
+ if use isabelle; then |
156 |
+ ewarn "All open source versions of spass are broken with Isabelle 2016.1" |
157 |
+ ISABELLE_HOME="$(isabelle getenv ISABELLE_HOME | cut -d'=' -f 2)" |
158 |
+ [[ -n "${ISABELLE_HOME}" ]] || die "ISABELLE_HOME empty" |
159 |
+ dodir "${ISABELLE_HOME}/contrib/${PN}-${PV}/etc" |
160 |
+ cat <<- EOF >> "${S}/settings" |
161 |
+ SPASS_HOME="${ROOT}usr/bin" |
162 |
+ SPASS_VERSION="${PV}" |
163 |
+ EOF |
164 |
+ insinto "${ISABELLE_HOME}/contrib/${PN}-${PV}/etc" |
165 |
+ doins "${S}/settings" |
166 |
+ fi |
167 |
+} |
168 |
+ |
169 |
+pkg_postinst() { |
170 |
+ if use isabelle; then |
171 |
+ if [ -f "${ROOT}etc/isabelle/components" ]; then |
172 |
+ if egrep "contrib/${PN}-[0-9.]*" "${ROOT}etc/isabelle/components"; then |
173 |
+ sed -e "/contrib\/${PN}-[0-9.]*/d" \ |
174 |
+ -i "${ROOT}etc/isabelle/components" |
175 |
+ fi |
176 |
+ cat <<- EOF >> "${ROOT}etc/isabelle/components" |
177 |
+ contrib/${PN}-${PV} |
178 |
+ EOF |
179 |
+ fi |
180 |
+ fi |
181 |
+} |
182 |
+ |
183 |
+pkg_postrm() { |
184 |
+ if use isabelle; then |
185 |
+ if [ ! -f "${ROOT}usr/bin/SPASS" ]; then |
186 |
+ if [ -f "${ROOT}etc/isabelle/components" ]; then |
187 |
+ # Note: this sed should only match the version of this ebuild |
188 |
+ # Which is what we want as we do not want to remove the line |
189 |
+ # of a new spass being installed during an upgrade. |
190 |
+ sed -e "/contrib\/${PN}-${PV}/d" \ |
191 |
+ -i "${ROOT}etc/isabelle/components" |
192 |
+ fi |
193 |
+ fi |
194 |
+ fi |
195 |
+} |