summaryrefslogtreecommitdiff
path: root/sci-mathematics/isabelle/isabelle-2009.ebuild
diff options
context:
space:
mode:
authorRené 'Necoro' Neumann <necoro@necoro.net>2009-09-28 18:58:55 +0200
committerRené 'Necoro' Neumann <necoro@necoro.net>2009-09-28 18:58:55 +0200
commite1a68a8c00d2b7f4ed09578305917a1595faebb4 (patch)
treed0fc9a4b05f201835282c403b88938a5730f68e9 /sci-mathematics/isabelle/isabelle-2009.ebuild
parent62580ba14d004b3611f4ea14accf1f47fe14922e (diff)
downloadoverlay-e1a68a8c00d2b7f4ed09578305917a1595faebb4.tar.gz
overlay-e1a68a8c00d2b7f4ed09578305917a1595faebb4.tar.bz2
overlay-e1a68a8c00d2b7f4ed09578305917a1595faebb4.zip
Add isabelle ebuild
Diffstat (limited to '')
-rw-r--r--sci-mathematics/isabelle/isabelle-2009.ebuild102
1 files changed, 102 insertions, 0 deletions
diff --git a/sci-mathematics/isabelle/isabelle-2009.ebuild b/sci-mathematics/isabelle/isabelle-2009.ebuild
new file mode 100644
index 0000000..f483bda
--- /dev/null
+++ b/sci-mathematics/isabelle/isabelle-2009.ebuild
@@ -0,0 +1,102 @@
+# Copyright 1999-2009 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Header: $
+
+EAPI="2"
+
+inherit eutils multilib
+
+DESCRIPTION="Isabelle is a generic proof assistant"
+HOMEPAGE="http://isabelle.in.tum.de/ http://www.cl.cam.ac.uk/research/hvg/Isabelle/"
+SRC_URI="http://isabelle.in.tum.de/dist/Isabelle${PV}.tar.gz"
+
+LICENSE="BSD"
+SLOT="0"
+KEYWORDS="~x86 ~amd64"
+IUSE="doc graphbrowsing +proofgeneral"
+
+
+#upstream says
+#bash 2.x/3.x, Poly/ML 5.x, Perl 5.x,
+#for Proof General GNU Emacs 21/22, xemacs 21.4.x, NOT xemacs 21.5 beta
+#for document preparation: complete LaTeX
+DEPEND=">=app-shells/bash-3.0
+ graphbrowsing? (
+ virtual/jdk
+ )"
+
+#proofgeneral uses eclass elisp that depends on virtual/emacs-21
+RDEPEND=">=dev-lang/polyml-5.2.1
+ >=dev-lang/perl-5.8.8-r2
+ doc? (
+ virtual/latex-base
+ )
+ proofgeneral? (
+ app-emacs/proofgeneral
+ )
+ ${DEPEND}"
+
+S="${WORKDIR}"/Isabelle${PV}
+TARGETDIR="/usr/share/Isabelle"${PV}
+LIBDIR="/usr/"$(get_libdir)"/Isabelle"${PV}
+
+pkg_setup() {
+ if ! use proofgeneral
+ then
+ ewarn "You have deselected the Proof General interface."
+ ewarn "Only a text terminal will be installed."
+ ewarn "Emerge Isabelle with the proofgeneral USE flag enabled"
+ ewarn "to get the common interface, that most people want."
+ fi
+}
+
+src_prepare() {
+ use proofgeneral && epatch ${FILESDIR}/isabelle-2009-proofgeneral-gentoo-path.patch
+}
+
+src_compile() {
+ einfo "Building Isabelle logics. This may take some time."
+ ./build -b || die "building logics failed"
+ if use graphbrowsing
+ then
+ cd lib/browser
+ emake clean || die "failed cleaning graph browser directory"
+ emake || die "failed building the graph browser"
+ fi
+}
+
+src_test() {
+ einfo "Running tests. A test run can take up to several hours!"
+ ./build -b HOL -t
+}
+
+src_install() {
+ exeinto ${TARGETDIR}/bin
+ doexe bin/isabelle-process bin/isabelle \
+ || die "install failed"
+
+ exeinto ${TARGETDIR}
+ doexe build || die "install failed"
+
+ insinto ${TARGETDIR}
+ use doc && ( doins -r doc || die "install failed" )
+
+ doins -r etc || die "install failed"
+ dosym ${LIBDIR}/heaps ${TARGETDIR}/heaps
+
+ insinto ${LIBDIR}
+ doins -r heaps || die "install failed"
+
+ # use cp to keep file attributes
+ cp -R lib ${D}${TARGETDIR} || die "install failed"
+
+ bin/isabelle install -d ${TARGETDIR} -p ${D}usr/bin
+ newicon lib/icons/isabelle.xpm ${PN}.xpm
+ make_desktop_entry Isabelle "Isabelle ${PV}" isabelle.xpm "Education;Math"
+ dodoc ANNOUNCE CONTRIBUTORS INSTALL NEWS README \
+ || die "dodoc failed"
+}
+
+pkg_postinst() {
+ elog "You will need to re-emerge Isabelle after emerging polyml."
+}