From e1a68a8c00d2b7f4ed09578305917a1595faebb4 Mon Sep 17 00:00:00 2001
From: René 'Necoro' Neumann <necoro@necoro.net>
Date: Mon, 28 Sep 2009 18:58:55 +0200
Subject: Add isabelle ebuild

---
 sci-mathematics/isabelle/Manifest                  |   3 +
 .../isabelle-2009-proofgeneral-gentoo-path.patch   |  10 ++
 sci-mathematics/isabelle/isabelle-2009.ebuild      | 102 +++++++++++++++++++++
 3 files changed, 115 insertions(+)
 create mode 100644 sci-mathematics/isabelle/Manifest
 create mode 100644 sci-mathematics/isabelle/files/isabelle-2009-proofgeneral-gentoo-path.patch
 create mode 100644 sci-mathematics/isabelle/isabelle-2009.ebuild

(limited to 'sci-mathematics')

diff --git a/sci-mathematics/isabelle/Manifest b/sci-mathematics/isabelle/Manifest
new file mode 100644
index 0000000..dd12e33
--- /dev/null
+++ b/sci-mathematics/isabelle/Manifest
@@ -0,0 +1,3 @@
+AUX isabelle-2009-proofgeneral-gentoo-path.patch 316 RMD160 ecf031c8807f0e8a0403293e1c47abc92c7ddb76 SHA1 4e38535264f69901c00e48c8ccf75af42256cae9 SHA256 84fe80a5f7f5e623b0e9fd9da67e8ca5b216551fd2e05ce4f62456f051a73a8c
+DIST Isabelle2009.tar.gz 9073615 RMD160 7cbde579b6f897b8110c465f17a185f04f6587e0 SHA1 2af6f19f23436c37611d8df23e918f76e9190f39 SHA256 49f8708962a89102cd25d9b5b7bf1298017c0689f9ced7741c124351b58f8e71
+EBUILD isabelle-2009.ebuild 2589 RMD160 a5ce601359e7800c9cd66f7d500e5b8ec4ba75e1 SHA1 52f5d8463f0ebf9e0688cac6c3c0345f027de44b SHA256 0591b55a123df6153d9ef10b4284d461997b1fd03eaf95028603d81ee06cb3ae
diff --git a/sci-mathematics/isabelle/files/isabelle-2009-proofgeneral-gentoo-path.patch b/sci-mathematics/isabelle/files/isabelle-2009-proofgeneral-gentoo-path.patch
new file mode 100644
index 0000000..f64581d
--- /dev/null
+++ b/sci-mathematics/isabelle/files/isabelle-2009-proofgeneral-gentoo-path.patch
@@ -0,0 +1,10 @@
+--- Isabelle/etc/settings.old	2009-09-28 15:20:14.000000000 +0200
++++ Isabelle/etc/settings	2009-09-28 15:20:34.000000000 +0200
+@@ -194,6 +194,7 @@
+   "/usr/local/ProofGeneral" \
+   "/usr/share/ProofGeneral" \
+   "/opt/ProofGeneral" \
++  "/usr/share/emacs/site-lisp/ProofGeneral" \
+   "")
+ 
+ PROOFGENERAL_OPTIONS=""
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."
+}
-- 
cgit v1.2.3-70-g09d2