ports/73634: [UPDATE] math/coq -- add support for CoqIde

Rene Ladan r.c.ladan at student.tue.nl
Sun Nov 7 01:40:28 UTC 2004 

>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 at 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 at 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 <bsd.port.pre.mk>
+
+.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 <bsd.port.mk>
+.include <bsd.port.post.mk>
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 <r.c.ladan at student.tue.nl>
 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 @@
- at 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
+ at 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
+ at dirrm lib/coq/contrib/field
 lib/coq/contrib/fourier/Fourier.vo
 lib/coq/contrib/fourier/Fourier_util.vo
+ at dirrm lib/coq/contrib/fourier
 lib/coq/contrib/interface/vernacrc
+ at dirrm lib/coq/contrib/interface
 lib/coq/contrib/omega/Omega.vo
 lib/coq/contrib/omega/OmegaLemmas.vo
+ at 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
+ at dirrm lib/coq/contrib/ring
 lib/coq/contrib/romega/ROmega.vo
 lib/coq/contrib/romega/ReflOmegaCore.vo
+ at dirrm lib/coq/contrib/romega
+ at dirrm lib/coq/contrib
 lib/coq/contrib7/cc/CCSolve.vo
+ at 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
+ at dirrm lib/coq/contrib7/field
 lib/coq/contrib7/fourier/Fourier.vo
 lib/coq/contrib7/fourier/Fourier_util.vo
+ at dirrm lib/coq/contrib7/fourier
 lib/coq/contrib7/omega/Omega.vo
 lib/coq/contrib7/omega/OmegaLemmas.vo
+ at 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
+ at dirrm lib/coq/contrib7/ring
 lib/coq/contrib7/romega/ROmega.vo
 lib/coq/contrib7/romega/ReflOmegaCore.vo
+ at dirrm lib/coq/contrib7/romega
+ at 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
+ at dirrm lib/coq/ide
 lib/coq/states/initial.coq
+ at dirrm lib/coq/states
 lib/coq/states7/barestate.coq
 lib/coq/states7/initial.coq
+ at 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
+ at 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
+ at 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
+ at 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
+ at 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
+ at 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
+ at 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
+ at 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
+ at 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
+ at dirrm lib/coq/theories/Relations
 lib/coq/theories/Setoids/Setoid.vo
+ at 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
+ at dirrm lib/coq/theories/Sets
 lib/coq/theories/Sorting/Heap.vo
 lib/coq/theories/Sorting/Permutation.vo
 lib/coq/theories/Sorting/Sorting.vo
+ at 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
+ at 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
+ at dirrm lib/coq/theories/ZArith
+ at 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
+ at 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
+ at 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
+ at 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
+ at 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
+ at 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
+ at 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
+ at 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
+ at 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
+ at dirrm lib/coq/theories7/Relations
 lib/coq/theories7/Setoids/Setoid.vo
+ at 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
+ at dirrm lib/coq/theories7/Sets
 lib/coq/theories7/Sorting/Heap.vo
 lib/coq/theories7/Sorting/Permutation.vo
 lib/coq/theories7/Sorting/Sorting.vo
+ at 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
+ at 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
+ at dirrm lib/coq/theories7/ZArith
+ at dirrm lib/coq/theories7
+ at 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%%
- at dirrm lib/coq/contrib/cc
- at dirrm lib/coq/contrib/field
- at dirrm lib/coq/contrib/fourier
- at dirrm lib/coq/contrib/interface
- at dirrm lib/coq/contrib/omega
- at dirrm lib/coq/contrib/ring
- at dirrm lib/coq/contrib/romega
- at dirrm lib/coq/contrib
- at dirrm lib/coq/contrib7/cc
- at dirrm lib/coq/contrib7/field
- at dirrm lib/coq/contrib7/fourier
- at dirrm lib/coq/contrib7/omega
- at dirrm lib/coq/contrib7/ring
- at dirrm lib/coq/contrib7/romega
- at dirrm lib/coq/contrib7
- at dirrm lib/coq/ide
- at dirrm lib/coq/states
- at dirrm lib/coq/states7
- at dirrm lib/coq/theories/Arith
- at dirrm lib/coq/theories/Bool
- at dirrm lib/coq/theories/Init
- at dirrm lib/coq/theories/IntMap
- at dirrm lib/coq/theories/Lists
- at dirrm lib/coq/theories/Logic
- at dirrm lib/coq/theories/NArith
- at dirrm lib/coq/theories/Reals
- at dirrm lib/coq/theories/Relations
- at dirrm lib/coq/theories/Setoids
- at dirrm lib/coq/theories/Sets
- at dirrm lib/coq/theories/Sorting
- at dirrm lib/coq/theories/Wellfounded
- at dirrm lib/coq/theories/ZArith
- at dirrm lib/coq/theories
- at dirrm lib/coq/theories7/Arith
- at dirrm lib/coq/theories7/Bool
- at dirrm lib/coq/theories7/Init
- at dirrm lib/coq/theories7/IntMap
- at dirrm lib/coq/theories7/Lists
- at dirrm lib/coq/theories7/Logic
- at dirrm lib/coq/theories7/NArith
- at dirrm lib/coq/theories7/Reals
- at dirrm lib/coq/theories7/Relations
- at dirrm lib/coq/theories7/Setoids
- at dirrm lib/coq/theories7/Sets
- at dirrm lib/coq/theories7/Sorting
- at dirrm lib/coq/theories7/Wellfounded
- at dirrm lib/coq/theories7/ZArith
- at dirrm lib/coq/theories7
- at dirrm lib/coq

>Release-Note:
>Audit-Trail:
>Unformatted:

More information about the freebsd-ports-bugs mailing list