blob: 1804581ff3dc0fc48b4c80eedc0ebccba1ddbbe2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
|
# Copyright 1999-2017 Gentoo Foundation
# Distributed under the terms of the GNU General Public License v2
# $Id$
EAPI=6
inherit versionator
MY_PV=$(delete_all_version_separators "${PV}")
MY_P="${PN}${MY_PV}"
DESCRIPTION="An Automated Theorem Prover for First-Order Logic with Equality"
HOMEPAGE="http://www.spass-prover.org/"
SRC_URI="http://www.spass-prover.org/download/sources/${MY_P}.tgz"
LICENSE="BSD-2"
SLOT="0/${PV}"
KEYWORDS="~amd64 ~x86"
IUSE="isabelle"
RDEPEND="isabelle? (
sci-mathematics/isabelle:=
)"
DEPEND="${RDEPEND}"
src_unpack() {
mkdir -p "${P}" || die
cd "${S}" || die
unpack "${MY_P}.tgz"
}
src_compile() {
einfo "generating parsers"
bison -d -p pro_ -o proparser.c proparser.y || die
bison -d -p tptp_ -o tptpparser.c tptpparser.y || die
bison -d -p ia_ -o iaparser.c iaparser.y || die
einfo "generating lexers"
flex -Ppro_ -o proscanner.c proscanner.l || die
flex -Ptptp_ -o tptpscanner.c tptpscanner.l || die
flex -Pia_ -o iascanner.c iascanner.l || die
einfo "compiling sources"
local x
for x in *.c
do
$(tc-getCC) \
${CPPFLAGS} ${CFLAGS} \
-c -o ${x/.c/.o} ${x} || die "compile ${x} failed"
done
einfo "linking tptp2dfg"
$(tc-getCC) \
${LDFLAGS} -o tptp2dfg \
array.o clause.o cmdline.o context.o description.o dfg_diagnostic.o \
dfg_string_table.o dfg_token.o dfgparser.o dfglexer.o \
tptpparser.o tptpscanner.o eml.o flags.o foldfg.o hashmap.o kbo.o \
list.o memory.o misc.o order.o rpos.o sharing.o st.o stack.o \
strings.o subst.o symbol.o term.o unify.o tptp2dfg.o -lm \
|| die "link tptp2dfg failed"
einfo "linking dfg2ascii"
$(tc-getCC) \
${LDFLAGS} -o dfg2ascii \
array.o clause.o cmdline.o context.o description.o dfg_diagnostic.o \
dfg_string_table.o dfg_token.o dfgparser.o dfglexer.o \
tptpparser.o tptpscanner.o eml.o flags.o foldfg.o hashmap.o kbo.o \
list.o memory.o misc.o order.o rpos.o sharing.o st.o stack.o \
strings.o subst.o symbol.o term.o unify.o dfg2ascii.o -lm \
|| die "link dfg2ascii failed"
einfo "linking dfg2dfg"
$(tc-getCC) \
${LDFLAGS} -o dfg2dfg \
array.o clause.o cmdline.o context.o description.o dfg_diagnostic.o \
dfg_string_table.o dfg_token.o dfgparser.o dfglexer.o \
tptpparser.o tptpscanner.o eml.o flags.o foldfg.o hashmap.o kbo.o \
list.o memory.o misc.o order.o rpos.o sharing.o st.o stack.o \
strings.o subst.o symbol.o term.o unify.o approx.o dfg2dfg.o -lm \
|| die "link dfg2dfg failed"
einfo "linking SPASS"
$(tc-getCC) \
${LDFLAGS} -o SPASS \
array.o clause.o cmdline.o context.o description.o dfg_diagnostic.o \
dfg_string_table.o dfg_token.o dfgparser.o dfglexer.o \
tptpparser.o tptpscanner.o eml.o flags.o foldfg.o hashmap.o kbo.o \
list.o memory.o misc.o order.o rpos.o sharing.o st.o stack.o \
strings.o subst.o symbol.o term.o unify.o analyze.o clock.o \
closure.o cnf.o component.o condensing.o defs.o doc-proof.o graph.o \
hash.o hasharray.o iaparser.o iascanner.o partition.o proofcheck.o \
ras.o renaming.o resolution.o rules-inf.o rules-red.o rules-sort.o \
rules-split.o rules-ur.o search.o sort.o subsumption.o table.o \
tableau.o terminator.o top.o vector.o -lm \
|| die "link SPASS failed"
}
src_install() {
exeinto /usr/bin
local x
for x in tptp2dfg dfg2ascii dfg2dfg SPASS
do
doexe ${x}
done
if use isabelle; then
ewarn "All open source versions of spass are broken with Isabelle 2016.1"
ISABELLE_HOME="$(isabelle getenv ISABELLE_HOME | cut -d'=' -f 2)"
[[ -n "${ISABELLE_HOME}" ]] || die "ISABELLE_HOME empty"
dodir "${ISABELLE_HOME}/contrib/${PN}-${PV}/etc"
cat <<- EOF >> "${S}/settings"
SPASS_HOME="${ROOT}usr/bin"
SPASS_VERSION="${PV}"
EOF
insinto "${ISABELLE_HOME}/contrib/${PN}-${PV}/etc"
doins "${S}/settings"
fi
}
pkg_postinst() {
if use isabelle; then
if [ -f "${ROOT}etc/isabelle/components" ]; then
if egrep "contrib/${PN}-[0-9.]*" "${ROOT}etc/isabelle/components"; then
sed -e "/contrib\/${PN}-[0-9.]*/d" \
-i "${ROOT}etc/isabelle/components"
fi
cat <<- EOF >> "${ROOT}etc/isabelle/components"
contrib/${PN}-${PV}
EOF
fi
fi
}
pkg_postrm() {
if use isabelle; then
if [ ! -f "${ROOT}usr/bin/SPASS" ]; then
if [ -f "${ROOT}etc/isabelle/components" ]; then
# Note: this sed should only match the version of this ebuild
# Which is what we want as we do not want to remove the line
# of a new spass being installed during an upgrade.
sed -e "/contrib\/${PN}-${PV}/d" \
-i "${ROOT}etc/isabelle/components"
fi
fi
fi
}
|
GitWeb