| 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 |
|
|
} |
Parent Directory
| 
Revision Log