From owner-freebsd-ports-bugs@FreeBSD.ORG Sun Nov 7 01:40:27 2004 Return-Path: Delivered-To: freebsd-ports-bugs@hub.freebsd.org Received: from mx1.FreeBSD.org (mx1.freebsd.org [216.136.204.125]) by hub.freebsd.org (Postfix) with ESMTP id A27DE16A4CF for ; Sun, 7 Nov 2004 01:40:27 +0000 (GMT) Received: from freefall.freebsd.org (freefall.freebsd.org [216.136.204.21]) by mx1.FreeBSD.org (Postfix) with ESMTP id 491AF43D4C for ; Sun, 7 Nov 2004 01:40:27 +0000 (GMT) (envelope-from gnats@FreeBSD.org) Received: from freefall.freebsd.org (gnats@localhost [127.0.0.1]) iA71eRke092365 for ; Sun, 7 Nov 2004 01:40:27 GMT (envelope-from gnats@freefall.freebsd.org) Received: (from gnats@localhost) by freefall.freebsd.org (8.12.11/8.12.11/Submit) id iA71eR2b092364; Sun, 7 Nov 2004 01:40:27 GMT (envelope-from gnats) Resent-Date: Sun, 7 Nov 2004 01:40:27 GMT Resent-Message-Id: <200411070140.iA71eR2b092364@freefall.freebsd.org> Resent-From: FreeBSD-gnats-submit@FreeBSD.org (GNATS Filer) Resent-To: freebsd-ports-bugs@FreeBSD.org Resent-Reply-To: FreeBSD-gnats-submit@FreeBSD.org, Rene Ladan Received: from mx1.FreeBSD.org (mx1.freebsd.org [216.136.204.125]) by hub.freebsd.org (Postfix) with ESMTP id EAF6C16A4D1 for ; Sun, 7 Nov 2004 01:37:18 +0000 (GMT) Received: from 82-168-140-74-bbxl.xdsl.tiscali.nl (82-168-140-74-bbxl.xdsl.tiscali.nl [82.168.140.74]) by mx1.FreeBSD.org (Postfix) with ESMTP id 0801243D45 for ; Sun, 7 Nov 2004 01:37:17 +0000 (GMT) (envelope-from r.c.ladan@student.tue.nl) Received: from 82-168-140-74-bbxl.xdsl.tiscali.nl (localhost [127.0.0.1]) iA71c7xN076138 for ; Sun, 7 Nov 2004 02:38:08 +0100 (CET) (envelope-from r.c.ladan@student.tue.nl) Received: (from rene@localhost)iA71c7vB076137; Sun, 7 Nov 2004 02:38:07 +0100 (CET) (envelope-from r.c.ladan@student.tue.nl) Message-Id: <200411070138.iA71c7vB076137@82-168-140-74-bbxl.xdsl.tiscali.nl> Date: Sun, 7 Nov 2004 02:38:07 +0100 (CET) From: Rene Ladan To: FreeBSD-gnats-submit@FreeBSD.org X-Send-Pr-Version: 3.113 Subject: ports/73634: [UPDATE] math/coq -- add support for CoqIde X-BeenThere: freebsd-ports-bugs@freebsd.org X-Mailman-Version: 2.1.1 Precedence: list Reply-To: Rene Ladan List-Id: Ports bug reports List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sun, 07 Nov 2004 01:40:28 -0000 >Number: 73634 >Category: ports >Synopsis: [UPDATE] math/coq -- add support for CoqIde >Confidential: no >Severity: non-critical >Priority: low >Responsible: freebsd-ports-bugs >State: open >Quarter: >Keywords: >Date-Required: >Class: maintainer-update >Submitter-Id: current-users >Arrival-Date: Sun Nov 07 01:40:27 GMT 2004 >Closed-Date: >Last-Modified: >Originator: Rene Ladan >Release: FreeBSD 5.3-STABLE i386 >Organization: >Environment: System: FreeBSD 82-168-140-74-bbxl.xdsl.tiscali.nl 5.3-STABLE FreeBSD 5.3-STABLE #3: Wed Nov 3 19:15:37 CET 2004 root@82-168-140-74-bbxl.xdsl.tiscali.nl:/usr/obj/usr/src/sys/RENE i386 >Description: * Add support for CoqIde * Bump PORTVERSION to 8.0p1 to indicate that the distribution is at version 8.0pl1 and not 8.0 * Move @dirrm tags right after directory contents instead of at end of pkg-plist * Sort MAN1 section in Makefile >How-To-Repeat: >Fix: diff -ruN --exclude=CVS /usr/ports/math/coq.orig/Makefile /usr/ports/math/coq/Makefile --- /usr/ports/math/coq.orig/Makefile Sun Nov 7 02:28:31 2004 +++ /usr/ports/math/coq/Makefile Sun Nov 7 01:52:00 2004 @@ -6,13 +6,13 @@ # PORTNAME= coq -PORTVERSION= 8.0 +PORTVERSION= 8.0p1 CATEGORIES= math MASTER_SITES= ftp://ftp.inria.fr/INRIA/coq/V8.0pl1/ DISTNAME= coq-8.0pl1 PATCH_SITES= ${MASTER_SITES} -#Ports has Ocaml 3.08.1 : +#only for Ocaml 3.08.1 : PATCHFILES= patch-coq-8.0pl1-ocaml-3.08.1 MAINTAINER= r.c.ladan@student.tue.nl @@ -29,11 +29,20 @@ CONFIGURE_ARGS+= --opt ALL_TARGET= world -#no lablgl2 in ports yet -MAN1= coq-interface.1 coq-tex.1 coq_makefile.1 coqc.1 coqdep.1 \ - coqdoc.1 coqmktop.1 coqtop.1 coqtop.byte.1 coqtop.opt.1 \ - coqwc.1 parser.1 gallina.1 +.include + +.if exists(${LOCALBASE}/bin/lablgtk2) +BUILD_DEPENDS+= lablgtk2:${PORTSDIR}/x11-toolkits/ocaml-lablgtk2 +RUN_DEPENDS+= ${BUILD_DEPENDS} +PLIST_SUB+= IDE="" +.else +PLIST_SUB+= IDE="@comment " +.endif + +MAN1= coq-interface.1 coq-tex.1 coq_makefile.1 coqc.1 coqdep.1 coqdoc.1 \ + coqmktop.1 coqtop.1 coqtop.byte.1 coqtop.opt.1 coqwc.1 gallina.1 \ + parser.1 post-install: .if !defined(NOPORTDOCS) @@ -43,4 +52,4 @@ .endfor .endif -.include +.include diff -ruN --exclude=CVS /usr/ports/math/coq.orig/pkg-descr /usr/ports/math/coq/pkg-descr --- /usr/ports/math/coq.orig/pkg-descr Sun Nov 7 00:31:38 2004 +++ /usr/ports/math/coq/pkg-descr Sun Nov 7 02:11:18 2004 @@ -17,7 +17,7 @@ Coq is distributed under the GNU Lesser General Public Licence Version 2.1 (LGPL). -CoqIde is not yet available in this port. +CoqIde is installed if the x11-toolkits/ocaml-lablgtk2 port is installed. Author: Rene Ladan WWW: http://coq.inria.fr/ diff -ruN --exclude=CVS /usr/ports/math/coq.orig/pkg-plist /usr/ports/math/coq/pkg-plist --- /usr/ports/math/coq.orig/pkg-plist Sun Nov 7 00:31:38 2004 +++ /usr/ports/math/coq/pkg-plist Sun Nov 7 02:10:12 2004 @@ -1,4 +1,3 @@ -@comment $FreeBSD: ports/math/coq/pkg-plist,v 1.1 2004/10/16 00:55:32 pav Exp $ bin/coq-interface bin/coq-interface.opt bin/coq-tex @@ -6,6 +5,9 @@ bin/coqc bin/coqdep bin/coqdoc +%%IDE%%bin/coqide +%%IDE%%bin/coqide.byte +%%IDE%%bin/coqide.opt bin/coqmktop bin/coqtop bin/coqtop.byte @@ -15,15 +17,20 @@ bin/parser bin/parser.opt lib/coq/contrib/cc/CCSolve.vo +@dirrm lib/coq/contrib/cc lib/coq/contrib/field/Field.vo lib/coq/contrib/field/Field_Compl.vo lib/coq/contrib/field/Field_Tactic.vo lib/coq/contrib/field/Field_Theory.vo +@dirrm lib/coq/contrib/field lib/coq/contrib/fourier/Fourier.vo lib/coq/contrib/fourier/Fourier_util.vo +@dirrm lib/coq/contrib/fourier lib/coq/contrib/interface/vernacrc +@dirrm lib/coq/contrib/interface lib/coq/contrib/omega/Omega.vo lib/coq/contrib/omega/OmegaLemmas.vo +@dirrm lib/coq/contrib/omega lib/coq/contrib/ring/ArithRing.vo lib/coq/contrib/ring/NArithRing.vo lib/coq/contrib/ring/Quote.vo @@ -35,17 +42,24 @@ lib/coq/contrib/ring/Setoid_ring_normalize.vo lib/coq/contrib/ring/Setoid_ring_theory.vo lib/coq/contrib/ring/ZArithRing.vo +@dirrm lib/coq/contrib/ring lib/coq/contrib/romega/ROmega.vo lib/coq/contrib/romega/ReflOmegaCore.vo +@dirrm lib/coq/contrib/romega +@dirrm lib/coq/contrib lib/coq/contrib7/cc/CCSolve.vo +@dirrm lib/coq/contrib7/cc lib/coq/contrib7/field/Field.vo lib/coq/contrib7/field/Field_Compl.vo lib/coq/contrib7/field/Field_Tactic.vo lib/coq/contrib7/field/Field_Theory.vo +@dirrm lib/coq/contrib7/field lib/coq/contrib7/fourier/Fourier.vo lib/coq/contrib7/fourier/Fourier_util.vo +@dirrm lib/coq/contrib7/fourier lib/coq/contrib7/omega/Omega.vo lib/coq/contrib7/omega/OmegaLemmas.vo +@dirrm lib/coq/contrib7/omega lib/coq/contrib7/ring/ArithRing.vo lib/coq/contrib7/ring/NArithRing.vo lib/coq/contrib7/ring/Quote.vo @@ -57,16 +71,22 @@ lib/coq/contrib7/ring/Setoid_ring_normalize.vo lib/coq/contrib7/ring/Setoid_ring_theory.vo lib/coq/contrib7/ring/ZArithRing.vo +@dirrm lib/coq/contrib7/ring lib/coq/contrib7/romega/ROmega.vo lib/coq/contrib7/romega/ReflOmegaCore.vo +@dirrm lib/coq/contrib7/romega +@dirrm lib/coq/contrib7 lib/coq/ide/.coqide-gtk2rc lib/coq/ide/FAQ lib/coq/ide/coq.png lib/coq/ide/utf8.v lib/coq/ide/utf8.vo +@dirrm lib/coq/ide lib/coq/states/initial.coq +@dirrm lib/coq/states lib/coq/states7/barestate.coq lib/coq/states7/initial.coq +@dirrm lib/coq/states7 lib/coq/theories/Arith/Arith.vo lib/coq/theories/Arith/Between.vo lib/coq/theories/Arith/Bool_nat.vo @@ -87,6 +107,7 @@ lib/coq/theories/Arith/Peano_dec.vo lib/coq/theories/Arith/Plus.vo lib/coq/theories/Arith/Wf_nat.vo +@dirrm lib/coq/theories/Arith lib/coq/theories/Bool/Bool.vo lib/coq/theories/Bool/BoolEq.vo lib/coq/theories/Bool/Bvector.vo @@ -94,6 +115,7 @@ lib/coq/theories/Bool/IfProp.vo lib/coq/theories/Bool/Sumbool.vo lib/coq/theories/Bool/Zerob.vo +@dirrm lib/coq/theories/Bool lib/coq/theories/Init/Datatypes.vo lib/coq/theories/Init/Logic.vo lib/coq/theories/Init/Logic_Type.vo @@ -102,6 +124,7 @@ lib/coq/theories/Init/Prelude.vo lib/coq/theories/Init/Specif.vo lib/coq/theories/Init/Wf.vo +@dirrm lib/coq/theories/Init lib/coq/theories/IntMap/Adalloc.vo lib/coq/theories/IntMap/Addec.vo lib/coq/theories/IntMap/Addr.vo @@ -118,11 +141,13 @@ lib/coq/theories/IntMap/Mapiter.vo lib/coq/theories/IntMap/Maplists.vo lib/coq/theories/IntMap/Mapsubset.vo +@dirrm lib/coq/theories/IntMap lib/coq/theories/Lists/List.vo lib/coq/theories/Lists/ListSet.vo lib/coq/theories/Lists/MonoList.vo lib/coq/theories/Lists/Streams.vo lib/coq/theories/Lists/TheoryList.vo +@dirrm lib/coq/theories/Lists lib/coq/theories/Logic/Berardi.vo lib/coq/theories/Logic/ChoiceFacts.vo lib/coq/theories/Logic/Classical.vo @@ -141,10 +166,12 @@ lib/coq/theories/Logic/JMeq.vo lib/coq/theories/Logic/ProofIrrelevance.vo lib/coq/theories/Logic/RelationalChoice.vo +@dirrm lib/coq/theories/Logic lib/coq/theories/NArith/BinNat.vo lib/coq/theories/NArith/BinPos.vo lib/coq/theories/NArith/NArith.vo lib/coq/theories/NArith/Pnat.vo +@dirrm lib/coq/theories/NArith lib/coq/theories/Reals/Alembert.vo lib/coq/theories/Reals/AltSeries.vo lib/coq/theories/Reals/ArithProp.vo @@ -198,13 +225,16 @@ lib/coq/theories/Reals/SplitAbsolu.vo lib/coq/theories/Reals/SplitRmult.vo lib/coq/theories/Reals/Sqrt_reg.vo +@dirrm lib/coq/theories/Reals lib/coq/theories/Relations/Newman.vo lib/coq/theories/Relations/Operators_Properties.vo lib/coq/theories/Relations/Relation_Definitions.vo lib/coq/theories/Relations/Relation_Operators.vo lib/coq/theories/Relations/Relations.vo lib/coq/theories/Relations/Rstar.vo +@dirrm lib/coq/theories/Relations lib/coq/theories/Setoids/Setoid.vo +@dirrm lib/coq/theories/Setoids lib/coq/theories/Sets/Classical_sets.vo lib/coq/theories/Sets/Constructive_sets.vo lib/coq/theories/Sets/Cpo.vo @@ -227,9 +257,11 @@ lib/coq/theories/Sets/Relations_3.vo lib/coq/theories/Sets/Relations_3_facts.vo lib/coq/theories/Sets/Uniset.vo +@dirrm lib/coq/theories/Sets lib/coq/theories/Sorting/Heap.vo lib/coq/theories/Sorting/Permutation.vo lib/coq/theories/Sorting/Sorting.vo +@dirrm lib/coq/theories/Sorting lib/coq/theories/Wellfounded/Disjoint_Union.vo lib/coq/theories/Wellfounded/Inclusion.vo lib/coq/theories/Wellfounded/Inverse_Image.vo @@ -239,6 +271,7 @@ lib/coq/theories/Wellfounded/Union.vo lib/coq/theories/Wellfounded/Well_Ordering.vo lib/coq/theories/Wellfounded/Wellfounded.vo +@dirrm lib/coq/theories/Wellfounded lib/coq/theories/ZArith/BinInt.vo lib/coq/theories/ZArith/Wf_Z.vo lib/coq/theories/ZArith/ZArith.vo @@ -262,6 +295,8 @@ lib/coq/theories/ZArith/Zsqrt.vo lib/coq/theories/ZArith/Zwf.vo lib/coq/theories/ZArith/auxiliary.vo +@dirrm lib/coq/theories/ZArith +@dirrm lib/coq/theories lib/coq/theories7/Arith/Arith.vo lib/coq/theories7/Arith/Between.vo lib/coq/theories7/Arith/Bool_nat.vo @@ -282,6 +317,7 @@ lib/coq/theories7/Arith/Peano_dec.vo lib/coq/theories7/Arith/Plus.vo lib/coq/theories7/Arith/Wf_nat.vo +@dirrm lib/coq/theories7/Arith lib/coq/theories7/Bool/Bool.vo lib/coq/theories7/Bool/BoolEq.vo lib/coq/theories7/Bool/Bvector.vo @@ -289,6 +325,7 @@ lib/coq/theories7/Bool/IfProp.vo lib/coq/theories7/Bool/Sumbool.vo lib/coq/theories7/Bool/Zerob.vo +@dirrm lib/coq/theories7/Bool lib/coq/theories7/Init/Datatypes.vo lib/coq/theories7/Init/Logic.vo lib/coq/theories7/Init/Logic_Type.vo @@ -297,6 +334,7 @@ lib/coq/theories7/Init/Prelude.vo lib/coq/theories7/Init/Specif.vo lib/coq/theories7/Init/Wf.vo +@dirrm lib/coq/theories7/Init lib/coq/theories7/IntMap/Adalloc.vo lib/coq/theories7/IntMap/Addec.vo lib/coq/theories7/IntMap/Addr.vo @@ -313,6 +351,7 @@ lib/coq/theories7/IntMap/Mapiter.vo lib/coq/theories7/IntMap/Maplists.vo lib/coq/theories7/IntMap/Mapsubset.vo +@dirrm lib/coq/theories7/IntMap lib/coq/theories7/Lists/List.vo lib/coq/theories7/Lists/ListSet.vo lib/coq/theories7/Lists/MonoList.vo @@ -320,6 +359,7 @@ lib/coq/theories7/Lists/PolyListSyntax.vo lib/coq/theories7/Lists/Streams.vo lib/coq/theories7/Lists/TheoryList.vo +@dirrm lib/coq/theories7/Lists lib/coq/theories7/Logic/Berardi.vo lib/coq/theories7/Logic/ChoiceFacts.vo lib/coq/theories7/Logic/Classical.vo @@ -338,10 +378,12 @@ lib/coq/theories7/Logic/JMeq.vo lib/coq/theories7/Logic/ProofIrrelevance.vo lib/coq/theories7/Logic/RelationalChoice.vo +@dirrm lib/coq/theories7/Logic lib/coq/theories7/NArith/BinNat.vo lib/coq/theories7/NArith/BinPos.vo lib/coq/theories7/NArith/NArith.vo lib/coq/theories7/NArith/Pnat.vo +@dirrm lib/coq/theories7/NArith lib/coq/theories7/Reals/Alembert.vo lib/coq/theories7/Reals/AltSeries.vo lib/coq/theories7/Reals/ArithProp.vo @@ -396,13 +438,16 @@ lib/coq/theories7/Reals/SplitAbsolu.vo lib/coq/theories7/Reals/SplitRmult.vo lib/coq/theories7/Reals/Sqrt_reg.vo +@dirrm lib/coq/theories7/Reals lib/coq/theories7/Relations/Newman.vo lib/coq/theories7/Relations/Operators_Properties.vo lib/coq/theories7/Relations/Relation_Definitions.vo lib/coq/theories7/Relations/Relation_Operators.vo lib/coq/theories7/Relations/Relations.vo lib/coq/theories7/Relations/Rstar.vo +@dirrm lib/coq/theories7/Relations lib/coq/theories7/Setoids/Setoid.vo +@dirrm lib/coq/theories7/Setoids lib/coq/theories7/Sets/Classical_sets.vo lib/coq/theories7/Sets/Constructive_sets.vo lib/coq/theories7/Sets/Cpo.vo @@ -425,9 +470,11 @@ lib/coq/theories7/Sets/Relations_3.vo lib/coq/theories7/Sets/Relations_3_facts.vo lib/coq/theories7/Sets/Uniset.vo +@dirrm lib/coq/theories7/Sets lib/coq/theories7/Sorting/Heap.vo lib/coq/theories7/Sorting/Permutation.vo lib/coq/theories7/Sorting/Sorting.vo +@dirrm lib/coq/theories7/Sorting lib/coq/theories7/Wellfounded/Disjoint_Union.vo lib/coq/theories7/Wellfounded/Inclusion.vo lib/coq/theories7/Wellfounded/Inverse_Image.vo @@ -437,6 +484,7 @@ lib/coq/theories7/Wellfounded/Union.vo lib/coq/theories7/Wellfounded/Well_Ordering.vo lib/coq/theories7/Wellfounded/Wellfounded.vo +@dirrm lib/coq/theories7/Wellfounded lib/coq/theories7/ZArith/BinInt.vo lib/coq/theories7/ZArith/Wf_Z.vo lib/coq/theories7/ZArith/ZArith.vo @@ -463,6 +511,9 @@ lib/coq/theories7/ZArith/auxiliary.vo lib/coq/theories7/ZArith/fast_integer.vo lib/coq/theories7/ZArith/zarith_aux.vo +@dirrm lib/coq/theories7/ZArith +@dirrm lib/coq/theories7 +@dirrm lib/coq share/emacs/site-lisp/coq-inferior.el share/emacs/site-lisp/coq.el share/texmf/tex/latex/misc/coqdoc.sty @@ -473,52 +524,3 @@ %%PORTDOCS%%%%DOCSDIR%%/LICENSE %%PORTDOCS%%%%DOCSDIR%%/README %%PORTDOCS%%@dirrm %%DOCSDIR%% -@dirrm lib/coq/contrib/cc -@dirrm lib/coq/contrib/field -@dirrm lib/coq/contrib/fourier -@dirrm lib/coq/contrib/interface -@dirrm lib/coq/contrib/omega -@dirrm lib/coq/contrib/ring -@dirrm lib/coq/contrib/romega -@dirrm lib/coq/contrib -@dirrm lib/coq/contrib7/cc -@dirrm lib/coq/contrib7/field -@dirrm lib/coq/contrib7/fourier -@dirrm lib/coq/contrib7/omega -@dirrm lib/coq/contrib7/ring -@dirrm lib/coq/contrib7/romega -@dirrm lib/coq/contrib7 -@dirrm lib/coq/ide -@dirrm lib/coq/states -@dirrm lib/coq/states7 -@dirrm lib/coq/theories/Arith -@dirrm lib/coq/theories/Bool -@dirrm lib/coq/theories/Init -@dirrm lib/coq/theories/IntMap -@dirrm lib/coq/theories/Lists -@dirrm lib/coq/theories/Logic -@dirrm lib/coq/theories/NArith -@dirrm lib/coq/theories/Reals -@dirrm lib/coq/theories/Relations -@dirrm lib/coq/theories/Setoids -@dirrm lib/coq/theories/Sets -@dirrm lib/coq/theories/Sorting -@dirrm lib/coq/theories/Wellfounded -@dirrm lib/coq/theories/ZArith -@dirrm lib/coq/theories -@dirrm lib/coq/theories7/Arith -@dirrm lib/coq/theories7/Bool -@dirrm lib/coq/theories7/Init -@dirrm lib/coq/theories7/IntMap -@dirrm lib/coq/theories7/Lists -@dirrm lib/coq/theories7/Logic -@dirrm lib/coq/theories7/NArith -@dirrm lib/coq/theories7/Reals -@dirrm lib/coq/theories7/Relations -@dirrm lib/coq/theories7/Setoids -@dirrm lib/coq/theories7/Sets -@dirrm lib/coq/theories7/Sorting -@dirrm lib/coq/theories7/Wellfounded -@dirrm lib/coq/theories7/ZArith -@dirrm lib/coq/theories7 -@dirrm lib/coq >Release-Note: >Audit-Trail: >Unformatted: