* [gentoo-commits] gentoo-x86 commit in sci-mathematics/isabelle: metadata.xml ChangeLog isabelle-2011.1.ebuild
@ 2012-01-08 12:35 Mark Wright (gienah)
0 siblings, 0 replies; 2+ messages in thread
From: Mark Wright (gienah) @ 2012-01-08 12:35 UTC (permalink / raw
To: gentoo-commits
gienah 12/01/08 12:35:43
Added: metadata.xml ChangeLog isabelle-2011.1.ebuild
Log:
New ebuild, thanks Mr. Anderson for earlier version, fixes #397995
(Portage version: 2.1.10.44/cvs/Linux x86_64)
Revision Changes Path
1.1 sci-mathematics/isabelle/metadata.xml
file : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/metadata.xml?rev=1.1&view=markup
plain: http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/metadata.xml?rev=1.1&content-type=text/plain
Index: metadata.xml
===================================================================
<?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>
1.1 sci-mathematics/isabelle/ChangeLog
file : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/ChangeLog?rev=1.1&view=markup
plain: http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/ChangeLog?rev=1.1&content-type=text/plain
Index: ChangeLog
===================================================================
# 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
1.1 sci-mathematics/isabelle/isabelle-2011.1.ebuild
file : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/isabelle-2011.1.ebuild?rev=1.1&view=markup
plain: http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/isabelle-2011.1.ebuild?rev=1.1&content-type=text/plain
Index: isabelle-2011.1.ebuild
===================================================================
# 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
}
^ permalink raw reply [flat|nested] 2+ messages in thread
* [gentoo-commits] gentoo-x86 commit in sci-mathematics/isabelle: metadata.xml ChangeLog isabelle-2011.1.ebuild
@ 2012-01-30 6:54 Mark Wright (gienah)
0 siblings, 0 replies; 2+ messages in thread
From: Mark Wright (gienah) @ 2012-01-30 6:54 UTC (permalink / raw
To: gentoo-commits
gienah 12/01/30 06:54:53
Modified: metadata.xml ChangeLog isabelle-2011.1.ebuild
Log:
Fix bug #400961, thanks to Mr. Anderson for report and fix.
(Portage version: 2.1.10.44/cvs/Linux x86_64)
Revision Changes Path
1.2 sci-mathematics/isabelle/metadata.xml
file : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/metadata.xml?rev=1.2&view=markup
plain: http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/metadata.xml?rev=1.2&content-type=text/plain
diff : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/metadata.xml?r1=1.1&r2=1.2
Index: metadata.xml
===================================================================
RCS file: /var/cvsroot/gentoo-x86/sci-mathematics/isabelle/metadata.xml,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -r1.1 -r1.2
--- metadata.xml 8 Jan 2012 12:35:43 -0000 1.1
+++ metadata.xml 30 Jan 2012 06:54:53 -0000 1.2
@@ -1,6 +1,9 @@
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
<pkgmetadata>
+<maintainer>
+ <email>gienah@gentoo.org></email>
+</maintainer>
<herd>sci-mathematics</herd>
<longdescription lang='en'>
Isabelle is a generic proof assistant. It allows mathematical
1.3 sci-mathematics/isabelle/ChangeLog
file : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/ChangeLog?rev=1.3&view=markup
plain: http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/ChangeLog?rev=1.3&content-type=text/plain
diff : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/ChangeLog?r1=1.2&r2=1.3
Index: ChangeLog
===================================================================
RCS file: /var/cvsroot/gentoo-x86/sci-mathematics/isabelle/ChangeLog,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -r1.2 -r1.3
--- ChangeLog 9 Jan 2012 13:49:21 -0000 1.2
+++ ChangeLog 30 Jan 2012 06:54:53 -0000 1.3
@@ -1,6 +1,10 @@
# 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.2 2012/01/09 13:49:21 gienah Exp $
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/isabelle/ChangeLog,v 1.3 2012/01/30 06:54:53 gienah Exp $
+
+ 30 Jan 2012; Mark Wright <gienah@gentoo.org> isabelle-2011.1.ebuild,
+ metadata.xml:
+ Fix bug #400961, thanks to Mr. Anderson for report and fix.
09 Jan 2012; Mark Wright <gienah@gentoo.org> isabelle-2011.1.ebuild:
Thanks to few_ and xarthisius for reviewing, remove pdf use flag, add || die
1.3 sci-mathematics/isabelle/isabelle-2011.1.ebuild
file : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/isabelle-2011.1.ebuild?rev=1.3&view=markup
plain: http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/isabelle-2011.1.ebuild?rev=1.3&content-type=text/plain
diff : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/isabelle-2011.1.ebuild?r1=1.2&r2=1.3
Index: isabelle-2011.1.ebuild
===================================================================
RCS file: /var/cvsroot/gentoo-x86/sci-mathematics/isabelle/isabelle-2011.1.ebuild,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -r1.2 -r1.3
--- isabelle-2011.1.ebuild 9 Jan 2012 13:49:21 -0000 1.2
+++ isabelle-2011.1.ebuild 30 Jan 2012 06:54:53 -0000 1.3
@@ -1,6 +1,6 @@
# 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.2 2012/01/09 13:49:21 gienah Exp $
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/isabelle/isabelle-2011.1.ebuild,v 1.3 2012/01/30 06:54:53 gienah Exp $
EAPI="4"
@@ -109,7 +109,7 @@
dodir /etc/isabelle
insinto /etc/isabelle
- doins -r etc
+ doins -r etc/*
dosym /etc/isabelle "${TARGETDIR}/etc"
dosym "${LIBDIR}/heaps" "${TARGETDIR}/heaps"
^ permalink raw reply [flat|nested] 2+ messages in thread
end of thread, other threads:[~2012-01-30 6:55 UTC | newest]
Thread overview: 2+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2012-01-08 12:35 [gentoo-commits] gentoo-x86 commit in sci-mathematics/isabelle: metadata.xml ChangeLog isabelle-2011.1.ebuild Mark Wright (gienah)
-- strict thread matches above, loose matches on Subject: below --
2012-01-30 6:54 Mark Wright (gienah)
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox