proj/gentoo: Initial commit

This commit represents a new era for Gentoo:
Storing the gentoo-x86 tree in Git, as converted from CVS.

This commit is the start of the NEW history.
Any historical data is intended to be grafted onto this point.

Creation process:
1. Take final CVS checkout snapshot
2. Remove ALL ChangeLog* files
3. Transform all Manifests to thin
4. Remove empty Manifests
5. Convert all stale $Header$/$Id$ CVS keywords to non-expanded Git $Id$
5.1. Do not touch files with -kb/-ko keyword flags.

Signed-off-by: Robin H. Johnson <robbat2@gentoo.org>
X-Thanks: Alec Warner <antarus@gentoo.org> - did the GSoC 2006 migration tests
X-Thanks: Robin H. Johnson <robbat2@gentoo.org> - infra guy, herding this project
X-Thanks: Nguyen Thai Ngoc Duy <pclouds@gentoo.org> - Former Gentoo developer, wrote Git features for the migration
X-Thanks: Brian Harring <ferringb@gentoo.org> - wrote much python to improve cvs2svn
X-Thanks: Rich Freeman <rich0@gentoo.org> - validation scripts
X-Thanks: Patrick Lauer <patrick@gentoo.org> - Gentoo dev, running new 2014 work in migration
X-Thanks: Michał Górny <mgorny@gentoo.org> - scripts, QA, nagging
X-Thanks: All of other Gentoo developers - many ideas and lots of paint on the bikeshed

13 files changed, 632 insertions, 0 deletions

