summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMatthieu Sozeau <mattam@gentoo.org>2004-07-01 14:48:09 +0000
committerMatthieu Sozeau <mattam@gentoo.org>2004-07-01 14:48:09 +0000
commite7f984b201736aefa8c450705996aa626e7364bb (patch)
treeece2c119a4bb8325199c12d76234a2a776e633fc /app-sci/coq
parentCoq 8.0 use flags (diff)
downloadgentoo-2-e7f984b201736aefa8c450705996aa626e7364bb.tar.gz
gentoo-2-e7f984b201736aefa8c450705996aa626e7364bb.tar.bz2
gentoo-2-e7f984b201736aefa8c450705996aa626e7364bb.zip
New stable release.
Diffstat (limited to 'app-sci/coq')
-rw-r--r--app-sci/coq/ChangeLog11
-rw-r--r--app-sci/coq/Manifest12
-rw-r--r--app-sci/coq/coq-8.0.ebuild80
-rw-r--r--app-sci/coq/files/coq-8.0-byteflags.patch20
-rw-r--r--app-sci/coq/files/coqide.desktop10
-rw-r--r--app-sci/coq/files/digest-coq-8.02
6 files changed, 129 insertions, 6 deletions
diff --git a/app-sci/coq/ChangeLog b/app-sci/coq/ChangeLog
index 98fa395f3099..74f60f753db7 100644
--- a/app-sci/coq/ChangeLog
+++ b/app-sci/coq/ChangeLog
@@ -1,6 +1,13 @@
# 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.3 2004/06/24 21:56:14 agriffis Exp $
+# Copyright 2000-2004 Gentoo Technologies, Inc.; Distributed under the GPL v2
+# $Header: /var/cvsroot/gentoo-x86/app-sci/coq/ChangeLog,v 1.4 2004/07/01 14:48:09 mattam Exp $
+
+*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)
diff --git a/app-sci/coq/Manifest b/app-sci/coq/Manifest
index 861875b468b1..d16b386b344a 100644
--- a/app-sci/coq/Manifest
+++ b/app-sci/coq/Manifest
@@ -1,7 +1,11 @@
-MD5 f7362fd7ee6b7239ea9b2fc4119e7ce6 coq-8.0_beta.ebuild 957
-MD5 fd0597cc1580b05e07e89f66bdf3fd9d coq-7.4.ebuild 947
-MD5 0da4d9bb10c228d312018ce92e8c6452 ChangeLog 695
+MD5 d472faf45bae28669ad7b67e3540b455 ChangeLog 996
+MD5 b95dd6d75d060fa55af740d04647a3bd coq-7.4.ebuild 953
+MD5 030312fc00cd1d79004bffebd3df7941 coq-8.0_beta.ebuild 963
MD5 5af6b26df9264817e5b6a292c1436417 metadata.xml 238
-MD5 73c401b2052bccdc88677bf5be2d453f files/digest-coq-8.0_beta 64
+MD5 75c55de9b0530a6f71cae69f9bb1a61f coq-8.0.ebuild 1901
+MD5 e5491c930f8f944ed9c3590fdc8492c1 files/coqide.desktop 242
MD5 d3f33f3602d82ea691f91b062dbf236b files/digest-coq-7.4 60
+MD5 73c401b2052bccdc88677bf5be2d453f files/digest-coq-8.0_beta 64
MD5 393c3085f82f205122b4e66c94232ff7 files/ocaml-3.07.patch 333
+MD5 5d46723c29afcd1e24e529e5993c3096 files/coq-8.0-byteflags.patch 676
+MD5 86922705a72292e7508baae5bc75e2a3 files/digest-coq-8.0 130
diff --git a/app-sci/coq/coq-8.0.ebuild b/app-sci/coq/coq-8.0.ebuild
new file mode 100644
index 000000000000..2203f5f3dad6
--- /dev/null
+++ b/app-sci/coq/coq-8.0.ebuild
@@ -0,0 +1,80 @@
+# Copyright 1999-2004 Gentoo Technologies, Inc.
+# 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.1 2004/07/01 14:48:09 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
+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
new file mode 100644
index 000000000000..7b4acf017689
--- /dev/null
+++ b/app-sci/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/app-sci/coq/files/coqide.desktop b/app-sci/coq/files/coqide.desktop
new file mode 100644
index 000000000000..08b5b6918cd0
--- /dev/null
+++ b/app-sci/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/app-sci/coq/files/digest-coq-8.0 b/app-sci/coq/files/digest-coq-8.0
new file mode 100644
index 000000000000..c339254dca9e
--- /dev/null
+++ b/app-sci/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