blob: 63b9fad1839f5d398d462c4278804422c1dc91de (
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
|
# Copyright 1999-2024 Gentoo Authors
# Distributed under the terms of the GNU General Public License v2
EAPI=8
inherit toolchain-funcs
MY_PN="LADR"
typeset -u MY_PV
MY_PV="$(ver_rs 1 '-')"
MY_P="${MY_PN}-${MY_PV}"
DESCRIPTION="Automated theorem prover for first-order and equational logic"
HOMEPAGE="https://www.cs.unm.edu/~mccune/mace4/"
SRC_URI="
https://www.cs.unm.edu/~mccune/mace4/download/${MY_P}.tar.gz
https://dev.gentoo.org/~jlec/distfiles/${MY_PN}-2009-11A-makefile.patch.xz
"
S="${WORKDIR}/${MY_P}/"
LICENSE="GPL-2"
SLOT="0"
KEYWORDS="~amd64 ~x86"
IUSE="examples"
PATCHES=(
"${WORKDIR}/${MY_PN}-2009-11A-makefile.patch"
"${FILESDIR}/${MY_PN}-2009-11A-manpages.patch"
)
src_prepare() {
default
sed -e "/^CC =/s:gcc:$(tc-getCC):g" -i */Makefile || die
export MAKEOPTS+=" -j1 "
tc-export AR CC
}
src_compile() {
emake CFLAGS="${CFLAGS} ${LDFLAGS}" -j1 all
}
src_test() {
LD_LIBRARY_PATH="${S}/ladr/.libs/" emake -j1 test1 test2 test3
}
src_install() {
dobin \
bin/attack \
bin/autosketches4 \
bin/clausefilter \
bin/clausetester \
bin/complex \
bin/directproof \
bin/dprofiles \
bin/fof-prover9 \
bin/gen_trc_defs \
bin/get_givens \
bin/get_interps \
bin/get_kept \
bin/gvizify \
bin/idfilter \
bin/interpfilter \
bin/interpformat \
bin/isofilter \
bin/isofilter0 \
bin/isofilter2 \
bin/ladr_to_tptp \
bin/latfilter \
bin/looper \
bin/mace4 \
bin/miniscope \
bin/mirror-flip \
bin/newauto \
bin/newsax \
bin/olfilter \
bin/perm3 \
bin/proof3fo.xsl \
bin/prooftrans \
bin/prover9 \
bin/renamer \
bin/rewriter \
bin/sigtest \
bin/test_clause_eval \
bin/test_complex \
bin/tptp_to_ladr \
bin/unfast \
bin/upper-covers
doman \
manpages/interpformat.1 \
manpages/isofilter.1 \
manpages/prooftrans.1 \
manpages/mace4.1 \
manpages/prover9.1 \
manpages/clausefilter.1 \
manpages/clausetester.1 \
manpages/interpfilter.1 \
manpages/rewriter.1 \
manpages/prover9-apps.1
docinto html
dodoc -r ladr/index.html.master ladr/html/*
insinto "/usr/$(get_libdir)"
dolib.so ladr/.libs/libladr.so.4.0.0
dosym libladr.so.4.0.0 "/usr/$(get_libdir)/libladr.so.4"
dosym libladr.so.4.0.0 "/usr/$(get_libdir)/libladr.so"
insinto /usr/include/ladr
doins ladr/*.h
if use examples ; then
insinto "/usr/share/${PN}/examples"
doins prover9.examples/*
# The prover9-mace4 script is installed as an example script
# to avoid confusion with the GUI sci-mathematics/p9m4 prover9mace4.py
insinto "/usr/share/${PN}/scripts"
doins bin/prover9-mace4
fi
}
|
GitWeb