Update for ocaml-3.08, remove old ebuild.

8 files changed, 104 insertions, 50 deletions

diff --git a/app-sci/coq/ChangeLog b/app-sci/coq/ChangeLog
index 0ef313d5f5bc..a2acdb960720 100644
--- a/app-sci/coq/ChangeLog
+++ b/app-sci/coq/ChangeLog
@@ -1,6 +1,12 @@
 # ChangeLog for app-sci/coq
 # Copyright 2000-2004 Gentoo Foundation; Distributed under the GPL v2
-# $Header: /var/cvsroot/gentoo-x86/app-sci/coq/ChangeLog,v 1.6 2004/07/14 01:33:10 lv Exp $
+# $Header: /var/cvsroot/gentoo-x86/app-sci/coq/ChangeLog,v 1.7 2004/08/08 07:00:05 mattam Exp $
+
+*coq-8.0-r1 (08 Aug 2004)
+
+  08 Aug 2004; Matthieu Sozeau <mattam@gentoo.org> coq-7.4.ebuild,
+  +coq-8.0-r1.ebuild, coq-8.0.ebuild, -coq-8.0_beta.ebuild:
+  Prepare for 3.08 insertion, remove old beta ebuild and add the latest version.
 
   13 Jul 2004; Travis Tilley <lv@gentoo.org> coq-7.4.ebuild:
   adding ~amd64 keyword
diff --git a/app-sci/coq/Manifest b/app-sci/coq/Manifest
index c43bdba1b245..19502223ea65 100644
--- a/app-sci/coq/Manifest
+++ b/app-sci/coq/Manifest
@@ -1,11 +1,11 @@
-MD5 f7362fd7ee6b7239ea9b2fc4119e7ce6 coq-8.0_beta.ebuild 957
-MD5 dcfaeb126d2f6d629b7bb08dad938493 coq-8.0.ebuild 1890
-MD5 4086c425a9d17c6e54e23201184e90ec coq-7.4.ebuild 948
-MD5 9aff6bfd98e9836736a5cab5a0a31986 ChangeLog 1070
+MD5 e826079e6cd5df87ce36f2461e2b654e ChangeLog 1310
+MD5 2559fb0ebf76645f855752a3a18fa7d2 coq-7.4.ebuild 975
 MD5 5af6b26df9264817e5b6a292c1436417 metadata.xml 238
-MD5 73c401b2052bccdc88677bf5be2d453f files/digest-coq-8.0_beta 64
+MD5 d339db772572f94a8a1bbfb760feb745 coq-8.0-r1.ebuild 1942
+MD5 4b3e22466363130a7a799228534043a2 coq-8.0.ebuild 1910
+MD5 e5491c930f8f944ed9c3590fdc8492c1 files/coqide.desktop 242
 MD5 d3f33f3602d82ea691f91b062dbf236b files/digest-coq-7.4 60
-MD5 86922705a72292e7508baae5bc75e2a3 files/digest-coq-8.0 130
+MD5 dc0f737371101bc7c97b0a80165ddac6 files/digest-coq-8.0-r1 136
 MD5 393c3085f82f205122b4e66c94232ff7 files/ocaml-3.07.patch 333
 MD5 5d46723c29afcd1e24e529e5993c3096 files/coq-8.0-byteflags.patch 676
-MD5 e5491c930f8f944ed9c3590fdc8492c1 files/coqide.desktop 242
+MD5 86922705a72292e7508baae5bc75e2a3 files/digest-coq-8.0 130
diff --git a/app-sci/coq/coq-7.4.ebuild b/app-sci/coq/coq-7.4.ebuild
index 0ddb0cd4232b..b6f832034788 100644
--- a/app-sci/coq/coq-7.4.ebuild
+++ b/app-sci/coq/coq-7.4.ebuild
@@ -1,6 +1,6 @@
 # Copyright 1999-2004 Gentoo Foundation
 # Distributed under the terms of the GNU General Public License v2
-# $Header: /var/cvsroot/gentoo-x86/app-sci/coq/coq-7.4.ebuild,v 1.5 2004/07/14 01:33:10 lv Exp $
+# $Header: /var/cvsroot/gentoo-x86/app-sci/coq/coq-7.4.ebuild,v 1.6 2004/08/08 07:00:05 mattam Exp $
 
 inherit eutils
 
@@ -13,7 +13,8 @@ SLOT="0"
 KEYWORDS="x86 ppc ~amd64"
 IUSE="norealanalysis"
 
