version bump, bug #196533, compatible with ocaml 3.10 (needs camlp5 though)

Package-Manager: portage-2.1.3.15

4 files changed, 90 insertions, 8 deletions

diff --git a/sci-mathematics/coq/ChangeLog b/sci-mathematics/coq/ChangeLog
index 794656d1d3be..d16d0a10721c 100644
--- a/sci-mathematics/coq/ChangeLog
+++ b/sci-mathematics/coq/ChangeLog
@@ -1,6 +1,11 @@
 # ChangeLog for sci-mathematics/coq
 # Copyright 2000-2007 Gentoo Foundation; Distributed under the GPL v2
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/ChangeLog,v 1.17 2007/10/11 10:04:22 aballier Exp $
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/ChangeLog,v 1.18 2007/10/20 15:37:29 aballier Exp $
+
+*coq-8.1_p2 (20 Oct 2007)
+
+  20 Oct 2007; Alexis Ballier <aballier@gentoo.org> +coq-8.1_p2.ebuild:
+  version bump, bug #196533, compatible with ocaml 3.10 (needs camlp5 though)
 
   11 Oct 2007; Alexis Ballier <aballier@gentoo.org> coq-8.1_p1.ebuild:
   fix configure call when ide and norealanalysis useflags are set, bug #195483
diff --git a/sci-mathematics/coq/Manifest b/sci-mathematics/coq/Manifest
index c4ca75435685..9a24ddef1e36 100644
--- a/sci-mathematics/coq/Manifest
+++ b/sci-mathematics/coq/Manifest
@@ -23,6 +23,7 @@ DIST coq-8.0pl1.tar.gz 2272613 RMD160 e8437bc84e130757ae4bc46b832a95c0ea655da3 S
 DIST coq-8.0pl3-translator.tar.gz 233228 RMD160 7dd748ee5929faf93ca75bec94b443573405b0fe SHA1 4a62e60759c8bbbf454febc47da0c92a0e9f862e SHA256 78def7e2998526db8c5740580113802a821c31de65bb12a7c74c512f6a9328f7
 DIST coq-8.0pl3.tar.gz 2309002 RMD160 925a65fdd0c96f4fe6082bc7bfb8483c83b5fea7 SHA1 b182f25b8e6591139281f7078d049aaa7f0408d8 SHA256 03d02b39873197f5365aad9bc2b917f4db234dcfd4bcff79febd8525770fb84c
 DIST coq-8.1pl1.tar.gz 2984726 RMD160 9982d2022abfb2f74dc34cdc6cdd25343f5cb583 SHA1 8142cd21b3d0b5fd56c3b5568550c09cac91a3f8 SHA256 04ffc9c5a31953af6294753118dbb2e41b6aa5aaa5a41f7cf2648afff98f4940
+DIST coq-8.1pl2.tar.gz 2997185 RMD160 e45451fdd41b1f979febcfb2c0dbd19a39d09256 SHA1 33ab31abffe42559a5c8341b66a0520805337526 SHA256 04d1ab1cfefe453224dee89d4351fd45a9553acc8f242e87f8fdad6e8af5320c
 EBUILD coq-8.0-r1.ebuild 2065 RMD160 3a8f789e1b2aa5685bf91ea8275adbc5d9399cdc SHA1 6af7eede753cdcf30c39975b0b6bde09fcac5705 SHA256 ca17fb5bbf9e36fb3880307a6f0df9b6a90c985d6d47d7830f9f6a891cb34b17
 MD5 32ab0325f73670990840fd4d5cbb87e6 coq-8.0-r1.ebuild 2065
 RMD160 3a8f789e1b2aa5685bf91ea8275adbc5d9399cdc coq-8.0-r1.ebuild 2065
