From 06ca475a202d54af1732d75fb1ade08561e70a47 Mon Sep 17 00:00:00 2001 From: Mark Wright Date: Sun, 8 Jan 2012 12:35:43 +0000 Subject: [PATCH] New ebuild, thanks Mr. Anderson for earlier version, fixes #397995 Package-Manager: portage-2.1.10.44/cvs/Linux x86_64 --- sci-mathematics/isabelle/ChangeLog | 11 ++ sci-mathematics/isabelle/Manifest | 16 ++ .../files/isabelle-2011.1-graphbrowser.patch | 11 ++ ...elle-2011.1-proofgeneral-gentoo-path.patch | 39 +++++ .../isabelle/isabelle-2011.1.ebuild | 148 ++++++++++++++++++ sci-mathematics/isabelle/metadata.xml | 36 +++++ 6 files changed, 261 insertions(+) create mode 100644 sci-mathematics/isabelle/ChangeLog create mode 100644 sci-mathematics/isabelle/Manifest create mode 100644 sci-mathematics/isabelle/files/isabelle-2011.1-graphbrowser.patch create mode 100644 sci-mathematics/isabelle/files/isabelle-2011.1-proofgeneral-gentoo-path.patch create mode 100644 sci-mathematics/isabelle/isabelle-2011.1.ebuild create mode 100644 sci-mathematics/isabelle/metadata.xml 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 +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/Manifest b/sci-mathematics/isabelle/Manifest new file mode 100644 index 000000000000..75dbaf4960fe --- /dev/null +++ b/sci-mathematics/isabelle/Manifest @@ -0,0 +1,16 @@ +-----BEGIN PGP SIGNED MESSAGE----- +Hash: SHA256 + +AUX isabelle-2011.1-graphbrowser.patch 358 RMD160 debe029504aad72c611f783569ca6e5e07d6fcfa SHA1 5067aa4f60a9185d6b7ca2e4d9511dd93ed6f239 SHA256 3c4a1567e06ea062f3064a7fb4555a645591732dc2d77daf7b4c49de6f640115 +AUX isabelle-2011.1-proofgeneral-gentoo-path.patch 1265 RMD160 9060454ab5480056b931b7a663137c80efa73b42 SHA1 e447977ddfbf08de46695f7b63e0ce2af3b55ac5 SHA256 08f6dae3f3157331ac83a3204f95e75838725175994c54f25b5f71715836556a +DIST Isabelle2011-1.tar.gz 42239059 RMD160 70dadeaf38ae71ff9871f8c5b9ba823c4d5cbcc7 SHA1 2f514bc2cff7e7f7c75a3cb15c71ea71009f8df7 SHA256 48d77fe31a16b44f6015aa7953a60bdad8fcec9e60847630dc7b98c053edfc08 +EBUILD isabelle-2011.1.ebuild 4086 RMD160 b338eb3274078232ecb028f5b7690e1de2655b57 SHA1 331131526dde18c8d81e050ed66d3e5033a57124 SHA256 29e1c504ccb2a930abcc0b9317eb9cb6a71dbf4a260b70cc8da84e1c6756b464 +MISC ChangeLog 512 RMD160 cd98157922b80efa0078f449340f9d4f297b020e SHA1 b8f1ddfc5e1f32a294170e72767adabd8ea5418d SHA256 7199fdb19f50c41a442d47bd23a2eba424fd317c077b120bcc089321ae94fb53 +MISC metadata.xml 1865 RMD160 6da50a4518e0bc23b6e6e5e540d8c4d47e71d74f SHA1 2e018687c48c173777159b28921d7d01a69b4ab9 SHA256 1a9f11e26050e0236ff9017d14b67ef7fd1a440cd4e865dbdf0b6cf1ddb2ff82 +-----BEGIN PGP SIGNATURE----- +Version: GnuPG v2.0.17 (GNU/Linux) + +iF4EAREIAAYFAk8Jja4ACgkQoBEVQmGOlx/1gQD/XP627XJ5PAtsbDQx11Tg3/AJ +f9KYwd0coxlGu8XW76YA/iISKM6zT8o3ebKFUVolyl02TtuCOShmj0min0bytK2S +=lMg2 +-----END PGP SIGNATURE----- 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 @@ + + + +sci-mathematics + +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. + + + Pure is the basis for all object-logics. + FOL (Many-sorted First-Order Logic) provides basic + classical and intuitionistic first-order logic. It is polymorphic. + (Higher-Order Logic) is a version of classical higher-order + logic resembling that of the HOL System. + ZF (Set Theory) offers a formulation of Zermelo-Fraenkel + set theory on top of FOL. + CCL (Classical Computational Logic) + CTT (Constructive Type Theory) is an extensional version + of Martin-Löf's Type Theory. + Cube (The Lambda Cube) + FOLP (FOL with Proof Terms) + LCF (Logic of Computable Functions) + Sequents (first-order, modal and linear logics) + 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. + Add support for the + app-emacs/proofgeneral proof assistant front end. + + -- 2.26.2