-DEPEND=">=dev-lang/ocaml-3.06"
+DEPEND=">=dev-lang/ocaml-3.06
+!>=dev-lang/ocaml-3.08"
 
 src_compile() {
 	local myconf="--prefix /usr \
diff --git a/app-sci/coq/coq-8.0-r1.ebuild b/app-sci/coq/coq-8.0-r1.ebuild
new file mode 100644
index 000000000000..64623533f745
--- /dev/null
+++ b/app-sci/coq/coq-8.0-r1.ebuild
@@ -0,0 +1,83 @@
+# Copyright 1999-2004 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Header: /var/cvsroot/gentoo-x86/app-sci/coq/coq-8.0-r1.ebuild,v 1.1 2004/08/08 07:00:05 mattam Exp $
+
+inherit eutils
+
+IUSE="norealanalysis ide debug translator doc"
+
+RESTRICT="nostrip"
+
+MY_PV="8.0pl1"
+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
+translator? ( ftp://ftp.inria.fr/INRIA/coq/V${MY_PV}/${MY_P}-translator.tar.gz )"
+
+LICENSE="LGPL-2.1"
+SLOT="0"
+KEYWORDS="~x86 ~ppc"
+
+DEPEND=">=dev-lang/ocaml-3.06
+ide? ( >=dev-ml/lablgtk-2.2.0 )"
+
+S="${WORKDIR}/${MY_P/_/}"
+
+src_unpack()
+{
+	unpack ${A}
+	cd ${S}
+	epatch ${FILESDIR}/${P}-byteflags.patch
+}
+
+src_compile() {
+	local myconf="--prefix /usr \
+		--bindir /usr/bin \
+		--libdir /usr/lib/coq \
+		--mandir /usr/man \
+		--emacslib /usr/share/emacs/site-lisp \
+		--coqdocdir /usr/lib/coq/coqdoc"
+
+	use debug && myconf="--debug $myconf"
+	use norealanalysis && myconf="$myconf --reals"
+	use norealanalysis || myconf="$myconf --reals all"
+
+	if use ide; then
+		myconf="$myconf --coqide opt"
+	else
+		myconf="$myconf --coqide no"
+	fi
+
+	./configure $myconf || die
+
+	if use ide; then
+		labldir=/usr/lib/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
+		make world || die
+	else
+		make world
+	fi
+}
+
+src_install() {
+	make COQINSTALLPREFIX=${D} install || die
+	dodoc README CREDITS CHANGES LICENSE
+
+	if use translator; then
+		cd ${WORKDIR}/${MY_P}-translator
+		mv translate-v8 coq-translate-v8
+		dobin coq-translate-v8
+		if use doc; then
+			dodoc Translator.* syntax-v8.*
+		fi
+	fi
+
+	if use ide; then
+		insinto /usr/share/applnk/Edutainment/Mathematics
+		doins ${FILESDIR}/coqide.desktop
+	fi
+}
diff --git a/app-sci/coq/coq-8.0.ebuild b/app-sci/coq/coq-8.0.ebuild
index 0e548828c481..9a5ec212a4ce 100644
--- a/app-sci/coq/coq-8.0.ebuild
+++ b/app-sci/coq/coq-8.0.ebuild
@@ -1,6 +1,6 @@
 # Copyright 1999-2004 Gentoo Foundation
 # Distributed under the terms of the GNU General Public License v2
-# $Header: /var/cvsroot/gentoo-x86/app-sci/coq/coq-8.0.ebuild,v 1.2 2004/07/09 21:42:18 mr_bones_ Exp $
+# $Header: /var/cvsroot/gentoo-x86/app-sci/coq/coq-8.0.ebuild,v 1.3 2004/08/08 07:00:05 mattam Exp $
 
 inherit eutils
 
@@ -18,6 +18,7 @@ SLOT="0"
 KEYWORDS="~x86 ~ppc"
 
 DEPEND=">=dev-lang/ocaml-3.06
+!>=dev-lang/ocaml-3.08
 ide? ( >=dev-ml/lablgtk-2.2.0 )"
 
 S="${WORKDIR}/${P/_/}"
diff --git a/app-sci/coq/coq-8.0_beta.ebuild b/app-sci/coq/coq-8.0_beta.ebuild
deleted file mode 100644
index 5ffb6a2ba93f..000000000000
--- a/app-sci/coq/coq-8.0_beta.ebuild
+++ /dev/null
@@ -1,38 +0,0 @@
-# Copyright 1999-2004 Gentoo Foundation
-# Distributed under the terms of the GNU General Public License v2
-# $Header: /var/cvsroot/gentoo-x86/app-sci/coq/coq-8.0_beta.ebuild,v 1.2 2004/06/24 21:56:14 agriffis Exp $
-
-IUSE="norealanalysis debug"
-
-DESCRIPTION="Coq is a proof assistant written in O'Caml"
-HOMEPAGE="http://coq.inria.fr/"
-SRC_URI="ftp://ftp.inria.fr/INRIA/${PN}/V${PV/_/}/${P/_/}.tar.gz"
-
-LICENSE="LGPL-2.1"
-SLOT="0"
-KEYWORDS="~x86 ~ppc"
-
-DEPEND=">=dev-lang/ocaml-3.06"
-
-S="${WORKDIR}/${P/_/}"
-
-src_compile() {
-	local myconf="--prefix /usr \
-		--bindir /usr/bin \
-		--libdir /usr/lib/coq \
-		--mandir /usr/man \
-		--emacslib /usr/share/emacs/site-lisp"
-
-	use debug && myconf="--debug $myconf"
-	use norealanalysis && myconf="$myconf --reals"
-	use norealanalysis || myconf="$myconf --reals all"
-
-	./configure $myconf || die
-
-	emake world || die
-}
-
-src_install() {
-	make COQINSTALLPREFIX=${D} install || die
-	dodoc README CREDITS CHANGES LICENSE
-}
diff --git a/app-sci/coq/files/digest-coq-8.0-r1 b/app-sci/coq/files/digest-coq-8.0-r1
new file mode 100644
index 000000000000..73335eb85772
--- /dev/null
+++ b/app-sci/coq/files/digest-coq-8.0-r1
@@ -0,0 +1,2 @@
+MD5 95237e64081d7306fdea49e1988bde12 coq-8.0pl1.tar.gz 2272613
+MD5 58a3c3c6e3903b0267857d283047c7e3 coq-8.0pl1-translator.tar.gz 233233
diff --git a/app-sci/coq/files/digest-coq-8.0_beta b/app-sci/coq/files/digest-coq-8.0_beta
deleted file mode 100644
index 150e17bc1f6f..000000000000
--- a/app-sci/coq/files/digest-coq-8.0_beta
+++ /dev/null
@@ -1 +0,0 @@
-MD5 6b1a3a4a725a12a7a129d3cfbe6cdb62 coq-8.0beta.tar.gz 2248308