diff --git a/sci-mathematics/coq/Manifest b/sci-mathematics/coq/Manifest
new file mode 100644
index 000000000000..d322df030f8f
--- /dev/null
+++ b/sci-mathematics/coq/Manifest
@@ -0,0 +1,6 @@
+DIST coq-8.3pl1.tar.gz 3756961 SHA256 3a497386bd74f43a5af1d0c53f29a017ce7ed1b1e60c052217fe04b7f40be928
+DIST coq-8.4pl1.tar.gz 4139808 SHA256 5d0e4553ab50677a94b4d5ca1650a90718e9362082a649ba95be4010390a0f80 SHA512 dc0073d2cbce91ac27749d84de1b350ad71632555a682d8af6612768d2c92311eb1fd36b7370e0fb630d540639a1c7e16f26a9de25d03d82c3a6eefb99aa3420 WHIRLPOOL e912b97ba1f91d3398d569a588d7cb420389c88971847e66ddff38c3fc715e45842aab285e343c0c6339da659f324ee7b60f37fd0cdcd5a8ce27ab0e8cce915a
+DIST coq-8.4pl2.tar.gz 4145112 SHA256 fb719a38f613b01861e3b251e745a5c8ef395a26ce7029668e85ac75fcbca2d8 SHA512 151291a508c56f9fdc9efd96096852e94c247724030ad13122ad729476f3f7d4885c9202737d9109b6fa7f58029d3b9e8f472a7e587e0b60a49a0224ac399031 WHIRLPOOL ac338571da5f6efc08e9184f1e13b9783bd750627c70af2eee46116d2d949e61a0cbf31745373ccea3b3b862c1188316c2aa3b38e211a398185503c2844a33c5
+DIST coq-8.4pl3.tar.gz 4064579 SHA256 97583d637f981c5554007f4e99ce6420ebc737186b1d021bd71766fd891cfb38 SHA512 e4a385b10b30159545c283e11400f5790a6ca1b91632afe93b73c6a8b523fd408db173b25a1797f69bdfde9a16b37751944041aa9be5a1194b0fe49a9bb56240 WHIRLPOOL c44cc9f55f25dfb37d7b011c3ede3ad47f7191b02a6258bd4bda67854b9cce0e32b412ead826a5ca7a21dc2fe8841774231cb0693da335f5146172463ec57aa2
+DIST coq-8.4pl5.tar.gz 4070062 SHA256 35815ab78a58d72799eacaab155427620ab071677882ca6c98d7bfec97d25245 SHA512 0965ff409933d601a5c96963ea805ce20dd22f1fd9a9473898de1b376403b4e7a9a86b36b58eb1480cfb3a25970626e1dcd225899c089f5a301f4809e7f8f242 WHIRLPOOL 6dea97e7fe655a33757e8f031b28f91f98558e53205890d6b9d928d5641c05814f8d743cb02c39b26dcf93aa4076c5bbd9710a7dfd9f6a3456e38039b0cb8220
+DIST coq-8.4pl6.tar.gz 4099815 SHA256 a540a231a9970a49353ca039f3544616ff86a208966ab1c593779ae13c91ebd6 SHA512 238bc6e28348f40f5619aa28d2e871179d9edeb6eb3f2521af6f407e24a889c8c68fa11c8b12e026f016f0fb7d5006447c3ab7eeae0804fc082d65774aefe0ef WHIRLPOOL 2120dcddce773d90ba024e97fc00df3d563edf398eaf0bbb3dc1df1265b5e657cb4044d334f598898c30a88f0579b35b38f1d6bad4ea5e373a0a30826b245e99
diff --git a/sci-mathematics/coq/coq-8.3_p1.ebuild b/sci-mathematics/coq/coq-8.3_p1.ebuild
new file mode 100644
index 000000000000..28c3feb39ecc
--- /dev/null
+++ b/sci-mathematics/coq/coq-8.3_p1.ebuild
@@ -0,0 +1,81 @@
+# Copyright 1999-2014 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Id$
+
+EAPI="2"
+
+inherit eutils multilib
+
+MY_PV=${PV/_p/pl}
+MY_P=${PN}-${MY_PV}
+
+DESCRIPTION="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
+		dev-texlive/texlive-mathextra
+		dev-texlive/texlive-latexextra
+		)"
+
+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 :)
+	# It replaces \"$LABLGTKLIB\" by $LABLGTKLIB
+	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"
+}
diff --git a/sci-mathematics/coq/coq-8.4_p1.ebuild b/sci-mathematics/coq/coq-8.4_p1.ebuild
new file mode 100644
index 000000000000..0f01228661f9
--- /dev/null
+++ b/sci-mathematics/coq/coq-8.4_p1.ebuild
@@ -0,0 +1,81 @@
+# Copyright 1999-2014 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Id$
+
+EAPI="5"
+
+inherit eutils multilib
+
+MY_PV=${PV/_p/pl}
+MY_P=${PN}-${MY_PV}
+
+DESCRIPTION="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 camlp5"
+
+RDEPEND=">=dev-lang/ocaml-3.11.2:=[ocamlopt?]
+	camlp5? ( >=dev-ml/camlp5-6.02.3:=[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
+		dev-texlive/texlive-mathextra
+		dev-texlive/texlive-latexextra
+		)"
+
+S=${WORKDIR}/${MY_P}
+
+src_prepare() {
+	epatch "${FILESDIR}/${P}-camlp4.patch"
+}
+
+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}
+		--configdir /etc/xdg/${PN}
+		--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"
+
+	use camlp5 || myconf="$myconf --usecamlp4"
+	use camlp5 && myconf="$myconf --camlp5dir ${ocaml_lib}/camlp5"
+
+	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 && make_desktop_entry "/usr/bin/coqide" "Coq IDE" "/usr/share/coq/coq.png"
+}
diff --git a/sci-mathematics/coq/coq-8.4_p2.ebuild b/sci-mathematics/coq/coq-8.4_p2.ebuild
new file mode 100644
index 000000000000..15fb377f1b5f
--- /dev/null
+++ b/sci-mathematics/coq/coq-8.4_p2.ebuild
@@ -0,0 +1,78 @@
+# Copyright 1999-2014 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Id$
+
+EAPI="5"
+
+inherit eutils multilib
+
+MY_PV=${PV/_p/pl}
+MY_P=${PN}-${MY_PV}
+
+DESCRIPTION="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 camlp5"
+
+RDEPEND="
+	>=dev-lang/ocaml-3.11.2:=[ocamlopt?]
+	camlp5? ( >=dev-ml/camlp5-6.02.3:=[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
+		dev-texlive/texlive-mathextra
+		dev-texlive/texlive-latexextra
+		)"
+
+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}
+		--configdir /etc/xdg/${PN}
+		--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"
+
+	use camlp5 || myconf="$myconf --usecamlp4"
+	use camlp5 && myconf="$myconf --camlp5dir ${ocaml_lib}/camlp5"
+
+	export CAML_LD_LIBRARY_PATH="${S}/kernel/byterun/"
+	./configure $myconf || die "configure failed"
+}
+
+src_compile() {
+	emake STRIP="true" -j1
+}
+
+src_install() {
+	emake STRIP="true" COQINSTALLPREFIX="${D}" install
+	dodoc README CREDITS CHANGES
+
+	use gtk && make_desktop_entry "/usr/bin/coqide" "Coq IDE" "/usr/share/coq/coq.png"
+}
diff --git a/sci-mathematics/coq/coq-8.4_p3.ebuild b/sci-mathematics/coq/coq-8.4_p3.ebuild
new file mode 100644
index 000000000000..25516ad987ee
--- /dev/null
+++ b/sci-mathematics/coq/coq-8.4_p3.ebuild
@@ -0,0 +1,90 @@
+# Copyright 1999-2014 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Id$
+
+EAPI="5"
+
+inherit eutils multilib
+
+MY_PV=${PV/_p/pl}
+MY_P=${PN}-${MY_PV}
+
+DESCRIPTION="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 camlp5"
+
+RDEPEND="
+	>=dev-lang/ocaml-3.11.2:=[ocamlopt?]
+	camlp5? ( >=dev-ml/camlp5-6.02.3:=[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
+		dev-texlive/texlive-mathextra
+		dev-texlive/texlive-latexextra
+		)"
+
+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}
+		--configdir /etc/xdg/${PN}
+		--lablgtkdir ${ocaml_lib}/lablgtk2
+		)
+
+	use debug && myconf+=( --debug )
+	use doc || myconf+=( --with-doc no )
+
+	if use gtk; then
+		if use ocamlopt; then
+			myconf+=( --coqide opt )
+		else
+			myconf+=( --coqide byte )
+		fi
+	else
+		myconf+=( --coqide no )
+	fi
+
+	if use ocamlopt; then
+		myconf+=( --opt )
+	else
+		myconf+=( -byte-only )
+	fi
+
+	if use camlp5; then
+		myconf+=( --camlp5dir ${ocaml_lib}/camlp5 )
+	else
+		myconf+=( --usecamlp4 )
+	fi
+
+	export CAML_LD_LIBRARY_PATH="${S}/kernel/byterun/"
+	./configure ${myconf[@]} || die "configure failed"
+}
+
+src_compile() {
+	emake STRIP="true" -j1
+}
+
+src_install() {
+	emake STRIP="true" COQINSTALLPREFIX="${D}" install
+	dodoc README CREDITS CHANGES
+
+	use gtk && make_desktop_entry "coqide" "Coq IDE" "${EPREFIX}/usr/share/coq/coq.png"
+}
diff --git a/sci-mathematics/coq/coq-8.4_p5.ebuild b/sci-mathematics/coq/coq-8.4_p5.ebuild
new file mode 100644
index 000000000000..9840c716d59b
--- /dev/null
+++ b/sci-mathematics/coq/coq-8.4_p5.ebuild
@@ -0,0 +1,103 @@
+# Copyright 1999-2015 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Id$
+
+EAPI="5"
+
+inherit eutils multilib
+
+MY_PV=${PV/_p/pl}
+MY_P=${PN}-${MY_PV}
+
+DESCRIPTION="Proof assistant written in O'Caml"
+HOMEPAGE="http://coq.inria.fr/"
+SRC_URI="http://${PN}.inria.fr/distrib/V${MY_PV}/files/${MY_P}.tar.gz"
+
+LICENSE="LGPL-2.1"
+SLOT="0"
+KEYWORDS="amd64 ~ppc ~x86"
+IUSE="gtk debug +ocamlopt doc camlp5"
+
+RDEPEND="
+	>=dev-lang/ocaml-3.11.2:=[ocamlopt?]
+	camlp5? ( >=dev-ml/camlp5-6.02.3:=[ocamlopt?] )
+	!camlp5? ( || ( dev-ml/camlp4:= <dev-lang/ocaml-4.02.0 ) )
+	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
+		dev-texlive/texlive-mathextra
+		dev-texlive/texlive-latexextra
+		)"
+
+S=${WORKDIR}/${MY_P}
+
+src_prepare() {
+	epatch "${FILESDIR}/${PN}-8.4_p5-do-not-install-revision.patch"
+	# Fix generation of the index_urls.txt file with Gentoo dev-tex/hevea versions.
+	# http://lists.gforge.inria.fr/pipermail/coq-commits/2014-October/013582.html
+	epatch "${FILESDIR}/${P}-hevea.patch"
+	epatch "${FILESDIR}/${PN}-8.4_p5-no-clean-before-test.patch"
+}
+
+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}
+		--configdir /etc/xdg/${PN}
+		--lablgtkdir ${ocaml_lib}/lablgtk2
+		)
+
+	use debug && myconf+=( --debug )
+	use doc || myconf+=( --with-doc no )
+
+	if use gtk; then
+		if use ocamlopt; then
+			myconf+=( --coqide opt )
+		else
+			myconf+=( --coqide byte )
+		fi
+	else
+		myconf+=( --coqide no )
+	fi
+
+	if use ocamlopt; then
+		myconf+=( --opt )
+	else
+		myconf+=( -byte-only )
+	fi
+
+	if use camlp5; then
+		myconf+=( --camlp5dir ${ocaml_lib}/camlp5 )
+	else
+		myconf+=( --usecamlp4 )
+	fi
+
+	export CAML_LD_LIBRARY_PATH="${S}/kernel/byterun/"
+	./configure ${myconf[@]} || die "configure failed"
+}
+
+src_compile() {
+	emake STRIP="true" -j1 world VERBOSE=1
+}
+
+src_test() {
+	emake STRIP="true" check VERBOSE=1
+}
+
+src_install() {
+	emake STRIP="true" COQINSTALLPREFIX="${D}" install VERBOSE=1
+	dodoc README CREDITS CHANGES
+
+	use gtk && make_desktop_entry "coqide" "Coq IDE" "${EPREFIX}/usr/share/coq/coq.png"
+}
diff --git a/sci-mathematics/coq/coq-8.4_p6.ebuild b/sci-mathematics/coq/coq-8.4_p6.ebuild
new file mode 100644
index 000000000000..be183f11229d
--- /dev/null
+++ b/sci-mathematics/coq/coq-8.4_p6.ebuild
@@ -0,0 +1,103 @@
+# Copyright 1999-2015 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Id$
+
+EAPI="5"
+
+inherit eutils multilib
+
+MY_PV=${PV/_p/pl}
+MY_P=${PN}-${MY_PV}
+
+DESCRIPTION="Proof assistant written in O'Caml"
+HOMEPAGE="http://coq.inria.fr/"
+SRC_URI="http://${PN}.inria.fr/distrib/V${MY_PV}/files/${MY_P}.tar.gz"
+
+LICENSE="LGPL-2.1"
+SLOT="0"
+KEYWORDS="~amd64 ~ppc ~x86"
+IUSE="gtk debug +ocamlopt doc camlp5"
+
+RDEPEND="
+	>=dev-lang/ocaml-3.11.2:=[ocamlopt?]
+	camlp5? ( >=dev-ml/camlp5-6.02.3:=[ocamlopt?] )
+	!camlp5? ( || ( dev-ml/camlp4:= <dev-lang/ocaml-4.02.0 ) )
+	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
+		dev-texlive/texlive-mathextra
+		dev-texlive/texlive-latexextra
+		)"
+
+S=${WORKDIR}/${MY_P}
+
+src_prepare() {
+	epatch "${FILESDIR}/${PN}-8.4_p5-do-not-install-revision.patch"
+	# Fix generation of the index_urls.txt file with Gentoo dev-tex/hevea versions.
+	# http://lists.gforge.inria.fr/pipermail/coq-commits/2014-October/013582.html
+	epatch "${FILESDIR}/${PN}-8.4_p5-hevea.patch"
+	epatch "${FILESDIR}/${PN}-8.4_p5-no-clean-before-test.patch"
+}
+
+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}
+		--configdir /etc/xdg/${PN}
+		--lablgtkdir ${ocaml_lib}/lablgtk2
+		)
+
+	use debug && myconf+=( --debug )
+	use doc || myconf+=( --with-doc no )
+
+	if use gtk; then
+		if use ocamlopt; then
+			myconf+=( --coqide opt )
+		else
+			myconf+=( --coqide byte )
+		fi
+	else
+		myconf+=( --coqide no )
+	fi
+
+	if use ocamlopt; then
+		myconf+=( --opt )
+	else
+		myconf+=( -byte-only )
+	fi
+
+	if use camlp5; then
+		myconf+=( --camlp5dir ${ocaml_lib}/camlp5 )
+	else
+		myconf+=( --usecamlp4 )
+	fi
+
+	export CAML_LD_LIBRARY_PATH="${S}/kernel/byterun/"
+	./configure ${myconf[@]} || die "configure failed"
+}
+
+src_compile() {
+	emake STRIP="true" -j1 world VERBOSE=1
+}
+
+src_test() {
+	emake STRIP="true" check VERBOSE=1
+}
+
+src_install() {
+	emake STRIP="true" COQINSTALLPREFIX="${D}" install VERBOSE=1
+	dodoc README CREDITS CHANGES
+
+	use gtk && make_desktop_entry "coqide" "Coq IDE" "${EPREFIX}/usr/share/coq/coq.png"
+}
diff --git a/sci-mathematics/coq/files/coq-8.4_p1-camlp4.patch b/sci-mathematics/coq/files/coq-8.4_p1-camlp4.patch
new file mode 100644
index 000000000000..bc60b9f56f4c
--- /dev/null
+++ b/sci-mathematics/coq/files/coq-8.4_p1-camlp4.patch
@@ -0,0 +1,17 @@
+Upstream rev 16121
+https://bugs.gentoo.org/show_bug.cgi?id=450954
+
+Index: coq-8.4pl1/scripts/coqmktop.ml
+===================================================================
+--- coq-8.4pl1.orig/scripts/coqmktop.ml
++++ coq-8.4pl1/scripts/coqmktop.ml
+@@ -45,8 +45,7 @@ let camlp4topobjs =
+     [ "Camlp4Top.cmo";
+       "Camlp4Parsers/Camlp4OCamlRevisedParser.cmo";
+       "Camlp4Parsers/Camlp4OCamlParser.cmo";
+-      "Camlp4Parsers/Camlp4GrammarParser.cmo";
+-      "q_util.cmo"; "q_coqast.cmo" ]
++      "Camlp4Parsers/Camlp4GrammarParser.cmo" ]
+ let topobjs = camlp4topobjs
+ 
+ let gramobjs = []
diff --git a/sci-mathematics/coq/files/coq-8.4_p5-do-not-install-revision.patch b/sci-mathematics/coq/files/coq-8.4_p5-do-not-install-revision.patch
new file mode 100644
index 000000000000..e97f4a165f87
--- /dev/null
+++ b/sci-mathematics/coq/files/coq-8.4_p5-do-not-install-revision.patch
@@ -0,0 +1,19 @@
+--- coq-8.4pl5-orig/Makefile.build	2014-10-22 19:30:53.000000000 +1100
++++ coq-8.4pl5/Makefile.build	2015-02-15 12:06:48.044999959 +1100
+@@ -655,16 +655,12 @@
+ # it with libraries
+ 	-$(MKDIR) $(FULLCOQLIB)/plugins/micromega
+ 	$(INSTALLBIN) $(CSDPCERT) $(FULLCOQLIB)/plugins/micromega
+-	rm -f $(FULLCOQLIB)/revision
+-	-$(INSTALLLIB) revision $(FULLCOQLIB)
+ 
+ install-library-light:
+ 	$(MKDIR) $(FULLCOQLIB)
+ 	$(INSTALLSH) $(FULLCOQLIB) $(LIBFILESLIGHT) $(INITPLUGINS)
+ 	$(MKDIR) $(FULLCOQLIB)/states
+ 	$(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states
+-	rm -f $(FULLCOQLIB)/revision
+-	-$(INSTALLLIB) revision $(FULLCOQLIB)
+ ifeq ($(BEST),opt)
+ 	$(INSTALLSH)  $(FULLCOQLIB) $(INITPLUGINSOPT)
+ endif
diff --git a/sci-mathematics/coq/files/coq-8.4_p5-hevea.patch b/sci-mathematics/coq/files/coq-8.4_p5-hevea.patch
new file mode 100644
index 000000000000..c76f1dea8e11
--- /dev/null
+++ b/sci-mathematics/coq/files/coq-8.4_p5-hevea.patch
@@ -0,0 +1,11 @@
+--- coq-8.4pl5-orig/Makefile.doc	2014-10-22 19:30:53.000000000 +1100
++++ coq-8.4pl5/Makefile.doc	2015-02-15 15:28:34.797911303 +1100
+@@ -148,7 +148,7 @@
+ ######################################################################
+ 
+ $(INDEXURLS): $(INDEXES)
+-	cat $< | grep li-indexenv | grep HREF | sed -e 's@.*<TT>\(.*\)</TT>.*, <A HREF="\(.*\)">.*@\1,\2@' > $@
++	cat $< | grep li-indexenv | grep href | sed -e 's@.*>\([^<]*\)</span>.*, <a href="\([^"]*\)">.*@\1,\2@' > $@
+ 
+ 
+ ######################################################################
diff --git a/sci-mathematics/coq/files/coq-8.4_p5-no-clean-before-test.patch b/sci-mathematics/coq/files/coq-8.4_p5-no-clean-before-test.patch
new file mode 100644
index 000000000000..ef4b6cf3e824
--- /dev/null
+++ b/sci-mathematics/coq/files/coq-8.4_p5-no-clean-before-test.patch
@@ -0,0 +1,12 @@
+--- coq-8.4pl5-orig/Makefile.build	2015-02-15 12:06:48.044999959 +1100
++++ coq-8.4pl5/Makefile.build	2015-02-15 16:41:06.521892146 +1100
+@@ -395,8 +395,7 @@
+ 
+ check:: validate test-suite
+ 
+-test-suite: world $(ALLSTDLIB).v
+-	$(MAKE) $(MAKE_TSOPTS) clean
++test-suite: $(ALLSTDLIB).v
+ 	$(MAKE) $(MAKE_TSOPTS) all
+ 	$(HIDE)if grep -F 'Error!' test-suite/summary.log ; then false; fi
+ 
diff --git a/sci-mathematics/coq/files/coqide.desktop b/sci-mathematics/coq/files/coqide.desktop
new file mode 100644
index 000000000000..cc8bb54e1ad1
--- /dev/null
+++ b/sci-mathematics/coq/files/coqide.desktop
@@ -0,0 +1,9 @@
+[Desktop Entry]
+Comment=Coq integrated developpment environment
+Icon=/usr/lib/coq/ide/coq.png
+Exec=/usr/bin/coqide
+Name=CoqIDE
+GenericName=Coq IDE
+Terminal=false
+Type=Application
+Categories=Science;Math;
diff --git a/sci-mathematics/coq/metadata.xml b/sci-mathematics/coq/metadata.xml
new file mode 100644
index 000000000000..2fbebc05a0d7
--- /dev/null
+++ b/sci-mathematics/coq/metadata.xml
@@ -0,0 +1,22 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
+<pkgmetadata>
+  <herd>ml</herd>
+  <herd>sci-mathematics</herd>
+  <longdescription lang="en">
+  Developed in the LogiCal project, the Coq tool is a formal proof
+  management system: a proof done with Coq is mechanically checked
+  by the machine.
+  In particular, Coq allows:
+  * the definition of functions or predicates,
+  * to state mathematical theorems and software specifications,
+  * to develop interactively formal proofs of these theorems,
+  * to check these proofs by a small certification "kernel".
+  Coq is based on a logical framework called "Calculus of Inductive
+  Constructions" extended by a modular development system for
+  theories.
+</longdescription>
+  <use>
+    <flag name="camlp5">Build using camlp5. This is required for some plugins like Ssreflect.</flag>
+  </use>
+</pkgmetadata>