@@ -35,10 +36,14 @@ EBUILD coq-8.1_p1.ebuild 1611 RMD160 559396a223725eda333e1aeaa70ea823b44b466e SH
 MD5 3b09dfd84267c421b137c9711f35add1 coq-8.1_p1.ebuild 1611
 RMD160 559396a223725eda333e1aeaa70ea823b44b466e coq-8.1_p1.ebuild 1611
 SHA256 ee46e0ec50bbaea62c896db4ecfd0cd9f1a29447b33e62eab5f552cc506ab74d coq-8.1_p1.ebuild 1611
-MISC ChangeLog 3863 RMD160 929bfc774007b6ac261304d855839b1b1e0c9bbc SHA1 0b9f6966babb98ca5ae07a23aa98309979feeb86 SHA256 c4c9ee356e12379259215a62148f9e243f9b301032ac546560af473fe90f14bc
-MD5 7f687eeb2d9ef93cf6565f68e102cd5c ChangeLog 3863
-RMD160 929bfc774007b6ac261304d855839b1b1e0c9bbc ChangeLog 3863
-SHA256 c4c9ee356e12379259215a62148f9e243f9b301032ac546560af473fe90f14bc ChangeLog 3863
+EBUILD coq-8.1_p2.ebuild 1707 RMD160 ce08d9a05e6bf60aae1f32501015bc0e4e42246d SHA1 995f6481a4bd1892a7e7bc7d6d5beac5b70f2ca8 SHA256 8eab7d69053318aef442a967885e78dcfa30b2c41656462bd9cc68876043196b
+MD5 352d4eeb9b8d3cc44e038527b3b8ffa4 coq-8.1_p2.ebuild 1707
+RMD160 ce08d9a05e6bf60aae1f32501015bc0e4e42246d coq-8.1_p2.ebuild 1707
+SHA256 8eab7d69053318aef442a967885e78dcfa30b2c41656462bd9cc68876043196b coq-8.1_p2.ebuild 1707
+MISC ChangeLog 4041 RMD160 fe822198d1f65f3b4b5943adf47cf2c808f0d2e0 SHA1 361e1564b83670f8f9b30514a460b6df7d24b18c SHA256 4cec909aaca1a060e8a4679853487927f23483995935e989aea178e8c0902fbc
+MD5 00ec172a6a3bf79283b817e00a8d0f9a ChangeLog 4041
+RMD160 fe822198d1f65f3b4b5943adf47cf2c808f0d2e0 ChangeLog 4041
+SHA256 4cec909aaca1a060e8a4679853487927f23483995935e989aea178e8c0902fbc ChangeLog 4041
 MISC metadata.xml 174 RMD160 b6d9f7a487e305c44a47ffaa8d982731b5825a19 SHA1 70e63d5e68a5449b129f8f91f2554e8406e212a0 SHA256 3c931940a18c0692dd36b609c3026ce41dcde08cdc9e2d0d7bc0a0cf774e8c5b
 MD5 587dfb99f9b1ef3ef6a79733b24811cc metadata.xml 174
 RMD160 b6d9f7a487e305c44a47ffaa8d982731b5825a19 metadata.xml 174
@@ -52,10 +57,13 @@ SHA256 d1900263704dc613417b872026abf1bde19771a25ebd7c0a09e7c82ee1201ec6 files/di
 MD5 7a4fed88ce4670c5216e542adeaaa4f7 files/digest-coq-8.1_p1 235
 RMD160 25cc8fd78c93c6b6ce97ba7435ead0c8b7f863f5 files/digest-coq-8.1_p1 235
 SHA256 c45e2081aea31363e671e61b8335e4a15955ea13bc5e9f26f6f0a0fd96cdae84 files/digest-coq-8.1_p1 235
+MD5 2cfc8fd041d90954c16584ef6b800760 files/digest-coq-8.1_p2 235
+RMD160 02ab849b986c8d8e0da29e3d6dd79b410e2d7c61 files/digest-coq-8.1_p2 235
+SHA256 6e90b572e62f580834a9721149404b02faf2cac779670386219b778dfd7492e3 files/digest-coq-8.1_p2 235
 -----BEGIN PGP SIGNATURE-----
 Version: GnuPG v2.0.7 (GNU/Linux)
 
