summaryrefslogtreecommitdiff
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
}