Moved from app-sci/coq to sci-mathematics/coq.

13 files changed, 353 insertions, 0 deletions

diff --git a/sci-mathematics/coq/ChangeLog b/sci-mathematics/coq/ChangeLog
new file mode 100644
index 000000000000..595cc2abfa78
--- /dev/null
+++ b/sci-mathematics/coq/ChangeLog
@@ -0,0 +1,49 @@
+# ChangeLog for app-sci/coq
+# Copyright 2000-2004 Gentoo Foundation; Distributed under the GPL v2
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/ChangeLog,v 1.1 2004/12/28 05:03:02 ribosome Exp $
+
+*coq-8.0-r1 (28 Dec 2004)
+
+  28 Dec 2004; Olivier Fisette <ribosome@gentoo.org> +metadata.xml,
+  +files/coq-8.0-byteflags.patch, +files/coq-8.0-ocaml-3.08.1.patch,
+  +files/coqide.desktop, +files/ocaml-3.07.patch, +coq-7.4.ebuild,
+  +coq-8.0-r1.ebuild, +coq-8.0.ebuild:
+  Moved from app-sci/coq to sci-mathematics/coq.
+
+  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/sci-mathematics/coq/Manifest b/sci-mathematics/coq/Manifest
new file mode 100644
index 000000000000..0d8a82e0cdcc
--- /dev/null
+++ b/sci-mathematics/coq/Manifest
@@ -0,0 +1,12 @@
+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/sci-mathematics/coq/coq-7.4.ebuild b/sci-mathematics/coq/coq-7.4.ebuild
new file mode 100644
index 000000000000..1c168e0cbd55
--- /dev/null
+++ b/sci-mathematics/coq/coq-7.4.ebuild
@@ -0,0 +1,40 @@
+# Copyright 1999-2004 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.1 2004/12/28 05:03:02 ribosome 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
new file mode 100644
index 000000000000..27f98d532cb5
--- /dev/null
+++ b/sci-mathematics/coq/coq-8.0-r1.ebuild
@@ -0,0 +1,88 @@
+# Copyright 1999-2004 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.1 2004/12/28 05:03:02 ribosome 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/sci-mathematics/coq/coq-8.0.ebuild b/sci-mathematics/coq/coq-8.0.ebuild
new file mode 100644
index 000000000000..24fbf597ff94
--- /dev/null
+++ b/sci-mathematics/coq/coq-8.0.ebuild
@@ -0,0 +1,81 @@
+# Copyright 1999-2004 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.1 2004/12/28 05:03:02 ribosome 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/sci-mathematics/coq/files/coq-8.0-byteflags.patch b/sci-mathematics/coq/files/coq-8.0-byteflags.patch
new file mode 100644
index 000000000000..7b4acf017689
--- /dev/null
+++ b/sci-mathematics/coq/files/coq-8.0-byteflags.patch
@@ -0,0 +1,20 @@
+--- 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
new file mode 100644
index 000000000000..39f57e16521e
--- /dev/null
+++ b/sci-mathematics/coq/files/coq-8.0-ocaml-3.08.1.patch
@@ -0,0 +1,29 @@
+--- 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/coqide.desktop b/sci-mathematics/coq/files/coqide.desktop
new file mode 100644
index 000000000000..08b5b6918cd0
--- /dev/null
+++ b/sci-mathematics/coq/files/coqide.desktop
@@ -0,0 +1,10 @@
+[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/sci-mathematics/coq/files/digest-coq-7.4 b/sci-mathematics/coq/files/digest-coq-7.4
new file mode 100644
index 000000000000..ab1d3353a4d9
--- /dev/null
+++ b/sci-mathematics/coq/files/digest-coq-7.4
@@ -0,0 +1 @@
+MD5 13ac61f150823e54ad84a9096e2dd646 coq-7.4.tar.gz 1537547
diff --git a/sci-mathematics/coq/files/digest-coq-8.0 b/sci-mathematics/coq/files/digest-coq-8.0
new file mode 100644
index 000000000000..c339254dca9e
--- /dev/null
+++ b/sci-mathematics/coq/files/digest-coq-8.0
@@ -0,0 +1,2 @@
+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-r1 b/sci-mathematics/coq/files/digest-coq-8.0-r1
new file mode 100644
index 000000000000..73335eb85772
--- /dev/null
+++ b/sci-mathematics/coq/files/digest-coq-8.0-r1
@@ -0,0 +1,2 @@
+MD5 95237e64081d7306fdea49e1988bde12 coq-8.0pl1.tar.gz 2272613
+MD5 58a3c3c6e3903b0267857d283047c7e3 coq-8.0pl1-translator.tar.gz 233233
diff --git a/sci-mathematics/coq/files/ocaml-3.07.patch b/sci-mathematics/coq/files/ocaml-3.07.patch
new file mode 100644
index 000000000000..707c51039b8a
--- /dev/null
+++ b/sci-mathematics/coq/files/ocaml-3.07.patch
@@ -0,0 +1,10 @@
+--- /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/sci-mathematics/coq/metadata.xml b/sci-mathematics/coq/metadata.xml
new file mode 100644
index 000000000000..75191cd37a28
--- /dev/null
+++ b/sci-mathematics/coq/metadata.xml
@@ -0,0 +1,9 @@
+<?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>