1 |
gienah |
1.1 |
# Copyright 1999-2012 Gentoo Foundation |
2 |
|
|
# Distributed under the terms of the GNU General Public License v2 |
3 |
|
|
# $Header: $ |
4 |
|
|
|
5 |
|
|
EAPI="4" |
6 |
|
|
|
7 |
|
|
JAVA_PKG_OPT_USE="graphbrowsing" |
8 |
|
|
inherit eutils java-pkg-opt-2 multilib versionator |
9 |
|
|
|
10 |
|
|
MY_PN="Isabelle" |
11 |
|
|
typeset -u MY_PV |
12 |
|
|
MY_PV=$(replace_all_version_separators '-') |
13 |
|
|
MY_P="${MY_PN}${MY_PV}" |
14 |
|
|
|
15 |
|
|
DESCRIPTION="Isabelle is a generic proof assistant" |
16 |
|
|
HOMEPAGE="http://www.cl.cam.ac.uk/research/hvg/isabelle/index.html" |
17 |
|
|
SRC_URI="http://www.cl.cam.ac.uk/research/hvg/isabelle/dist/${MY_P}.tar.gz" |
18 |
|
|
|
19 |
|
|
LICENSE="BSD" |
20 |
|
|
SLOT="0" |
21 |
|
|
KEYWORDS="~x86 ~amd64" |
22 |
|
|
ALL_LOGICS="Pure FOL +HOL ZF CCL CTT Cube FOLP LCF Sequents" |
23 |
|
|
IUSE="${ALL_LOGICS} doc graphbrowsing +pdf +proofgeneral" |
24 |
|
|
|
25 |
|
|
#upstream says |
26 |
|
|
#bash 2.x/3.x, Poly/ML 5.x, Perl 5.x, |
27 |
|
|
#for document preparation: complete LaTeX |
28 |
|
|
DEPEND=">=app-shells/bash-3.0 |
29 |
|
|
>=dev-lang/polyml-5.4.1 |
30 |
|
|
>=dev-lang/perl-5.8.8-r2" |
31 |
|
|
|
32 |
|
|
RDEPEND="doc? ( |
33 |
|
|
virtual/latex-base |
34 |
|
|
dev-tex/rail |
35 |
|
|
) |
36 |
|
|
pdf? ( || ( app-text/xpdf |
37 |
|
|
app-text/gv |
38 |
|
|
app-text/gsview |
39 |
|
|
app-text/epdfview |
40 |
|
|
app-text/acroread |
41 |
|
|
app-text/zathura ) |
42 |
|
|
) |
43 |
|
|
proofgeneral? ( |
44 |
|
|
app-emacs/proofgeneral |
45 |
|
|
) |
46 |
|
|
${DEPEND}" |
47 |
|
|
|
48 |
|
|
S="${WORKDIR}"/Isabelle${MY_PV} |
49 |
|
|
TARGETDIR="/usr/share/Isabelle"${MY_PV} |
50 |
|
|
LIBDIR="/usr/"$(get_libdir)"/Isabelle"${MY_PV} |
51 |
|
|
|
52 |
|
|
pkg_setup() { |
53 |
|
|
java-pkg-opt-2_pkg_setup |
54 |
|
|
if ! use proofgeneral |
55 |
|
|
then |
56 |
|
|
ewarn "You have deselected the Proof General interface." |
57 |
|
|
ewarn "Only a text terminal will be installed." |
58 |
|
|
ewarn "Emerge Isabelle with the proofgeneral USE flag enabled" |
59 |
|
|
ewarn "to get the common interface, that most people want." |
60 |
|
|
fi |
61 |
|
|
} |
62 |
|
|
|
63 |
|
|
src_prepare() { |
64 |
|
|
java-pkg-opt-2_src_prepare |
65 |
|
|
if use proofgeneral; then |
66 |
|
|
epatch "${FILESDIR}/${PN}-2011.1-proofgeneral-gentoo-path.patch" |
67 |
|
|
polymlver=$(poly -v | cut -d' ' -f2) |
68 |
|
|
polymlarch=$(poly -v | cut -d' ' -f9 | cut -d'-' -f1) |
69 |
|
|
sed -e "s@5.4.0@${polymlver}@g" \ |
70 |
|
|
-i "${S}/etc/settings" || die "Could not configure polyml version in etc/settings" |
71 |
|
|
sed -e "s@x86_64@${polymlarch}@g" \ |
72 |
|
|
-i "${S}/etc/settings" || die "Could not configure polyml arch in etc/settings" |
73 |
|
|
fi |
74 |
|
|
if use graphbrowsing; then |
75 |
|
|
epatch "${FILESDIR}/${PN}-2011.1-graphbrowser.patch" |
76 |
|
|
fi |
77 |
|
|
} |
78 |
|
|
|
79 |
|
|
src_compile() { |
80 |
|
|
LOGICS="" |
81 |
|
|
for l in "${ALL_LOGICS}"; do |
82 |
|
|
if has "${l/+/}"; then |
83 |
|
|
LOGICS="${LOGICS} ${l/+/}" |
84 |
|
|
fi |
85 |
|
|
done |
86 |
|
|
einfo "Building Isabelle logics ${LOGICS}. This may take some time." |
87 |
|
|
./build -b -i "${LOGICS}" || die "building logics failed" |
88 |
|
|
./bin/isabelle makeall || die "isabelle makeall failed" |
89 |
|
|
if use graphbrowsing |
90 |
|
|
then |
91 |
|
|
rm -f "${S}/lib/browser/GraphBrowser.jar" || die "failed cleaning graph browser directory" |
92 |
|
|
cd "${S}/lib/browser" |
93 |
|
|
./build || die "failed building the graph browser" |
94 |
|
|
cd "${S}" |
95 |
|
|
fi |
96 |
|
|
} |
97 |
|
|
|
98 |
|
|
src_test() { |
99 |
|
|
einfo "Running tests. A test run can take up to several hours!" |
100 |
|
|
./build -b -t |
101 |
|
|
} |
102 |
|
|
|
103 |
|
|
src_install() { |
104 |
|
|
exeinto ${TARGETDIR}/bin |
105 |
|
|
doexe bin/isabelle-process bin/isabelle |
106 |
|
|
|
107 |
|
|
exeinto ${TARGETDIR} |
108 |
|
|
doexe build |
109 |
|
|
|
110 |
|
|
insinto ${TARGETDIR} |
111 |
|
|
doins -r src |
112 |
|
|
dodoc -r doc |
113 |
|
|
|
114 |
|
|
dodir /etc/isabelle |
115 |
|
|
insinto /etc/isabelle |
116 |
|
|
doins -r etc |
117 |
|
|
|
118 |
|
|
dosym /etc/isabelle "${TARGETDIR}/etc" |
119 |
|
|
dosym "${LIBDIR}/heaps" "${TARGETDIR}/heaps" |
120 |
|
|
|
121 |
|
|
insinto ${LIBDIR} |
122 |
|
|
doins -r heaps |
123 |
|
|
|
124 |
|
|
# use cp to keep file attributes |
125 |
|
|
cp -R lib "${ED}${TARGETDIR}" || die "install lib failed" |
126 |
|
|
|
127 |
|
|
bin/isabelle install -d ${TARGETDIR} -p "${ED}usr/bin" \ |
128 |
|
|
|| die "isabelle install failed" |
129 |
|
|
newicon lib/icons/isabelle.xpm "${PN}.xpm" |
130 |
|
|
dodoc ANNOUNCE CONTRIBUTORS COPYRIGHT NEWS README |
131 |
|
|
|
132 |
|
|
java-pkg_regjar \ |
133 |
|
|
"${ED}${TARGETDIR}/lib/browser/GraphBrowser.jar" \ |
134 |
|
|
"${ED}${TARGETDIR}/lib/classes/ext/Pure.jar" \ |
135 |
|
|
"${ED}${TARGETDIR}/lib/classes/ext/scala-library.jar" \ |
136 |
|
|
"${ED}${TARGETDIR}/lib/classes/ext/scala-swing.jar" \ |
137 |
|
|
"${ED}${TARGETDIR}/lib/classes/java_ext_dirs.jar" |
138 |
|
|
} |
139 |
|
|
|
140 |
|
|
pkg_postinst() { |
141 |
|
|
elog "You will need to re-emerge Isabelle after emerging polyml." |
142 |
|
|
if use pdf; then |
143 |
|
|
einfo "Please configure your preferred pdf viewer by editing" |
144 |
|
|
einfo "the PDF_VIEWER variable in the system settings file" |
145 |
|
|
einfo "/etc/conf/isabelle and/or the user settings file" |
146 |
|
|
einfo "\$HOME/.isabelle/${MY_P}" |
147 |
|
|
fi |
148 |
|
|
} |