version bump

Package-Manager: portage-2.2_rc40/cvs/Linux x86_64

3 files changed, 80 insertions, 5 deletions

diff --git a/sci-mathematics/coq/ChangeLog b/sci-mathematics/coq/ChangeLog
index fdaaa8fd68ef..1184513dcdca 100644
--- a/sci-mathematics/coq/ChangeLog
+++ b/sci-mathematics/coq/ChangeLog
@@ -1,6 +1,11 @@
 # ChangeLog for sci-mathematics/coq
 # Copyright 1999-2009 Gentoo Foundation; Distributed under the GPL v2
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/ChangeLog,v 1.41 2009/05/18 06:38:23 aballier Exp $
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/ChangeLog,v 1.42 2009/08/27 13:11:43 aballier Exp $
+
+*coq-8.2_p1 (27 Aug 2009)
+
+  27 Aug 2009; Alexis Ballier <aballier@gentoo.org> +coq-8.2_p1.ebuild:
+  version bump
 
   18 May 2009; Alexis Ballier <aballier@gentoo.org> -coq-8.1_p3.ebuild,
   -coq-8.1_p3-r1.ebuild, metadata.xml:
diff --git a/sci-mathematics/coq/Manifest b/sci-mathematics/coq/Manifest
index 51958cb552b4..3419c2a88a2d 100644
--- a/sci-mathematics/coq/Manifest
+++ b/sci-mathematics/coq/Manifest
@@ -6,14 +6,16 @@ AUX coq-8.1_p3-noocamlopt.patch 640 RMD160 dce43c53544a7c4d3437841a89b53e4349627
 AUX coqide.desktop 233 RMD160 3f9d112d7f55454f72c42b427005b37971c6e928 SHA1 40571b86c25793e7d4e9bef80f637d7440b03704 SHA256 dba2e81a408ae51e187c2a164794f9505c4abfa0b92f47a44d0e9f96e2b6dfac
 DIST coq-8.1pl4.tar.gz 3009030 RMD160 87dff2cb205951e31e04e5b4596cfd846d309bb2 SHA1 d65f81e465709b52599356d253dd172cc3d395be SHA256 8b78c6b7382426246dab813d9dcdead7d1dc10d26846483fc27d727077588d9d
 DIST coq-8.2.tar.gz 3597544 RMD160 fb8506fa0c469a428a43649a13819bc18949570e SHA1 cac79093f1639c309b400aced13c749f278abbea SHA256 85a828696b960c7e3c55e6680daf5a04dc9edb8849d61abef8e0531378e2d728
+DIST coq-8.2pl1.tar.gz 3600620 RMD160 dd5758a94bb3de49967cec76baa33eb5169659ce SHA1 4aed3302adc2edbaa5d97984512c1c13014bd649 SHA256 7c15acfd369111e51d937cce632d22fc77a6718a5ac9f2dd2dcbdfab4256ae0c
 EBUILD coq-8.1_p4.ebuild 1767 RMD160 3ad1949545093969a7b53896e184cdcd9bf1eff3 SHA1 1716919015434acdf8936bfd0c8891f4c72cdbb7 SHA256 253d8611b132bfb47a1b0fee4cd072e9cb0041a8dce12e4b378b9be049ca7056
 EBUILD coq-8.2.ebuild 1834 RMD160 c2dfe536bb25d7d26db942395324726161f50f43 SHA1 fad970919ed49520ba7c5381dadf113bc90e377f SHA256 9ab95009cfcf003db3831ad02b0152d08b3c1ddd480e82d80eb0e0e17475101e
-MISC ChangeLog 7184 RMD160 fae0c383c1e3b6e79a455e4b6943b0600627fde2 SHA1 0b90b708fbeac0ef91a96591e9044f30cc150b25 SHA256 c74cf95628002d4ccec73d0a88c03e1718603358e37a2c31f80c4f2e6eea5c80
+EBUILD coq-8.2_p1.ebuild 1844 RMD160 6739ad553f921369da14ff597278bae4d8d93a54 SHA1 0b2367d5ee4f6297e0eed64b1bccc47ea3f9eeb5 SHA256 86142bc1f08b74386e53280383bbe49e92e175bac27f134fda4e387175e744ec
+MISC ChangeLog 7299 RMD160 8751b67797046530016c3007af34878a0c515479 SHA1 2041fe5c64c23d516d005e3b11dfc3fcdedbb750 SHA256 f17aa9b305ce6a04d5c29e617a2737a69c6511f2daae93ea89b6a04cde996edc
 MISC metadata.xml 282 RMD160 dfd17179bb9bb01273006a8c00cc941f1a313523 SHA1 bfc493a2aa04b1ee10be87c6e09c3d97e3ecd8e9 SHA256 9885bd063535c49f50e664cde9bba05ce04f880126d126c51768a8ec52780d7c
 -----BEGIN PGP SIGNATURE-----
 Version: GnuPG v2.0.11 (GNU/Linux)
 
-iEYEARECAAYFAkoRAmQACgkQvFcC4BYPU0r17wCgiVXUwvLqZ7DopK1F+irhQZxV
-AHIAn2nhAetBf6WU60vHhIMSG0W0YX1o
-=tQZe
+iEYEARECAAYFAkqWhhQACgkQvFcC4BYPU0poQwCgmE3Jwm4kGAeexAiHE8NFPX8K
++GsAnjYteW3S//4t6nzDy4HYsY+d535M
+=s3nx
 -----END PGP SIGNATURE-----
diff --git a/sci-mathematics/coq/coq-8.2_p1.ebuild b/sci-mathematics/coq/coq-8.2_p1.ebuild
new file mode 100644
index 000000000000..92ef4f5aea29
--- /dev/null
+++ b/sci-mathematics/coq/coq-8.2_p1.ebuild
@@ -0,0 +1,68 @@
+# Copyright 1999-2009 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.2_p1.ebuild,v 1.1 2009/08/27 13:11:43 aballier 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://coq.inria.fr/distrib/V${MY_PV}/files/${MY_P}.tar.gz"
+
+LICENSE="LGPL-2.1"
+SLOT="0"
+KEYWORDS="~amd64 ~ppc ~sparc ~x86"
+IUSE="norealanalysis 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="${RDPEND}
+	doc? ( dev-tex/hevea virtual/latex-base )"
+
+S="${WORKDIR}/${MY_P}"
+
+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 norealanalysis && myconf="$myconf --reals no"
+	use norealanalysis || myconf="$myconf --reals all"
+	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 -j1 || die "make failed"
+}
+
+src_install() {
+	emake COQINSTALLPREFIX="${D}" install || die
+	dodoc README CREDITS CHANGES
+
+	use gtk && domenu "${FILESDIR}/coqide.desktop"
+}