-iD8DBQFHDfU4vFcC4BYPU0oRAs01AJ9CZlMdR1WPYdWrvyR2iTjDhL3y7wCfWymp
-VF0xD5LQGn6PaO/ZxaMld/c=
-=EbMo
+iD8DBQFHGiDJvFcC4BYPU0oRAuLBAJ9uJZzaEZA1J3t6BrtzNoZB/2HKPQCgwGLh
+8hEdMVmBerEPTn/CdxerRZg=
+=n1xL
 -----END PGP SIGNATURE-----
diff --git a/sci-mathematics/coq/coq-8.1_p2.ebuild b/sci-mathematics/coq/coq-8.1_p2.ebuild
new file mode 100644
index 000000000000..42a86fbe9a82
--- /dev/null
+++ b/sci-mathematics/coq/coq-8.1_p2.ebuild
@@ -0,0 +1,66 @@
+# Copyright 1999-2007 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.1_p2.ebuild,v 1.1 2007/10/20 15:37:29 aballier Exp $
+
+inherit eutils multilib
+
+IUSE="norealanalysis ide debug"
+
+RESTRICT="strip"
+
+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="ftp://ftp.inria.fr/INRIA/${PN}/V${MY_PV}/${MY_P}.tar.gz"
+
+LICENSE="LGPL-2.1"
+SLOT="0"
+KEYWORDS="~amd64 ~ppc ~sparc ~x86"
+
+DEPEND="|| ( >=dev-ml/camlp5-5.01 <dev-lang/ocaml-3.10 )
+>=dev-lang/ocaml-3.08
+ide? ( >=dev-ml/lablgtk-2.2.0 )"
+
+S="${WORKDIR}/${MY_P}"
+
+src_compile() {
+	local myconf="--prefix /usr \
+		--bindir /usr/bin \
+		--libdir /usr/$(get_libdir)/coq \
+		--mandir /usr/man \
+		--emacslib /usr/share/emacs/site-lisp \
+		--coqdocdir /usr/$(get_libdir)/coq/coqdoc"
+
+	use debug && myconf="--debug $myconf"
+	use norealanalysis && myconf="$myconf --reals no"
+	use norealanalysis || myconf="$myconf --reals all"
+
+	if use ide; then
+		myconf="$myconf --coqide opt"
+	else
+		myconf="$myconf --coqide no"
+	fi
+
+	./configure $myconf || die "configure failed"
+
+	if use ide; then
+		labldir=/usr/$(get_libdir)/ocaml/lablgtk2
+		sed -i -e "s|BYTEFLAGS=|BYTEFLAGS=-I ${labldir} |" Makefile
+		sed -i -e "s|OPTFLAGS=|OPTFLAGS=-I ${labldir} |" Makefile
+		sed -i -e "s|COQIDEFLAGS=.*|COQIDEFLAGS=-thread -I ${labldir}|" Makefile
+	fi
+
+	emake -j1 alldepend || die "make failed"
+	emake worldnodep || die "make failed"
+}
+
+src_install() {
+	emake COQINSTALLPREFIX="${D}" install || die
+	dodoc README CREDITS CHANGES LICENSE
+
+	if use ide; then
+		domenu "${FILESDIR}/coqide.desktop"
+	fi
+}
diff --git a/sci-mathematics/coq/files/digest-coq-8.1_p2 b/sci-mathematics/coq/files/digest-coq-8.1_p2
new file mode 100644
index 000000000000..dbdb3c73a5b2
--- /dev/null
+++ b/sci-mathematics/coq/files/digest-coq-8.1_p2
@@ -0,0 +1,3 @@
+MD5 714e8ba53758c4e61af8854a4892d174 coq-8.1pl2.tar.gz 2997185
+RMD160 e45451fdd41b1f979febcfb2c0dbd19a39d09256 coq-8.1pl2.tar.gz 2997185
+SHA256 04d1ab1cfefe453224dee89d4351fd45a9553acc8f242e87f8fdad6e8af5320c coq-8.1pl2.tar.gz 2997185