diff options
author | Olivier Fisette <ribosome@gentoo.org> | 2004-12-28 05:01:49 +0000 |
---|---|---|
committer | Olivier Fisette <ribosome@gentoo.org> | 2004-12-28 05:01:49 +0000 |
commit | 9b08555463d5cf43274db31e19660eced643c53c (patch) | |
tree | cb5653e6cbe1b9e5412967cbb45619a565e7a0d9 /app-sci | |
parent | Moved from app-sci/calc to sci-mathematics/calc (diff) | |
download | historical-9b08555463d5cf43274db31e19660eced643c53c.tar.gz historical-9b08555463d5cf43274db31e19660eced643c53c.tar.bz2 historical-9b08555463d5cf43274db31e19660eced643c53c.zip |
Moving to sci-mathematics/coq
Diffstat (limited to 'app-sci')
-rw-r--r-- | app-sci/coq/ChangeLog | 41 | ||||
-rw-r--r-- | app-sci/coq/Manifest | 12 | ||||
-rw-r--r-- | app-sci/coq/coq-7.4.ebuild | 40 | ||||
-rw-r--r-- | app-sci/coq/coq-8.0-r1.ebuild | 88 | ||||
-rw-r--r-- | app-sci/coq/coq-8.0.ebuild | 81 | ||||
-rw-r--r-- | app-sci/coq/files/coq-8.0-byteflags.patch | 20 | ||||
-rw-r--r-- | app-sci/coq/files/coq-8.0-ocaml-3.08.1.patch | 29 | ||||
-rw-r--r-- | app-sci/coq/files/coqide.desktop | 10 | ||||
-rw-r--r-- | app-sci/coq/files/digest-coq-7.4 | 1 | ||||
-rw-r--r-- | app-sci/coq/files/digest-coq-8.0 | 2 | ||||
-rw-r--r-- | app-sci/coq/files/digest-coq-8.0-r1 | 2 | ||||
-rw-r--r-- | app-sci/coq/files/ocaml-3.07.patch | 10 | ||||
-rw-r--r-- | app-sci/coq/metadata.xml | 9 |
13 files changed, 0 insertions, 345 deletions
diff --git a/app-sci/coq/ChangeLog b/app-sci/coq/ChangeLog deleted file mode 100644 index e751c48656b5..000000000000 --- a/app-sci/coq/ChangeLog +++ /dev/null @@ -1,41 +0,0 @@ -# ChangeLog for app-sci/coq -# Copyright 2000-2004 Gentoo Foundation; Distributed under the GPL v2 -# $Header: /var/cvsroot/gentoo-x86/app-sci/coq/ChangeLog,v 1.9 2004/11/18 22:52:52 mattam Exp $ - - 18 Nov 2004; Matthieu Sozeau <mattam@gentoo.org> - +files/coq-8.0-ocaml-3.08.1.patch, coq-8.0-r1.ebuild: - Add patch for ocaml-3.08.1. - - 13 Aug 2004; Jason Wever <weeve@gentoo.org> coq-8.0-r1.ebuild: - Added ~sparc keyword. - -*coq-8.0-r1 (08 Aug 2004) - - 08 Aug 2004; Matthieu Sozeau <mattam@gentoo.org> coq-7.4.ebuild, - +coq-8.0-r1.ebuild, coq-8.0.ebuild, -coq-8.0_beta.ebuild: - Prepare for 3.08 insertion, remove old beta ebuild and add the latest version. - - 13 Jul 2004; Travis Tilley <lv@gentoo.org> coq-7.4.ebuild: - adding ~amd64 keyword - -*coq-8.0 (01 Jul 2004) - - 01 Jul 2004; Matthieu Sozeau <mattam@gentoo.org> coq-8.0.ebuild, - files/coq-8.0-byteflags.patch, files/coqide.desktop: - Add new stable release of coq, which comes with an ide now, and a translation - script from older versions. Adding two local use flags for those. - -*coq-8.0_beta (02 Apr 2004) - - 02 Apr 2004; Matthieu Sozeau <mattam@gentoo.org> coq-7.4.ebuild, - coq-8.0_beta.ebuild: - Added coq-8.0_beta ebuild, tested on x86. Make coq-7.4 stable, - as there were no bug reports for some time now. - -*coq-7.4 (22 Jan 2004) - - 22 Jan 2004; Matthieu Sozeau <mattam@gentoo.org> coq-7.4.ebuild, - metadata.xml, files/ocaml-3.07.patch: - Initial commit. Related bugs are 30388 and 24616. norealanalysis use flag idea - taken from Peter Lietz <p.lietz@gmx.de> ebuild. - diff --git a/app-sci/coq/Manifest b/app-sci/coq/Manifest deleted file mode 100644 index 0d8a82e0cdcc..000000000000 --- a/app-sci/coq/Manifest +++ /dev/null @@ -1,12 +0,0 @@ -MD5 4b3e22466363130a7a799228534043a2 coq-8.0.ebuild 1910 -MD5 2559fb0ebf76645f855752a3a18fa7d2 coq-7.4.ebuild 975 -MD5 c919fa171c61513b8683d11944adc86b ChangeLog 1538 -MD5 5af6b26df9264817e5b6a292c1436417 metadata.xml 238 -MD5 da62f53c7b4fab39a73e5f847ac5cad5 coq-8.0-r1.ebuild 2056 -MD5 02ac210c6af5d8e258a2805a22822a8b files/coq-8.0-ocaml-3.08.1.patch 1321 -MD5 dc0f737371101bc7c97b0a80165ddac6 files/digest-coq-8.0-r1 136 -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 diff --git a/app-sci/coq/coq-7.4.ebuild b/app-sci/coq/coq-7.4.ebuild deleted file mode 100644 index b6f832034788..000000000000 --- a/app-sci/coq/coq-7.4.ebuild +++ /dev/null @@ -1,40 +0,0 @@ -# Copyright 1999-2004 Gentoo Foundation -# Distributed under the terms of the GNU General Public License v2 -# $Header: /var/cvsroot/gentoo-x86/app-sci/coq/coq-7.4.ebuild,v 1.6 2004/08/08 07:00:05 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/app-sci/coq/coq-8.0-r1.ebuild b/app-sci/coq/coq-8.0-r1.ebuild deleted file mode 100644 index ae03d88c7eb5..000000000000 --- a/app-sci/coq/coq-8.0-r1.ebuild +++ /dev/null @@ -1,88 +0,0 @@ -# Copyright 1999-2004 Gentoo Foundation -# Distributed under the terms of the GNU General Public License v2 -# $Header: /var/cvsroot/gentoo-x86/app-sci/coq/coq-8.0-r1.ebuild,v 1.3 2004/11/18 22:52:52 mattam Exp $ - -inherit eutils - -IUSE="norealanalysis ide debug translator doc" - -RESTRICT="nostrip" - -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="~x86 ~ppc ~sparc" - -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/app-sci/coq/coq-8.0.ebuild b/app-sci/coq/coq-8.0.ebuild deleted file mode 100644 index 9a5ec212a4ce..000000000000 --- a/app-sci/coq/coq-8.0.ebuild +++ /dev/null @@ -1,81 +0,0 @@ -# Copyright 1999-2004 Gentoo Foundation -# Distributed under the terms of the GNU General Public License v2 -# $Header: /var/cvsroot/gentoo-x86/app-sci/coq/coq-8.0.ebuild,v 1.3 2004/08/08 07:00:05 mattam Exp $ - -inherit eutils - -IUSE="norealanalysis ide debug translator doc" - -RESTRICT="nostrip" - -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 )" - -LICENSE="LGPL-2.1" -SLOT="0" -KEYWORDS="~x86 ~ppc" - -DEPEND=">=dev-lang/ocaml-3.06 -!>=dev-lang/ocaml-3.08 -ide? ( >=dev-ml/lablgtk-2.2.0 )" - -S="${WORKDIR}/${P/_/}" - -src_unpack() -{ - unpack ${A} - cd ${S} - 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}/coq-8.0-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/app-sci/coq/files/coq-8.0-byteflags.patch b/app-sci/coq/files/coq-8.0-byteflags.patch deleted file mode 100644 index 7b4acf017689..000000000000 --- a/app-sci/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/app-sci/coq/files/coq-8.0-ocaml-3.08.1.patch b/app-sci/coq/files/coq-8.0-ocaml-3.08.1.patch deleted file mode 100644 index 39f57e16521e..000000000000 --- a/app-sci/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/app-sci/coq/files/coqide.desktop b/app-sci/coq/files/coqide.desktop deleted file mode 100644 index 08b5b6918cd0..000000000000 --- a/app-sci/coq/files/coqide.desktop +++ /dev/null @@ -1,10 +0,0 @@ -[Desktop Entry] -Encoding=UTF-8 -Comment=Coq integrated developpment environment -Icon=/usr/lib/coq/ide/coq.png -Exec=/usr/bin/coqide -Name=CoqIDE -GenericName=Coq IDE -Terminal=false -Type=Application -Categories=Application;Edutainment;Mathematics; diff --git a/app-sci/coq/files/digest-coq-7.4 b/app-sci/coq/files/digest-coq-7.4 deleted file mode 100644 index ab1d3353a4d9..000000000000 --- a/app-sci/coq/files/digest-coq-7.4 +++ /dev/null @@ -1 +0,0 @@ -MD5 13ac61f150823e54ad84a9096e2dd646 coq-7.4.tar.gz 1537547 diff --git a/app-sci/coq/files/digest-coq-8.0 b/app-sci/coq/files/digest-coq-8.0 deleted file mode 100644 index c339254dca9e..000000000000 --- a/app-sci/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/app-sci/coq/files/digest-coq-8.0-r1 b/app-sci/coq/files/digest-coq-8.0-r1 deleted file mode 100644 index 73335eb85772..000000000000 --- a/app-sci/coq/files/digest-coq-8.0-r1 +++ /dev/null @@ -1,2 +0,0 @@ -MD5 95237e64081d7306fdea49e1988bde12 coq-8.0pl1.tar.gz 2272613 -MD5 58a3c3c6e3903b0267857d283047c7e3 coq-8.0pl1-translator.tar.gz 233233 diff --git a/app-sci/coq/files/ocaml-3.07.patch b/app-sci/coq/files/ocaml-3.07.patch deleted file mode 100644 index 707c51039b8a..000000000000 --- a/app-sci/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 - diff --git a/app-sci/coq/metadata.xml b/app-sci/coq/metadata.xml deleted file mode 100644 index 75191cd37a28..000000000000 --- a/app-sci/coq/metadata.xml +++ /dev/null @@ -1,9 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd"> -<pkgmetadata> - <herd>sci</herd> - <herd>ml</herd> - <maintainer> - <email>mattam@gentoo.org</email> - </maintainer> -</pkgmetadata> |