summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAlexis Ballier <aballier@gentoo.org>2007-10-20 15:51:44 +0000
committerAlexis Ballier <aballier@gentoo.org>2007-10-20 15:51:44 +0000
commit5c5530dff9cceb47f17bb94a768f70e570ad71ae (patch)
tree65c9b6cc23271f393b55ebc2cf98c716ee67cbfc /sci-mathematics/coq
parentBackport the speex changes from #193768 to 1.0.14. (diff)
downloadhistorical-5c5530dff9cceb47f17bb94a768f70e570ad71ae.tar.gz
historical-5c5530dff9cceb47f17bb94a768f70e570ad71ae.tar.bz2
historical-5c5530dff9cceb47f17bb94a768f70e570ad71ae.zip
remove old versions
Package-Manager: portage-2.1.3.15
Diffstat (limited to 'sci-mathematics/coq')
-rw-r--r--sci-mathematics/coq/ChangeLog7
-rw-r--r--sci-mathematics/coq/Manifest35
-rw-r--r--sci-mathematics/coq/coq-8.0-r1.ebuild88
-rw-r--r--sci-mathematics/coq/files/coq-8.0-byteflags.patch20
-rw-r--r--sci-mathematics/coq/files/coq-8.0-ocaml-3.08.1.patch29
-rw-r--r--sci-mathematics/coq/files/digest-coq-8.0-r16
-rw-r--r--sci-mathematics/coq/files/ocaml-3.07.patch10
7 files changed, 13 insertions, 182 deletions
diff --git a/sci-mathematics/coq/ChangeLog b/sci-mathematics/coq/ChangeLog
index d16d0a10721c..1540334f880f 100644
--- a/sci-mathematics/coq/ChangeLog
+++ b/sci-mathematics/coq/ChangeLog
@@ -1,6 +1,11 @@
# ChangeLog for sci-mathematics/coq
# Copyright 2000-2007 Gentoo Foundation; Distributed under the GPL v2
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/ChangeLog,v 1.18 2007/10/20 15:37:29 aballier Exp $
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/ChangeLog,v 1.19 2007/10/20 15:51:44 aballier Exp $
+
+ 20 Oct 2007; Alexis Ballier <aballier@gentoo.org> -files/ocaml-3.07.patch,
+ -files/coq-8.0-byteflags.patch, -files/coq-8.0-ocaml-3.08.1.patch,
+ -coq-8.0-r1.ebuild:
+ remove old versions
*coq-8.1_p2 (20 Oct 2007)
diff --git a/sci-mathematics/coq/Manifest b/sci-mathematics/coq/Manifest
index 9a24ddef1e36..c4b796b2a522 100644
--- a/sci-mathematics/coq/Manifest
+++ b/sci-mathematics/coq/Manifest
@@ -1,33 +1,15 @@
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
-AUX coq-8.0-byteflags.patch 676 RMD160 c426bf5a23e83b354574b78f084d521fedc1c325 SHA1 7f2d8d87a2743ed0bfc1cb45ebaf8acf1ddcc11d SHA256 4bdd7fcddd5a1f845be8df40f9a5b7d7fee1cf88bb744866804ab1da4253a2d5
-MD5 5d46723c29afcd1e24e529e5993c3096 files/coq-8.0-byteflags.patch 676
-RMD160 c426bf5a23e83b354574b78f084d521fedc1c325 files/coq-8.0-byteflags.patch 676
-SHA256 4bdd7fcddd5a1f845be8df40f9a5b7d7fee1cf88bb744866804ab1da4253a2d5 files/coq-8.0-byteflags.patch 676
-AUX coq-8.0-ocaml-3.08.1.patch 1321 RMD160 9cacf8590ac611f04f6eeeaca0a9240b1dafc29a SHA1 d99ad532e597eb6b7ad8dde2b5a20ad4c53b8567 SHA256 bd5a0363840f483d98c4b2374f8199b0991f88eea1f152f235efc789d51c4616
-MD5 02ac210c6af5d8e258a2805a22822a8b files/coq-8.0-ocaml-3.08.1.patch 1321
-RMD160 9cacf8590ac611f04f6eeeaca0a9240b1dafc29a files/coq-8.0-ocaml-3.08.1.patch 1321
-SHA256 bd5a0363840f483d98c4b2374f8199b0991f88eea1f152f235efc789d51c4616 files/coq-8.0-ocaml-3.08.1.patch 1321
AUX coqide.desktop 242 RMD160 78d55202099015b63459b8d1366befc26dc0f259 SHA1 fefc588252399b33f34ff8a1f15bdcf13e5d4d0b SHA256 8444a5bdcf66303265c6fbaba67c0f1b6b06a97bd31929d91ca9742da6961a71
MD5 e5491c930f8f944ed9c3590fdc8492c1 files/coqide.desktop 242
RMD160 78d55202099015b63459b8d1366befc26dc0f259 files/coqide.desktop 242
SHA256 8444a5bdcf66303265c6fbaba67c0f1b6b06a97bd31929d91ca9742da6961a71 files/coqide.desktop 242
-AUX ocaml-3.07.patch 333 RMD160 8506611923b6a54b546419df43cda235d8fa042e SHA1 759145d7eb28248dc1d5ae670af20ade6bf30ab1 SHA256 d1cb93dedf8aa61723e897bdaf3aefd5699cb53a5042aeac408fef392095250a
-MD5 393c3085f82f205122b4e66c94232ff7 files/ocaml-3.07.patch 333
-RMD160 8506611923b6a54b546419df43cda235d8fa042e files/ocaml-3.07.patch 333
-SHA256 d1cb93dedf8aa61723e897bdaf3aefd5699cb53a5042aeac408fef392095250a files/ocaml-3.07.patch 333
DIST coq-8.0_p3-ocaml-3.09.patch.gz 5256 RMD160 17dd484a71ddcf5724435ef7386db070b9840949 SHA1 cf270ee2002f3d0f14802fdfc84dbf2d09c5434e SHA256 6eacae4a27de43e5cef2ef8c5971f869bf0df291436aa1ac573fd8bf7ae698fc
-DIST coq-8.0pl1-translator.tar.gz 233233 RMD160 dc241dcd596e5c667a4e8295eb44f23cbfef432e SHA1 b1e016f607aba76267771438481e1f5ed6d09d41 SHA256 baea2c89f52c06062b3c38d3cd9367206dcbb7728a0315d1d2ce49524f4aa340
-DIST coq-8.0pl1.tar.gz 2272613 RMD160 e8437bc84e130757ae4bc46b832a95c0ea655da3 SHA1 6a34bbed937e57b6e783765344004fadf9cd827f SHA256 e90955b200b1bd64093eeebbad173d1228ea9d88aea0615a28de08782024be33
DIST coq-8.0pl3-translator.tar.gz 233228 RMD160 7dd748ee5929faf93ca75bec94b443573405b0fe SHA1 4a62e60759c8bbbf454febc47da0c92a0e9f862e SHA256 78def7e2998526db8c5740580113802a821c31de65bb12a7c74c512f6a9328f7
DIST coq-8.0pl3.tar.gz 2309002 RMD160 925a65fdd0c96f4fe6082bc7bfb8483c83b5fea7 SHA1 b182f25b8e6591139281f7078d049aaa7f0408d8 SHA256 03d02b39873197f5365aad9bc2b917f4db234dcfd4bcff79febd8525770fb84c
DIST coq-8.1pl1.tar.gz 2984726 RMD160 9982d2022abfb2f74dc34cdc6cdd25343f5cb583 SHA1 8142cd21b3d0b5fd56c3b5568550c09cac91a3f8 SHA256 04ffc9c5a31953af6294753118dbb2e41b6aa5aaa5a41f7cf2648afff98f4940
DIST coq-8.1pl2.tar.gz 2997185 RMD160 e45451fdd41b1f979febcfb2c0dbd19a39d09256 SHA1 33ab31abffe42559a5c8341b66a0520805337526 SHA256 04d1ab1cfefe453224dee89d4351fd45a9553acc8f242e87f8fdad6e8af5320c
-EBUILD coq-8.0-r1.ebuild 2065 RMD160 3a8f789e1b2aa5685bf91ea8275adbc5d9399cdc SHA1 6af7eede753cdcf30c39975b0b6bde09fcac5705 SHA256 ca17fb5bbf9e36fb3880307a6f0df9b6a90c985d6d47d7830f9f6a891cb34b17
-MD5 32ab0325f73670990840fd4d5cbb87e6 coq-8.0-r1.ebuild 2065
-RMD160 3a8f789e1b2aa5685bf91ea8275adbc5d9399cdc coq-8.0-r1.ebuild 2065
-SHA256 ca17fb5bbf9e36fb3880307a6f0df9b6a90c985d6d47d7830f9f6a891cb34b17 coq-8.0-r1.ebuild 2065
EBUILD coq-8.0_p3.ebuild 2047 RMD160 e5a3917835844b9c45a3f17e6b242ac44e627112 SHA1 e7e01fa88f0a04c662ca3a7eff494985b4970daa SHA256 fa555a38d6b2f7716b2485cdcd9600b987251fa0ba13f3a06f46fe76d9228927
MD5 048ee6aefee27e33a7c61c076ec38154 coq-8.0_p3.ebuild 2047
RMD160 e5a3917835844b9c45a3f17e6b242ac44e627112 coq-8.0_p3.ebuild 2047
@@ -40,17 +22,14 @@ EBUILD coq-8.1_p2.ebuild 1707 RMD160 ce08d9a05e6bf60aae1f32501015bc0e4e42246d SH
MD5 352d4eeb9b8d3cc44e038527b3b8ffa4 coq-8.1_p2.ebuild 1707
RMD160 ce08d9a05e6bf60aae1f32501015bc0e4e42246d coq-8.1_p2.ebuild 1707
SHA256 8eab7d69053318aef442a967885e78dcfa30b2c41656462bd9cc68876043196b coq-8.1_p2.ebuild 1707
-MISC ChangeLog 4041 RMD160 fe822198d1f65f3b4b5943adf47cf2c808f0d2e0 SHA1 361e1564b83670f8f9b30514a460b6df7d24b18c SHA256 4cec909aaca1a060e8a4679853487927f23483995935e989aea178e8c0902fbc
-MD5 00ec172a6a3bf79283b817e00a8d0f9a ChangeLog 4041
-RMD160 fe822198d1f65f3b4b5943adf47cf2c808f0d2e0 ChangeLog 4041
-SHA256 4cec909aaca1a060e8a4679853487927f23483995935e989aea178e8c0902fbc ChangeLog 4041
+MISC ChangeLog 4232 RMD160 d848c56628f0ba77e7813ce8783cf65de96d1265 SHA1 f15023afa02e6f5e59b18244c5ae744a66a72722 SHA256 cdd834db29cbcff1596b5983516d8fcf2df3c5d6620156c6d441f077d9e154d6
+MD5 0885d8aa30d6cf496615e04afec01fa0 ChangeLog 4232
+RMD160 d848c56628f0ba77e7813ce8783cf65de96d1265 ChangeLog 4232
+SHA256 cdd834db29cbcff1596b5983516d8fcf2df3c5d6620156c6d441f077d9e154d6 ChangeLog 4232
MISC metadata.xml 174 RMD160 b6d9f7a487e305c44a47ffaa8d982731b5825a19 SHA1 70e63d5e68a5449b129f8f91f2554e8406e212a0 SHA256 3c931940a18c0692dd36b609c3026ce41dcde08cdc9e2d0d7bc0a0cf774e8c5b
MD5 587dfb99f9b1ef3ef6a79733b24811cc metadata.xml 174
RMD160 b6d9f7a487e305c44a47ffaa8d982731b5825a19 metadata.xml 174
SHA256 3c931940a18c0692dd36b609c3026ce41dcde08cdc9e2d0d7bc0a0cf774e8c5b metadata.xml 174
-MD5 aeca137009e9122f025cfd23b307d7a8 files/digest-coq-8.0-r1 500
-RMD160 8f45c953b095d4e8dad0409e798485eed9ead256 files/digest-coq-8.0-r1 500
-SHA256 a3b19476c72b3a27e40f09715030ceb8a0ec7ab781257b8542e9cba0f8c7cb3a files/digest-coq-8.0-r1 500
MD5 07d28c72f4d0913e374c8acba9a363b8 files/digest-coq-8.0_p3 765
RMD160 0eb02a90f6cb1bd9b1174cf2fc2e724a4f50cee9 files/digest-coq-8.0_p3 765
SHA256 d1900263704dc613417b872026abf1bde19771a25ebd7c0a09e7c82ee1201ec6 files/digest-coq-8.0_p3 765
@@ -63,7 +42,7 @@ SHA256 6e90b572e62f580834a9721149404b02faf2cac779670386219b778dfd7492e3 files/di
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.7 (GNU/Linux)
-iD8DBQFHGiDJvFcC4BYPU0oRAuLBAJ9uJZzaEZA1J3t6BrtzNoZB/2HKPQCgwGLh
-8hEdMVmBerEPTn/CdxerRZg=
-=n1xL
+iD8DBQFHGiQfvFcC4BYPU0oRApqpAKCbssH95HAsorB3/f851xbmHGyBEQCfVv+b
+dHGPmX6Eg5o2yuFXIPdUq+k=
+=AFac
-----END PGP SIGNATURE-----
diff --git a/sci-mathematics/coq/coq-8.0-r1.ebuild b/sci-mathematics/coq/coq-8.0-r1.ebuild
deleted file mode 100644
index 2f70a919e20b..000000000000
--- a/sci-mathematics/coq/coq-8.0-r1.ebuild
+++ /dev/null
@@ -1,88 +0,0 @@
-# Copyright 1999-2007 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.6 2007/07/02 15:26:46 peper Exp $
-
-inherit eutils
-
-IUSE="norealanalysis ide debug translator doc"
-
-RESTRICT="strip"
-
-MY_PV="8.0pl1"
-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
-translator? ( ftp://ftp.inria.fr/INRIA/coq/V${MY_PV}/${MY_P}-translator.tar.gz )"
-
-LICENSE="LGPL-2.1"
-SLOT="0"
-KEYWORDS="~amd64 ppc sparc x86"
-
-DEPEND=">=dev-lang/ocaml-3.06
-ide? ( >=dev-ml/lablgtk-2.2.0 )"
-
-S="${WORKDIR}/${MY_P/_/}"
-
-src_unpack()
-{
- unpack ${A}
- cd ${S}
- version=`ocamlc -v | grep 3.08.1`
- if [ $? -eq 0 ]
- then
- epatch ${FILESDIR}/${P}-ocaml-3.08.1.patch
- fi
- epatch ${FILESDIR}/${P}-byteflags.patch
-}
-
-src_compile() {
- local myconf="--prefix /usr \
- --bindir /usr/bin \
- --libdir /usr/lib/coq \
- --mandir /usr/man \
- --emacslib /usr/share/emacs/site-lisp \
- --coqdocdir /usr/lib/coq/coqdoc"
-
- use debug && myconf="--debug $myconf"
- use norealanalysis && myconf="$myconf --reals"
- use norealanalysis || myconf="$myconf --reals all"
-
- if use ide; then
- myconf="$myconf --coqide opt"
- else
- myconf="$myconf --coqide no"
- fi
-
- ./configure $myconf || die
-
- if use ide; then
- labldir=/usr/lib/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
- make world || die
- else
- make world
- fi
-}
-
-src_install() {
- make COQINSTALLPREFIX=${D} install || die
- dodoc README CREDITS CHANGES LICENSE
-
- if use translator; then
- cd ${WORKDIR}/${MY_P}-translator
- mv translate-v8 coq-translate-v8
- dobin coq-translate-v8
- if use doc; then
- dodoc Translator.* syntax-v8.*
- fi
- fi
-
- if use ide; then
- insinto /usr/share/applnk/Edutainment/Mathematics
- doins ${FILESDIR}/coqide.desktop
- fi
-}
diff --git a/sci-mathematics/coq/files/coq-8.0-byteflags.patch b/sci-mathematics/coq/files/coq-8.0-byteflags.patch
deleted file mode 100644
index 7b4acf017689..000000000000
--- a/sci-mathematics/coq/files/coq-8.0-byteflags.patch
+++ /dev/null
@@ -1,20 +0,0 @@
---- Makefile.orig 2004-06-19 23:53:43.231742696 +0200
-+++ Makefile 2004-06-19 23:54:39.977116088 +0200
-@@ -346,7 +346,7 @@
-
- $(COQTOPBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO)
- $(SHOW)'COQMKTOP -o $@'
-- $(HIDE)$(COQMKTOP) -top $(LOCALINCLUDES) $(CAMLDEBUG) -o $@
-+ $(HIDE)$(COQMKTOP) -top $(BYTEFLAGS) -o $@
-
- $(COQTOP):
- cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE)
-@@ -570,7 +570,7 @@
-
- $(COQIDEBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO) ide/ide.cma
- $(SHOW)'COQMKTOP -o $@'
-- $(HIDE)$(COQMKTOP) -g -ide -top $(LOCALINCLUDES) $(CAMLDEBUG) -o $@
-+ $(HIDE)$(COQMKTOP) -g -ide -top $(BYTEFLAGS) -o $@
-
- $(COQIDE):
- cd bin; ln -sf coqide.$(HASCOQIDE)$(EXE) coqide$(EXE)
diff --git a/sci-mathematics/coq/files/coq-8.0-ocaml-3.08.1.patch b/sci-mathematics/coq/files/coq-8.0-ocaml-3.08.1.patch
deleted file mode 100644
index 39f57e16521e..000000000000
--- a/sci-mathematics/coq/files/coq-8.0-ocaml-3.08.1.patch
+++ /dev/null
@@ -1,29 +0,0 @@
---- contrib/funind/tacinv.ml4.orig 2004-02-10 17:22:14.000000000 +0100
-+++ contrib/funind/tacinv.ml4 2004-08-20 13:29:59.000000000 +0200
-@@ -495,7 +495,7 @@
- let metav = mknewmeta() in
- let substmeta t = popn 1 (substitterm 0 (mkRel 1) metav t) in
- let newrec_call = substmeta rec_call in
-- let newlevar = List.map (fun ev,tev -> ev, substmeta tev) levar in
-+ let newlevar = List.map (fun (ev,tev) -> ev, substmeta tev) levar in
- let newabsc = Array.map substmeta absc in
- newrec_call,newlevar,lposeq,evararr,newabsc,((metav,nme, typ)::parms)
-
-@@ -693,7 +693,7 @@
- (* Generalize the goal. [[x1:T1][x2:T2]... g[arg1 <- x1 ...]]. *)
- let gl_abstr' = add_lambdas (pf_concl gl) gl listargs' in
- (* apply parameters immediately *)
-- let gl_abstr = applistc gl_abstr' (List.map (fun x,y,z -> x) (List.rev parms)) in
-+ let gl_abstr = applistc gl_abstr' (List.map (fun (x,y,z) -> x) (List.rev parms)) in
-
- (* we apply args of the fix now, the parameters will be applied later *)
- let princ_proof_applied_args =
-@@ -790,7 +790,7 @@
- in
- let rec princ_replace_params params t =
- List.fold_left (
-- fun acc ev,nam,typ ->
-+ fun acc (ev,nam,typ) ->
- mkLambda (Name (id_of_name nam) , typ,
- substitterm 0 ev (mkRel 1) (lift 0 acc)))
- t (List.rev params) in
diff --git a/sci-mathematics/coq/files/digest-coq-8.0-r1 b/sci-mathematics/coq/files/digest-coq-8.0-r1
deleted file mode 100644
index ce6925235d8c..000000000000
--- a/sci-mathematics/coq/files/digest-coq-8.0-r1
+++ /dev/null
@@ -1,6 +0,0 @@
-MD5 58a3c3c6e3903b0267857d283047c7e3 coq-8.0pl1-translator.tar.gz 233233
-RMD160 dc241dcd596e5c667a4e8295eb44f23cbfef432e coq-8.0pl1-translator.tar.gz 233233
-SHA256 baea2c89f52c06062b3c38d3cd9367206dcbb7728a0315d1d2ce49524f4aa340 coq-8.0pl1-translator.tar.gz 233233
-MD5 95237e64081d7306fdea49e1988bde12 coq-8.0pl1.tar.gz 2272613
-RMD160 e8437bc84e130757ae4bc46b832a95c0ea655da3 coq-8.0pl1.tar.gz 2272613
-SHA256 e90955b200b1bd64093eeebbad173d1228ea9d88aea0615a28de08782024be33 coq-8.0pl1.tar.gz 2272613
diff --git a/sci-mathematics/coq/files/ocaml-3.07.patch b/sci-mathematics/coq/files/ocaml-3.07.patch
deleted file mode 100644
index 707c51039b8a..000000000000
--- a/sci-mathematics/coq/files/ocaml-3.07.patch
+++ /dev/null
@@ -1,10 +0,0 @@
---- /root/tmp/coq-7.4/parsing/pcoq.ml4 2002-12-15 13:10:18.000000000 +0100
-+++ parsing/pcoq.ml4 2003-10-16 13:00:15.000000000 +0200
-@@ -108,6 +108,7 @@
- type parsable = G.parsable
- let parsable = G.parsable
- let tokens = G.tokens
-+ let glexer = G.glexer
- module Entry = G.Entry
- module Unsafe = G.Unsafe
-