summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMatthieu Sozeau <mattam@gentoo.org>2006-02-04 17:15:51 +0000
committerMatthieu Sozeau <mattam@gentoo.org>2006-02-04 17:15:51 +0000
commit4c6c6155f68c30852d5d153387cc5c36aa6bc924 (patch)
tree386ae675a97b7df2603438c5ab7092ba9d7d1ac7 /sci-mathematics/coq
parentMark 2.12.0 stable on alpha (diff)
downloadhistorical-4c6c6155f68c30852d5d153387cc5c36aa6bc924.tar.gz
historical-4c6c6155f68c30852d5d153387cc5c36aa6bc924.tar.bz2
historical-4c6c6155f68c30852d5d153387cc5c36aa6bc924.zip
Remove old version, incompatible with current ocaml and move current to stable (over a year of testing:)
Package-Manager: portage-2.0.51.22-r1
Diffstat (limited to 'sci-mathematics/coq')
-rw-r--r--sci-mathematics/coq/ChangeLog6
-rw-r--r--sci-mathematics/coq/Manifest6
-rw-r--r--sci-mathematics/coq/coq-7.4.ebuild40
-rw-r--r--sci-mathematics/coq/coq-8.0-r1.ebuild4
-rw-r--r--sci-mathematics/coq/files/digest-coq-7.41
5 files changed, 9 insertions, 48 deletions
diff --git a/sci-mathematics/coq/ChangeLog b/sci-mathematics/coq/ChangeLog
index 4365618b17e1..9ac848b86bfe 100644
--- a/sci-mathematics/coq/ChangeLog
+++ b/sci-mathematics/coq/ChangeLog
@@ -1,6 +1,10 @@
# ChangeLog for sci-mathematics/coq
# Copyright 2000-2006 Gentoo Foundation; Distributed under the GPL v2
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/ChangeLog,v 1.4 2006/02/04 16:30:27 mattam Exp $
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/ChangeLog,v 1.5 2006/02/04 17:15:51 mattam Exp $
+
+ 04 Feb 2006; Matthieu Sozeau <mattam@gentoo.org> -coq-7.4.ebuild,
+ coq-8.0-r1.ebuild:
+ Remove old 7.4 version and move 8.0-r1 to stable on x86 and ppc.
*coq-8.0_p3 (04 Feb 2006)
diff --git a/sci-mathematics/coq/Manifest b/sci-mathematics/coq/Manifest
index 812c20a255b3..d81cce0951e5 100644
--- a/sci-mathematics/coq/Manifest
+++ b/sci-mathematics/coq/Manifest
@@ -1,12 +1,10 @@
MD5 2561503852b06c6950d1e30e0c696835 coq-8.0_p3.ebuild 2059
-MD5 3d54f6b5dc456dd623a0f1ae04864e5c coq-7.4.ebuild 983
-MD5 9cb58d2978f6b0b70fe46dea6cfd1cf7 ChangeLog 2155
+MD5 f53f121e28c13d7bc92083befddc19f0 ChangeLog 2312
MD5 5af6b26df9264817e5b6a292c1436417 metadata.xml 238
-MD5 1df42d2fd48cb3e893cf9761a68098c3 coq-8.0-r1.ebuild 2071
+MD5 cb991d5ec534868ff853690657f2e104 coq-8.0-r1.ebuild 2069
MD5 02ac210c6af5d8e258a2805a22822a8b files/coq-8.0-ocaml-3.08.1.patch 1321
MD5 dc0f737371101bc7c97b0a80165ddac6 files/digest-coq-8.0-r1 136
MD5 94b1d26b3c8781903409657f25b64f29 files/digest-coq-8.0_p3 209
-MD5 d3f33f3602d82ea691f91b062dbf236b files/digest-coq-7.4 60
MD5 393c3085f82f205122b4e66c94232ff7 files/ocaml-3.07.patch 333
MD5 5d46723c29afcd1e24e529e5993c3096 files/coq-8.0-byteflags.patch 676
MD5 e5491c930f8f944ed9c3590fdc8492c1 files/coqide.desktop 242
diff --git a/sci-mathematics/coq/coq-7.4.ebuild b/sci-mathematics/coq/coq-7.4.ebuild
deleted file mode 100644
index 34d6b1b16bab..000000000000
--- a/sci-mathematics/coq/coq-7.4.ebuild
+++ /dev/null
@@ -1,40 +0,0 @@
-# Copyright 1999-2006 Gentoo Foundation
-# Distributed under the terms of the GNU General Public License v2
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-7.4.ebuild,v 1.3 2006/02/04 16:30:27 mattam Exp $
-
-inherit eutils
-
-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 ~amd64"
-IUSE="norealanalysis"
-
-DEPEND=">=dev-lang/ocaml-3.06
-!>=dev-lang/ocaml-3.08"
-
-src_compile() {
- local myconf="--prefix /usr \
- --bindir /usr/bin \
- --libdir /usr/lib/coq \
- --mandir /usr/man \
- --emacslib /usr/share/emacs/site-lisp"
-
- use norealanalysis \
- && myconf="$myconf --reals" \
- || myconf="$myconf --reals all"
-
- has_version ">=dev-lang/ocaml-3.07" && epatch ${FILESDIR}/ocaml-3.07.patch
-
- ./configure $myconf || die
-
- emake world || die
-}
-
-src_install() {
- make COQINSTALLPREFIX=${D} install || die
- dodoc README CREDITS CHANGES
-}
diff --git a/sci-mathematics/coq/coq-8.0-r1.ebuild b/sci-mathematics/coq/coq-8.0-r1.ebuild
index 24f89697c548..68b030deb7b6 100644
--- a/sci-mathematics/coq/coq-8.0-r1.ebuild
+++ b/sci-mathematics/coq/coq-8.0-r1.ebuild
@@ -1,6 +1,6 @@
# Copyright 1999-2006 Gentoo Foundation
# Distributed under the terms of the GNU General Public License v2
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.0-r1.ebuild,v 1.3 2006/02/04 16:30:27 mattam Exp $
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.0-r1.ebuild,v 1.4 2006/02/04 17:15:51 mattam Exp $
inherit eutils
@@ -18,7 +18,7 @@ translator? ( ftp://ftp.inria.fr/INRIA/coq/V${MY_PV}/${MY_P}-translator.tar.gz )
LICENSE="LGPL-2.1"
SLOT="0"
-KEYWORDS="~x86 ~ppc ~sparc ~amd64"
+KEYWORDS="x86 ppc ~sparc ~amd64"
DEPEND=">=dev-lang/ocaml-3.06
ide? ( >=dev-ml/lablgtk-2.2.0 )"
diff --git a/sci-mathematics/coq/files/digest-coq-7.4 b/sci-mathematics/coq/files/digest-coq-7.4
deleted file mode 100644
index ab1d3353a4d9..000000000000
--- a/sci-mathematics/coq/files/digest-coq-7.4
+++ /dev/null
@@ -1 +0,0 @@
-MD5 13ac61f150823e54ad84a9096e2dd646 coq-7.4.tar.gz 1537547