diff options
Diffstat (limited to 'sci-mathematics')
| -rw-r--r-- | sci-mathematics/coq/ChangeLog | 10 | ||||
| -rw-r--r-- | sci-mathematics/coq/Manifest | 20 | ||||
| -rw-r--r-- | sci-mathematics/coq/coq-7.4.ebuild | 4 | ||||
| -rw-r--r-- | sci-mathematics/coq/coq-8.0-r1.ebuild | 4 | ||||
| -rw-r--r-- | sci-mathematics/coq/coq-8.0_p3.ebuild (renamed from sci-mathematics/coq/coq-8.0.ebuild) | 27 | ||||
| -rw-r--r-- | sci-mathematics/coq/files/digest-coq-8.0 | 2 | ||||
| -rw-r--r-- | sci-mathematics/coq/files/digest-coq-8.0_p3 | 3 |
7 files changed, 37 insertions, 33 deletions
diff --git a/sci-mathematics/coq/ChangeLog b/sci-mathematics/coq/ChangeLog index ae5f99d6889c..4365618b17e1 100644 --- a/sci-mathematics/coq/ChangeLog +++ b/sci-mathematics/coq/ChangeLog @@ -1,6 +1,12 @@ # ChangeLog for sci-mathematics/coq -# Copyright 2000-2005 Gentoo Foundation; Distributed under the GPL v2 -# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/ChangeLog,v 1.3 2005/04/13 18:38:55 luckyduck Exp $ +# 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 $ + +*coq-8.0_p3 (04 Feb 2006) + + 04 Feb 2006; Matthieu Sozeau <mattam@gentoo.org> -coq-8.0.ebuild, + +coq-8.0_p3.ebuild: + Add latest version, compatible with ocaml-3.09. 13 Apr 2005; Jan Brinkmann <luckyduck@gentoo.org> coq-8.0-r1.ebuild: added ~amd64 to KEYWORDS, fixes #88950 diff --git a/sci-mathematics/coq/Manifest b/sci-mathematics/coq/Manifest index b99382b255e2..812c20a255b3 100644 --- a/sci-mathematics/coq/Manifest +++ b/sci-mathematics/coq/Manifest @@ -1,22 +1,12 @@ ------BEGIN PGP SIGNED MESSAGE----- -Hash: SHA1 - -MD5 cb898371df21f1a9d28fa6e073a5505f coq-8.0.ebuild 1921 -MD5 ec14c64c02c2760bfd7750bb764b41df coq-7.4.ebuild 986 -MD5 26d5c8abe245a9fb5540eea4558e91bf ChangeLog 1990 +MD5 2561503852b06c6950d1e30e0c696835 coq-8.0_p3.ebuild 2059 +MD5 3d54f6b5dc456dd623a0f1ae04864e5c coq-7.4.ebuild 983 +MD5 9cb58d2978f6b0b70fe46dea6cfd1cf7 ChangeLog 2155 MD5 5af6b26df9264817e5b6a292c1436417 metadata.xml 238 -MD5 83bfd344102e7fbd781532543b9a782f coq-8.0-r1.ebuild 2074 +MD5 1df42d2fd48cb3e893cf9761a68098c3 coq-8.0-r1.ebuild 2071 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 86922705a72292e7508baae5bc75e2a3 files/digest-coq-8.0 130 MD5 393c3085f82f205122b4e66c94232ff7 files/ocaml-3.07.patch 333 MD5 5d46723c29afcd1e24e529e5993c3096 files/coq-8.0-byteflags.patch 676 MD5 e5491c930f8f944ed9c3590fdc8492c1 files/coqide.desktop 242 ------BEGIN PGP SIGNATURE----- -Version: GnuPG v1.4.0 (GNU/Linux) - -iD8DBQFCXWdV06ebR+OMO78RAirZAJ97+fqd3K/MqyD8YQSs2fLeyY1xZwCfX1WV -N1PToVe395/xJCpJinFj9lQ= -=+SOF ------END PGP SIGNATURE----- diff --git a/sci-mathematics/coq/coq-7.4.ebuild b/sci-mathematics/coq/coq-7.4.ebuild index b7b288f326c1..34d6b1b16bab 100644 --- a/sci-mathematics/coq/coq-7.4.ebuild +++ b/sci-mathematics/coq/coq-7.4.ebuild @@ -1,6 +1,6 @@ -# Copyright 1999-2005 Gentoo Foundation +# 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.2 2005/04/13 18:38:55 luckyduck Exp $ +# $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 diff --git a/sci-mathematics/coq/coq-8.0-r1.ebuild b/sci-mathematics/coq/coq-8.0-r1.ebuild index 3770c3b2eb24..24f89697c548 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-2005 Gentoo Foundation +# 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.2 2005/04/13 18:38:55 luckyduck Exp $ +# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.0-r1.ebuild,v 1.3 2006/02/04 16:30:27 mattam Exp $ inherit eutils diff --git a/sci-mathematics/coq/coq-8.0.ebuild b/sci-mathematics/coq/coq-8.0_p3.ebuild index c07007872962..75a6aa180150 100644 --- a/sci-mathematics/coq/coq-8.0.ebuild +++ b/sci-mathematics/coq/coq-8.0_p3.ebuild @@ -1,6 +1,6 @@ -# Copyright 1999-2005 Gentoo Foundation +# 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.ebuild,v 1.2 2005/04/13 18:38:55 luckyduck Exp $ +# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.0_p3.ebuild,v 1.1 2006/02/04 16:30:27 mattam Exp $ inherit eutils @@ -8,26 +8,33 @@ IUSE="norealanalysis ide debug translator doc" RESTRICT="nostrip" +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${PV/_/}/${P/_/}.tar.gz -translator? ( ftp://ftp.inria.fr/INRIA/coq/V8.0/coq-8.0-translator.tar.gz )" +SRC_URI="ftp://ftp.inria.fr/INRIA/${PN}/V${MY_PV}/${MY_P}.tar.gz +mirror://gentoo/${P}-ocaml-3.09.patch.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" +KEYWORDS="~x86 ~ppc ~sparc ~amd64" -DEPEND=">=dev-lang/ocaml-3.06 -!>=dev-lang/ocaml-3.08 +DEPEND=">=dev-lang/ocaml-3.08 ide? ( >=dev-ml/lablgtk-2.2.0 )" -S="${WORKDIR}/${P/_/}" +S="${WORKDIR}/${MY_P}" src_unpack() { unpack ${A} cd ${S} - epatch ${FILESDIR}/${P}-byteflags.patch + + if has_version ">=dev-lang/ocaml-3.09"; + then + epatch ${DISTFILES}/${P}-ocaml-3.09.patch.gz + fi } src_compile() { @@ -66,7 +73,7 @@ src_install() { dodoc README CREDITS CHANGES LICENSE if use translator; then - cd ${WORKDIR}/coq-8.0-translator + cd ${WORKDIR}/${MY_P}-translator mv translate-v8 coq-translate-v8 dobin coq-translate-v8 if use doc; then diff --git a/sci-mathematics/coq/files/digest-coq-8.0 b/sci-mathematics/coq/files/digest-coq-8.0 deleted file mode 100644 index c339254dca9e..000000000000 --- a/sci-mathematics/coq/files/digest-coq-8.0 +++ /dev/null @@ -1,2 +0,0 @@ -MD5 75ab1eb131b3469d21ab74377826b32b coq-8.0.tar.gz 2281827 -MD5 e2e4ecc8a552c847a656dcf9e47dd738 coq-8.0-translator.tar.gz 233218 diff --git a/sci-mathematics/coq/files/digest-coq-8.0_p3 b/sci-mathematics/coq/files/digest-coq-8.0_p3 new file mode 100644 index 000000000000..388defd20836 --- /dev/null +++ b/sci-mathematics/coq/files/digest-coq-8.0_p3 @@ -0,0 +1,3 @@ +MD5 c98d4cefd119accb1ecdeebb41128822 coq-8.0pl3.tar.gz 2309002 +MD5 028d27ab3b2eb4ac5d223597b655c833 coq-8.0_p3-ocaml-3.09.patch.gz 5256 +MD5 78bbf518d2e15c8306f692707c24be1c coq-8.0pl3-translator.tar.gz 233228 |