diff options
author | Mark Wright <gienah@gentoo.org> | 2012-01-08 12:35:43 +0000 |
---|---|---|
committer | Mark Wright <gienah@gentoo.org> | 2012-01-08 12:35:43 +0000 |
commit | e209deb4b6bb526791005af111c16b6f5732405d (patch) | |
tree | bb9c4540aa30fd0f1108bfba6a199dcaf09f07b0 /sci-mathematics | |
parent | Fix a compilation problem (diff) | |
download | gentoo-2-e209deb4b6bb526791005af111c16b6f5732405d.tar.gz gentoo-2-e209deb4b6bb526791005af111c16b6f5732405d.tar.bz2 gentoo-2-e209deb4b6bb526791005af111c16b6f5732405d.zip |
New ebuild, thanks Mr. Anderson for earlier version, fixes #397995
(Portage version: 2.1.10.44/cvs/Linux x86_64)
Diffstat (limited to 'sci-mathematics')
-rw-r--r-- | sci-mathematics/isabelle/ChangeLog | 11 | ||||
-rw-r--r-- | sci-mathematics/isabelle/files/isabelle-2011.1-graphbrowser.patch | 11 | ||||
-rw-r--r-- | sci-mathematics/isabelle/files/isabelle-2011.1-proofgeneral-gentoo-path.patch | 39 | ||||
-rw-r--r-- | sci-mathematics/isabelle/isabelle-2011.1.ebuild | 148 | ||||
-rw-r--r-- | sci-mathematics/isabelle/metadata.xml | 36 |
5 files changed, 245 insertions, 0 deletions
diff --git a/sci-mathematics/isabelle/ChangeLog b/sci-mathematics/isabelle/ChangeLog new file mode 100644 index 000000000000..759d5478e73d --- /dev/null +++ b/sci-mathematics/isabelle/ChangeLog @@ -0,0 +1,11 @@ +# ChangeLog for sci-mathematics/isabelle +# Copyright 1999-2012 Gentoo Foundation; Distributed under the GPL v2 +# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/isabelle/ChangeLog,v 1.1 2012/01/08 12:35:43 gienah Exp $ + +*isabelle-2011.1 (08 Jan 2012) + + 08 Jan 2012; Mark Wright <gienah@gentoo.org> +isabelle-2011.1.ebuild, + +files/isabelle-2011.1-graphbrowser.patch, + +files/isabelle-2011.1-proofgeneral-gentoo-path.patch, +metadata.xml: + New ebuild, thanks Mr. Anderson for earlier version, fixes #397995 + diff --git a/sci-mathematics/isabelle/files/isabelle-2011.1-graphbrowser.patch b/sci-mathematics/isabelle/files/isabelle-2011.1-graphbrowser.patch new file mode 100644 index 000000000000..ed8036a9b2d4 --- /dev/null +++ b/sci-mathematics/isabelle/files/isabelle-2011.1-graphbrowser.patch @@ -0,0 +1,11 @@ +--- Isabelle2011-1-orig/lib/browser/build 2011-10-10 01:47:58.000000000 +1100 ++++ Isabelle2011-1/lib/browser/build 2012-01-08 12:58:06.041444651 +1100 +@@ -6,6 +6,8 @@ + # + # Requires proper Isabelle settings environment. + ++ISABELLE_HOME="$(cd "$(dirname "${0}")/../.."; pwd -P)" ++source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 + + ## diagnostics + diff --git a/sci-mathematics/isabelle/files/isabelle-2011.1-proofgeneral-gentoo-path.patch b/sci-mathematics/isabelle/files/isabelle-2011.1-proofgeneral-gentoo-path.patch new file mode 100644 index 000000000000..67e3476f2170 --- /dev/null +++ b/sci-mathematics/isabelle/files/isabelle-2011.1-proofgeneral-gentoo-path.patch @@ -0,0 +1,39 @@ +--- Isabelle2011-1-orig/etc/settings 2011-10-10 01:47:58.000000000 +1100 ++++ Isabelle2011-1/etc/settings 2012-01-01 16:33:27.922565527 +1100 +@@ -24,9 +24,16 @@ + "/usr/share/polyml/$ML_PLATFORM" \ + "/opt/polyml/$ML_PLATFORM" \ + "")" +-ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version") +-ML_OPTIONS="-H 200" +-ML_SOURCES="$ML_HOME/../src" ++# ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version") ++# ML_OPTIONS="-H 200" ++# ML_SOURCES="$ML_HOME/../src" ++ ++# Poly/ML 5.4.0 (64 bit) ++ML_PLATFORM=x86_64-linux ++ML_HOME=/usr/bin ++ML_SYSTEM=polyml-5.4.0 ++ML_OPTIONS="-H 1000" ++#ML_SOURCES="$ML_HOME/../src" + + # Poly/ML 32 bit (manual settings) + #ML_SYSTEM=polyml-5.4.0 +@@ -106,7 +113,7 @@ + ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER" + + # Heap input locations. ML system identifier is included in lookup. +-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps" ++ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:/usr/lib64/Isabelle2011-1/heaps" + + # Heap output location. ML system identifier is appended automatically later on. + ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" +@@ -170,6 +177,7 @@ + "/usr/local/ProofGeneral" \ + "/usr/share/ProofGeneral" \ + "/opt/ProofGeneral" \ ++ "/usr/share/emacs/site-lisp/ProofGeneral" \ + "")" + + PROOFGENERAL_OPTIONS="" diff --git a/sci-mathematics/isabelle/isabelle-2011.1.ebuild b/sci-mathematics/isabelle/isabelle-2011.1.ebuild new file mode 100644 index 000000000000..534db9147e52 --- /dev/null +++ b/sci-mathematics/isabelle/isabelle-2011.1.ebuild @@ -0,0 +1,148 @@ +# Copyright 1999-2012 Gentoo Foundation +# Distributed under the terms of the GNU General Public License v2 +# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/isabelle/isabelle-2011.1.ebuild,v 1.1 2012/01/08 12:35:43 gienah Exp $ + +EAPI="4" + +JAVA_PKG_OPT_USE="graphbrowsing" +inherit eutils java-pkg-opt-2 multilib versionator + +MY_PN="Isabelle" +typeset -u MY_PV +MY_PV=$(replace_all_version_separators '-') +MY_P="${MY_PN}${MY_PV}" + +DESCRIPTION="Isabelle is a generic proof assistant" +HOMEPAGE="http://www.cl.cam.ac.uk/research/hvg/isabelle/index.html" +SRC_URI="http://www.cl.cam.ac.uk/research/hvg/isabelle/dist/${MY_P}.tar.gz" + +LICENSE="BSD" +SLOT="0" +KEYWORDS="~x86 ~amd64" +ALL_LOGICS="Pure FOL +HOL ZF CCL CTT Cube FOLP LCF Sequents" +IUSE="${ALL_LOGICS} doc graphbrowsing +pdf +proofgeneral" + +#upstream says +#bash 2.x/3.x, Poly/ML 5.x, Perl 5.x, +#for document preparation: complete LaTeX +DEPEND=">=app-shells/bash-3.0 + >=dev-lang/polyml-5.4.1 + >=dev-lang/perl-5.8.8-r2" + +RDEPEND="doc? ( + virtual/latex-base + dev-tex/rail + ) + pdf? ( || ( app-text/xpdf + app-text/gv + app-text/gsview + app-text/epdfview + app-text/acroread + app-text/zathura ) + ) + proofgeneral? ( + app-emacs/proofgeneral + ) + ${DEPEND}" + +S="${WORKDIR}"/Isabelle${MY_PV} +TARGETDIR="/usr/share/Isabelle"${MY_PV} +LIBDIR="/usr/"$(get_libdir)"/Isabelle"${MY_PV} + +pkg_setup() { + java-pkg-opt-2_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() { + java-pkg-opt-2_src_prepare + if use proofgeneral; then + epatch "${FILESDIR}/${PN}-2011.1-proofgeneral-gentoo-path.patch" + polymlver=$(poly -v | cut -d' ' -f2) + polymlarch=$(poly -v | cut -d' ' -f9 | cut -d'-' -f1) + sed -e "s@5.4.0@${polymlver}@g" \ + -i "${S}/etc/settings" || die "Could not configure polyml version in etc/settings" + sed -e "s@x86_64@${polymlarch}@g" \ + -i "${S}/etc/settings" || die "Could not configure polyml arch in etc/settings" + fi + if use graphbrowsing; then + epatch "${FILESDIR}/${PN}-2011.1-graphbrowser.patch" + fi +} + +src_compile() { + LOGICS="" + for l in "${ALL_LOGICS}"; do + if has "${l/+/}"; then + LOGICS="${LOGICS} ${l/+/}" + fi + done + einfo "Building Isabelle logics ${LOGICS}. This may take some time." + ./build -b -i "${LOGICS}" || die "building logics failed" + ./bin/isabelle makeall || die "isabelle makeall failed" + if use graphbrowsing + then + rm -f "${S}/lib/browser/GraphBrowser.jar" || die "failed cleaning graph browser directory" + cd "${S}/lib/browser" + ./build || die "failed building the graph browser" + cd "${S}" + fi +} + +src_test() { + einfo "Running tests. A test run can take up to several hours!" + ./build -b -t +} + +src_install() { + exeinto ${TARGETDIR}/bin + doexe bin/isabelle-process bin/isabelle + + exeinto ${TARGETDIR} + doexe build + + insinto ${TARGETDIR} + doins -r src + dodoc -r doc + + dodir /etc/isabelle + insinto /etc/isabelle + doins -r etc + + dosym /etc/isabelle "${TARGETDIR}/etc" + dosym "${LIBDIR}/heaps" "${TARGETDIR}/heaps" + + insinto ${LIBDIR} + doins -r heaps + + # use cp to keep file attributes + cp -R lib "${ED}${TARGETDIR}" || die "install lib failed" + + bin/isabelle install -d ${TARGETDIR} -p "${ED}usr/bin" \ + || die "isabelle install failed" + newicon lib/icons/isabelle.xpm "${PN}.xpm" + dodoc ANNOUNCE CONTRIBUTORS COPYRIGHT NEWS README + + java-pkg_regjar \ + "${ED}${TARGETDIR}/lib/browser/GraphBrowser.jar" \ + "${ED}${TARGETDIR}/lib/classes/ext/Pure.jar" \ + "${ED}${TARGETDIR}/lib/classes/ext/scala-library.jar" \ + "${ED}${TARGETDIR}/lib/classes/ext/scala-swing.jar" \ + "${ED}${TARGETDIR}/lib/classes/java_ext_dirs.jar" +} + +pkg_postinst() { + elog "You will need to re-emerge Isabelle after emerging polyml." + if use pdf; then + einfo "Please configure your preferred pdf viewer by editing" + einfo "the PDF_VIEWER variable in the system settings file" + einfo "/etc/conf/isabelle and/or the user settings file" + einfo "\$HOME/.isabelle/${MY_P}" + fi +} diff --git a/sci-mathematics/isabelle/metadata.xml b/sci-mathematics/isabelle/metadata.xml new file mode 100644 index 000000000000..c874493b4533 --- /dev/null +++ b/sci-mathematics/isabelle/metadata.xml @@ -0,0 +1,36 @@ +<?xml version="1.0" encoding="UTF-8"?> +<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd"> +<pkgmetadata> +<herd>sci-mathematics</herd> +<longdescription lang='en'> +Isabelle is a generic proof assistant. It allows mathematical +formulas to be expressed in a formal language and provides tools +for proving those formulas in a logical calculus. The main +application is the formalization of mathematical proofs and in +particular formal verification, which includes proving the +correctness of computer hardware or software and proving +properties of computer languages and protocols. +</longdescription> +<use> + <flag name='Pure'>Pure is the basis for all object-logics.</flag> + <flag name='FOL'>FOL (Many-sorted First-Order Logic) provides basic + classical and intuitionistic first-order logic. It is polymorphic.</flag> + <flag name='HOL'>(Higher-Order Logic) is a version of classical higher-order + logic resembling that of the HOL System.</flag> + <flag name='ZF'>ZF (Set Theory) offers a formulation of Zermelo-Fraenkel + set theory on top of FOL.</flag> + <flag name='CCL'>CCL (Classical Computational Logic)</flag> + <flag name='CTT'>CTT (Constructive Type Theory) is an extensional version + of Martin-Löf's Type Theory.</flag> + <flag name='Cube'>Cube (The Lambda Cube)</flag> + <flag name='FOLP'>FOLP (FOL with Proof Terms)</flag> + <flag name='LCF'>LCF (Logic of Computable Functions)</flag> + <flag name='Sequents'>Sequents (first-order, modal and linear logics)</flag> + <flag name='graphbrowsing'>Generate theory browsing information, + including HTML documents that show a theory's definition, the + theorems proved in its ML file and the relationship with its + ancestors and descendants.</flag> + <flag name='proofgeneral'>Add support for the + <pkg>app-emacs/proofgeneral</pkg> proof assistant front end.</flag> +</use> +</pkgmetadata> |