bump to pl2

Package-Manager: portage-2.1.10.10/cvs/Linux i686

3 files changed, 96 insertions, 7 deletions

diff --git a/sci-mathematics/coq/ChangeLog b/sci-mathematics/coq/ChangeLog
index 26a32e8996eb..f8cc3cfbfb38 100644
--- a/sci-mathematics/coq/ChangeLog
+++ b/sci-mathematics/coq/ChangeLog
@@ -1,6 +1,11 @@
 # ChangeLog for sci-mathematics/coq
 # Copyright 1999-2011 Gentoo Foundation; Distributed under the GPL v2
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/ChangeLog,v 1.65 2011/07/06 18:41:39 aballier Exp $
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/ChangeLog,v 1.66 2011/08/13 12:53:00 tomka Exp $
+
+*coq-8.3_p2 (13 Aug 2011)
+
+  13 Aug 2011; Thomas Kahle <tomka@gentoo.org> +coq-8.3_p2.ebuild:
+  bump to pl2
 
   06 Jul 2011; Alexis Ballier <aballier@gentoo.org> -coq-8.2_p1-r1.ebuild,
   -coq-8.2_p2.ebuild, -files/coq-8.2_p2-camlp5-6-compat.patch,
diff --git a/sci-mathematics/coq/Manifest b/sci-mathematics/coq/Manifest
index e0563ba85ae4..ac2784637760 100644
--- a/sci-mathematics/coq/Manifest
+++ b/sci-mathematics/coq/Manifest
@@ -1,15 +1,17 @@
 -----BEGIN PGP SIGNED MESSAGE-----
-Hash: SHA1
+Hash: SHA256
 
 AUX coqide.desktop 233 RMD160 3f9d112d7f55454f72c42b427005b37971c6e928 SHA1 40571b86c25793e7d4e9bef80f637d7440b03704 SHA256 dba2e81a408ae51e187c2a164794f9505c4abfa0b92f47a44d0e9f96e2b6dfac
 DIST coq-8.3pl1.tar.gz 3756961 RMD160 687983bcaca723299b6ea902a1e1b07338209d55 SHA1 3fae9fa2fd6f39c9fb3c0b67fcd5e71f1e7a5f9f SHA256 3a497386bd74f43a5af1d0c53f29a017ce7ed1b1e60c052217fe04b7f40be928
+DIST coq-8.3pl2.tar.gz 3760176 RMD160 f59ee288a35c1009f88f050362bee21311b459a8 SHA1 8506761e4755739cc728aff790dd778db8217f3f SHA256 b82b44ec585903b6bfadca02008eb5549cda46038c776ec115bc408c4e0f34f1
 EBUILD coq-8.3_p1.ebuild 2203 RMD160 3599adbd03754de93230d9adf95b3210f092927e SHA1 7c753b264fc1837adada16e20c2e048dc1f08f6e SHA256 bf5317d76d666ff1f3199c68ec049641f518ec13e2388b4917aa34873667d4f5
-MISC ChangeLog 10706 RMD160 e5e1e1153819c4ac01dca4650979d5418643a119 SHA1 a5296c2ae88d45f28799a8fa56e42fb3cbee512d SHA256 32f29787aec0e871a6d4f14815bccb3e2cf04a66552287d7be34b8d7b0a0479b
+EBUILD coq-8.3_p2.ebuild 2276 RMD160 fc739cdb46156470d4e09f893257a0bf83008938 SHA1 8bc25542e744c23678a0628f3c16efb0a30ca701 SHA256 5cc6e23cdc2a21a79c2ec491cd1bee6c3d7194a691d0628161492ed53ff9bea0
+MISC ChangeLog 10812 RMD160 14d461c72756fc0d9398c5632ad386e2ade10dc2 SHA1 c09a9caaf0adc876394a92379a0154d34bad2324 SHA256 26295c17a97e0cce58baad74ac5343c411a0e4c44499511e3523dc7d106324e6
 MISC metadata.xml 788 RMD160 98e6a38354c1398f7bed64f34aa88e1d439190b3 SHA1 7d9ce5fed17eaf9bf756b493c76c27678212995b SHA256 5028003bf6d1ec17b51ce45c17bb565137f825a5eefcdf57de4a98c5c61d0626
 -----BEGIN PGP SIGNATURE-----
-Version: GnuPG v2.0.17 (GNU/Linux)
+Version: GnuPG v2.0.18 (GNU/Linux)
 
