+++ /dev/null
-# 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.
-
+++ /dev/null
-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
+++ /dev/null
-# 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
-}
+++ /dev/null
-# 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
-}
+++ /dev/null
-# 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
-}
+++ /dev/null
---- 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)
+++ /dev/null
---- 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
+++ /dev/null
-[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;
+++ /dev/null
-MD5 13ac61f150823e54ad84a9096e2dd646 coq-7.4.tar.gz 1537547
+++ /dev/null
-MD5 75ab1eb131b3469d21ab74377826b32b coq-8.0.tar.gz 2281827
-MD5 e2e4ecc8a552c847a656dcf9e47dd738 coq-8.0-translator.tar.gz 233218
+++ /dev/null
-MD5 95237e64081d7306fdea49e1988bde12 coq-8.0pl1.tar.gz 2272613
-MD5 58a3c3c6e3903b0267857d283047c7e3 coq-8.0pl1-translator.tar.gz 233233
+++ /dev/null
---- /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
-
+++ /dev/null
-<?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>
projects / gentoo.git / commitdiff