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
147
148
149
150
151
152
153
154
155
156
157
|
# Copyright 1999-2012 Gentoo Foundation
# Distributed under the terms of the GNU General Public License v2
# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/cvc3/cvc3-2.4.1.ebuild,v 1.4 2012/12/05 10:18:57 gienah Exp $
EAPI="5"
inherit elisp-common
DESCRIPTION="CVC3 is an automatic theorem prover for Satisfiability Modulo Theories (SMT) problems"
HOMEPAGE="http://www.cs.nyu.edu/acsys/cvc3/index.html"
SRC_URI="http://www.cs.nyu.edu/acsys/cvc3/releases/2.4.1/${P}.tar.gz"
LICENSE="BSD MIT as-is zchaff? ( zchaff )"
RESTRICT="mirror zchaff? ( bindist )"
SLOT="0/${PV}"
KEYWORDS="~amd64 ~x86"
IUSE="doc emacs isabelle test zchaff"
RDEPEND="dev-libs/gmp
isabelle? (
>=sci-mathematics/isabelle-2011.1-r1:=
)"
DEPEND="${RDEPEND}
doc? (
app-doc/doxygen
media-gfx/graphviz
)
emacs? (
virtual/emacs
)"
SITEFILE=50${PN}-gentoo.el
src_prepare() {
sed -e 's#prefix=@prefix@#prefix=$(patsubst %/,%,$(DESTDIR))@prefix@#' \
-e 's#libdir=@libdir@#libdir=$(patsubst %/,%,$(DESTDIR))@libdir@#' \
-e 's#mandir=@mandir@#mandir=$(patsubst %/,%,$(DESTDIR))@mandir@#' \
-i "${S}/Makefile.local.in" \
|| die "Could not set DESTDIR in Makefile.local.in"
}
src_configure() {
# --enable-static disables building of shared libraries, statically
# links /usr/bin/cvc3 and installs static libraries.
# --enable-static --enable-sharedlibs behaves the same as just --enable-static
econf \
--enable-dynamic \
$(use_enable zchaff)
if use test; then
sed -e 's@LD_LIBS = @LD_LIBS = -L'"${S}"'/lib -Wl,-R'"${S}"'/lib @' \
-i "${S}/test/Makefile" \
|| die "Could not set library paths in test/Makefile"
fi
}
src_compile() {
emake
if use doc; then
pushd doc || die "Could not cd to doc"
emake
popd
fi
if use emacs ; then
pushd "${S}/emacs" || die "Could change directory to emacs"
elisp-compile *.el || die "emacs elisp compile failed"
popd
fi
if use test; then
pushd test || die "Could not cd to test"
emake
popd
fi
}
src_test() {
pushd test || die "Could not cd to test"
./bin/test || die "tests failed"
popd
}
src_install() {
emake DESTDIR="${D}" install
if use doc; then
pushd "${S}"/doc/html || die "Could not cd to doc/html"
dohtml *.html
insinto /usr/share/doc/${PF}/html
doins *.css *.gif *.png
popd
fi
if use emacs ; then
elisp-install ${PN} emacs/*.{el,elc}
cp "${FILESDIR}"/${SITEFILE} "${S}"
elisp-site-file-install ${SITEFILE}
fi
if use isabelle; then
ISABELLE_HOME="$(isabelle getenv ISABELLE_HOME | cut -d'=' -f 2)" \
|| die "isabelle getenv ISABELLE_HOME failed"
[[ -n "${ISABELLE_HOME}" ]] || die "ISABELLE_HOME empty"
dodir "${ISABELLE_HOME}/contrib/${PN}-${PV}/etc"
cat <<- EOF >> "${S}/settings"
CVC3_COMPONENT="\$COMPONENT"
CVC3_HOME="${ROOT}usr/bin"
CVC3_SOLVER="\$CVC3_HOME/cvc3"
CVC3_REMOTE_SOLVER="cvc3"
CVC3_INSTALLED="yes"
EOF
insinto "${ISABELLE_HOME}/contrib/${PN}-${PV}/etc"
doins "${S}/settings"
fi
}
pkg_postinst() {
use emacs && elisp-site-regen
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
if use zchaff; then
einfo "This copy of CVC3 is also configured to use the SAT solver zchaff whose"
einfo "copyright is owned by Princeton University and is more restrictive."
einfo "Specifically, it may be used for internal, noncommercial, research purposes"
einfo "only. See the copyright notices from the zchaff source files which are"
einfo "included in the LICENSE file."
einfo "To build CVC3 without these files, please build cvc3 without the zchaff"
einfo "use flag (note: zchaff is disabled by default):"
einfo "USE=-zchaff emerge sci-mathemathematics/cvc3"
fi
}
pkg_postrm() {
use emacs && elisp-site-regen
if use isabelle; then
if [ ! -f "${ROOT}usr/bin/cvc3" ]; 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 CVC3 being installed during an upgrade.
sed -e "/contrib\/${PN}-${PV}/d" \
-i "${ROOT}etc/isabelle/components"
fi
fi
fi
}
|
GitWeb