--- /dev/null
+# 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
+
--- /dev/null
+-----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-----
--- /dev/null
+--- 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
+
--- /dev/null
+--- 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=""
--- /dev/null
+# 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
+}
--- /dev/null
+<?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>
projects / gentoo.git / commitdiff