-iEYEARECAAYFAk4UrGkACgkQvFcC4BYPU0qF8wCdHWsX1TxgE1eYDUN593VUoKS+
-YOgAnjsCalrKWyvVy1ITTRo8FKed9EfZ
-=OWqR
+iF4EAREIAAYFAk5GdlQACgkQodBTJSDyo67dJAD/SeYU5QaPAVhVuY12sD1OLlvA
+u71dpSXwkYnW8jxU8LcA/R8FaF/65dTVS+IYwPS7ZWYYvI2eyiK4qlFd6qCGXjWp
+=wyGL
 -----END PGP SIGNATURE-----
diff --git a/sci-mathematics/coq/coq-8.3_p2.ebuild b/sci-mathematics/coq/coq-8.3_p2.ebuild
new file mode 100644
index 000000000000..38438f4fd8ce
--- /dev/null
+++ b/sci-mathematics/coq/coq-8.3_p2.ebuild
@@ -0,0 +1,82 @@
+# Copyright 1999-2011 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.3_p2.ebuild,v 1.1 2011/08/13 12:53:00 tomka Exp $
+
+EAPI="2"
+
+inherit eutils multilib
+
+MY_PV=${PV/_p/pl}
+MY_P=${PN}-${MY_PV}
+
+DESCRIPTION="Coq is a proof assistant written in O'Caml"
+HOMEPAGE="http://coq.inria.fr/"
+SRC_URI="http://${PN}.inria.fr/V${MY_PV}/files/${MY_P}.tar.gz"
+
+LICENSE="LGPL-2.1"
+SLOT="0"
+KEYWORDS="~amd64 ~ppc ~x86"
+IUSE="gtk debug +ocamlopt doc"
+
+RDEPEND=">=dev-lang/ocaml-3.10[ocamlopt?]
+	>=dev-ml/camlp5-5.09[ocamlopt?]
+	gtk? ( >=dev-ml/lablgtk-2.10.1[ocamlopt?] )"
+DEPEND="${RDEPEND}
+	doc? (
+		media-libs/netpbm[png,zlib]
+		virtual/latex-base
+		dev-tex/hevea
+		dev-tex/xcolor
+		|| ( dev-texlive/texlive-pictures app-text/ptex )
+		|| ( dev-texlive/texlive-mathextra app-text/ptex )
+		|| ( dev-texlive/texlive-latexextra app-text/ptex )
+		)"
+
+S=${WORKDIR}/${MY_P}
+
+src_prepare() {
+	# configure has an error at line 640 leading to closing a
+	# string to early in the generated coq_config.ml. Here is a
+	# wild sed which replaces \"$LABLGTKLIB\" by $LABLGTKLIB.  Note
+	# during pl2-bump: Hmm, my patch did not get applied upstream?
+	sed -i "s/\\\\\"\\\$LABLGTKLIB\\\\\"/\\\$LABLGTKLIB/" configure
+}
+
+src_configure() {
+	ocaml_lib=`ocamlc -where`
+	local myconf="--prefix /usr
+		--bindir /usr/bin
+		--libdir /usr/$(get_libdir)/coq
+		--mandir /usr/share/man
+		--emacslib /usr/share/emacs/site-lisp
+		--coqdocdir /usr/$(get_libdir)/coq/coqdoc
+		--docdir /usr/share/doc/${PF}
+		--camlp5dir ${ocaml_lib}/camlp5
+		--lablgtkdir ${ocaml_lib}/lablgtk2"
+
+	use debug && myconf="--debug $myconf"
+	use doc || myconf="$myconf --with-doc no"
+
+	if use gtk; then
+		use ocamlopt && myconf="$myconf --coqide opt"
+		use ocamlopt || myconf="$myconf --coqide byte"
+	else
+		myconf="$myconf --coqide no"
+	fi
+	use ocamlopt || myconf="$myconf -byte-only"
+	use ocamlopt && myconf="$myconf --opt"
+
+	export CAML_LD_LIBRARY_PATH="${S}/kernel/byterun/"
+	./configure $myconf || die "configure failed"
+}
+
+src_compile() {
+	emake STRIP="true" -j1 || die "make failed"
+}
+
+src_install() {
+	emake STRIP="true" COQINSTALLPREFIX="${D}" install || die
+	dodoc README CREDITS CHANGES
+
+	use gtk && domenu "${FILESDIR}/coqide.desktop"
+}