diff options
author | Alexis Ballier <aballier@gentoo.org> | 2009-05-18 06:38:23 +0000 |
---|---|---|
committer | Alexis Ballier <aballier@gentoo.org> | 2009-05-18 06:38:23 +0000 |
commit | 4a5b24f7e9040aaf99acd4225949ebd3b97f0988 (patch) | |
tree | ec5ff36972869ed1a98d2f7837307e8cd2f95edb /sci-mathematics/coq | |
parent | OpenSSH HPN patch breakage has been resolved by upstream now. (diff) | |
download | gentoo-2-4a5b24f7e9040aaf99acd4225949ebd3b97f0988.tar.gz gentoo-2-4a5b24f7e9040aaf99acd4225949ebd3b97f0988.tar.bz2 gentoo-2-4a5b24f7e9040aaf99acd4225949ebd3b97f0988.zip |
remove old
(Portage version: 2.2_rc33/cvs/Linux x86_64)
Diffstat (limited to 'sci-mathematics/coq')
-rw-r--r-- | sci-mathematics/coq/ChangeLog | 8 | ||||
-rw-r--r-- | sci-mathematics/coq/coq-8.1_p3-r1.ebuild | 76 | ||||
-rw-r--r-- | sci-mathematics/coq/coq-8.1_p3.ebuild | 92 | ||||
-rw-r--r-- | sci-mathematics/coq/metadata.xml | 2 |
4 files changed, 6 insertions, 172 deletions
diff --git a/sci-mathematics/coq/ChangeLog b/sci-mathematics/coq/ChangeLog index a6dcc01a4c58..fdaaa8fd68ef 100644 --- a/sci-mathematics/coq/ChangeLog +++ b/sci-mathematics/coq/ChangeLog @@ -1,6 +1,10 @@ # ChangeLog for sci-mathematics/coq -# Copyright 2000-2009 Gentoo Foundation; Distributed under the GPL v2 -# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/ChangeLog,v 1.40 2009/02/18 18:07:53 aballier Exp $ +# 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 $ + + 18 May 2009; Alexis Ballier <aballier@gentoo.org> -coq-8.1_p3.ebuild, + -coq-8.1_p3-r1.ebuild, metadata.xml: + remove old *coq-8.2 (18 Feb 2009) diff --git a/sci-mathematics/coq/coq-8.1_p3-r1.ebuild b/sci-mathematics/coq/coq-8.1_p3-r1.ebuild deleted file mode 100644 index 6f0119a716b6..000000000000 --- a/sci-mathematics/coq/coq-8.1_p3-r1.ebuild +++ /dev/null @@ -1,76 +0,0 @@ -# Copyright 1999-2008 Gentoo Foundation -# Distributed under the terms of the GNU General Public License v2 -# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.1_p3-r1.ebuild,v 1.2 2008/12/31 03:41:46 mr_bones_ Exp $ - -EAPI="2" - -inherit eutils multilib - -RESTRICT="strip installsources" - -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" -IUSE="norealanalysis ide debug +ocamlopt" - -DEPEND=">=dev-lang/ocaml-3.10[ocamlopt?] - >=dev-ml/camlp5-5.09[ocamlopt?] - ide? ( >=dev-ml/lablgtk-2.10.1[ocamlopt?] )" - -S="${WORKDIR}/${MY_P}" - -src_prepare() { - epatch "${FILESDIR}/${P}-noocamlopt.patch" - epatch "${FILESDIR}/${P}-cmxa-install.dpatch" -} - -src_configure() { - 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 - --camlp5dir +camlp5" - - use debug && myconf="--debug $myconf" - use norealanalysis && myconf="$myconf --reals no" - use norealanalysis || myconf="$myconf --reals all" - - if use ide; 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" - - ./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 -} - -src_compile() { - emake -j1 || die "make failed" -} - -src_install() { - emake COQINSTALLPREFIX="${D}" install || die - dodoc README CREDITS CHANGES - - if use ide; then - domenu "${FILESDIR}/coqide.desktop" - fi -} diff --git a/sci-mathematics/coq/coq-8.1_p3.ebuild b/sci-mathematics/coq/coq-8.1_p3.ebuild deleted file mode 100644 index 7f27a7f8bb4e..000000000000 --- a/sci-mathematics/coq/coq-8.1_p3.ebuild +++ /dev/null @@ -1,92 +0,0 @@ -# Copyright 1999-2008 Gentoo Foundation -# Distributed under the terms of the GNU General Public License v2 -# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.1_p3.ebuild,v 1.9 2008/04/08 15:06:35 armin76 Exp $ - -inherit eutils multilib - -EAPI="1" - -IUSE="norealanalysis ide debug +ocamlopt" - -RESTRICT="strip installsources" - -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-lang/ocaml-3.10 >=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}" - -coq_need_ocamlopt() { - if use ocamlopt && ! built_with_use --missing true $1 ocamlopt; then - eerror "In order to build ${PN} with native code support from ocaml" - eerror "You first need to have a native code ocaml compiler and the related libraries." - eerror "You need to install $1 with ocamlopt useflag on." - die "Please install $1 with ocamlopt useflag" - fi -} - -pkg_setup() { - coq_need_ocamlopt 'dev-lang/ocaml' - use ide && coq_need_ocamlopt 'dev-ml/lablgtk' - has_version '>=dev-lang/ocaml-3.10.0' && coq_need_ocamlopt 'dev-ml/camlp5' -} - -src_unpack() { - unpack ${A} - cd "${S}" - - epatch "${FILESDIR}/${P}-noocamlopt.patch" - epatch "${FILESDIR}/${P}-cmxa-install.dpatch" -} - -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 - use ocamlopt && myconf="$myconf --coqide opt" - use ocamlopt || myconf="$myconf --coqide byte" - else - myconf="$myconf --coqide no" - fi - use ocamlopt || myconf="$myconf -byte-only" - - ./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 || die "make failed" -} - -src_install() { - emake COQINSTALLPREFIX="${D}" install || die - dodoc README CREDITS CHANGES - - if use ide; then - domenu "${FILESDIR}/coqide.desktop" - fi -} diff --git a/sci-mathematics/coq/metadata.xml b/sci-mathematics/coq/metadata.xml index 4eddd15b741c..059bdea3f8ec 100644 --- a/sci-mathematics/coq/metadata.xml +++ b/sci-mathematics/coq/metadata.xml @@ -4,8 +4,6 @@ <herd>sci</herd> <herd>ml</herd> <use> - <flag name='ide'>Build the Coq IDE, a clone of proof general using - <pkg>dev-ml/lablgtk</pkg></flag> <flag name='norealanalysis'>Do not build real analysis modules (faster compilation)</flag> </use> |