diff options
author | Alexis Ballier <aballier@gentoo.org> | 2007-10-20 15:51:44 +0000 |
---|---|---|
committer | Alexis Ballier <aballier@gentoo.org> | 2007-10-20 15:51:44 +0000 |
commit | 5c5530dff9cceb47f17bb94a768f70e570ad71ae (patch) | |
tree | 65c9b6cc23271f393b55ebc2cf98c716ee67cbfc /sci-mathematics/coq | |
parent | Backport the speex changes from #193768 to 1.0.14. (diff) | |
download | historical-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/ChangeLog | 7 | ||||
-rw-r--r-- | sci-mathematics/coq/Manifest | 35 | ||||
-rw-r--r-- | sci-mathematics/coq/coq-8.0-r1.ebuild | 88 | ||||
-rw-r--r-- | sci-mathematics/coq/files/coq-8.0-byteflags.patch | 20 | ||||
-rw-r--r-- | sci-mathematics/coq/files/coq-8.0-ocaml-3.08.1.patch | 29 | ||||
-rw-r--r-- | sci-mathematics/coq/files/digest-coq-8.0-r1 | 6 | ||||
-rw-r--r-- | sci-mathematics/coq/files/ocaml-3.07.patch | 10 |
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 - |