update to version 8.4

OK
jasper@, sthen@, Yozo Toda (maintainer)

math/coq/Makefile

@@ -1,68 +1,63 @@
-# $OpenBSD: Makefile,v 1.17 2012/11/30 19:38:09 chrisz Exp $
-
-BROKEN=			requires update due to ocaml 3.08
+# $OpenBSD: Makefile,v 1.18 2013/01/04 11:07:28 chrisz Exp $
 
 COMMENT=		proof assistant based on a typed lambda calculus
 
-DISTNAME=		coq-7.3.1
-REVISION=		1
+DISTNAME=		coq-8.4
 CATEGORIES=		math
 HOMEPAGE=		http://coq.inria.fr/
 
 MAINTAINER=		Yozo Toda <yozo@v007.vaio.ne.jp>
 
+# LGPL 2.1
 PERMIT_PACKAGE_CDROM=	Yes
 PERMIT_PACKAGE_FTP=	Yes
 PERMIT_DISTFILES_CDROM=	Yes
 PERMIT_DISTFILES_FTP=	Yes
-WANTLIB=		c curses m pthread
 
-MASTER_SITES=		ftp://ftp.inria.fr/INRIA/coq/V7.3.1/
-MASTER_SITES0=		${MASTER_SITES:S@$@doc/@}
-MASTER_SITES1=		http://coq.inria.fr/
-MASTER_SITES2=		http://coq.inria.fr/ps/
-MASTER_SITES3=		ftp://quatramaran.ens.fr/pub/espie/coq/
-DISTFILES=		${DISTNAME}.tar.gz \
-			doc-html-20040711.tar.gz:3 \
-			Changes.html:0 \
-			Reference-Manual-all.ps.gz:0 \
-			library.tar.gz:1 \
-			RecTutorial.v.ps:2
-PATCHFILES=		patch-coq-7.3.1-ocaml-3.07
+WANTLIB += GL X11 Xcomposite Xcursor Xdamage Xext Xfixes Xi Xinerama
+WANTLIB += Xrandr Xrender atk-1.0 c cairo expat fontconfig freetype
+WANTLIB += gdk-x11-2.0 gdk_pixbuf-2.0 gio-2.0 glib-2.0 gobject-2.0
+WANTLIB += gtk-x11-2.0 iconv intl m pango-1.0 pangocairo-1.0
+WANTLIB += pangoft2-1.0 pixman-1 png pthread pthread-stubs
+WANTLIB += xcb xcb-render xcb-shm z
 
-DIST_SUBDIR=		coq
-EXTRACT_ONLY=		${DISTNAME}.tar.gz \
-			doc-html-20040711.tar.gz \
-			library.tar.gz  \
+MASTER_SITES=	http://pauillac.inria.fr/~herbelin/coq/distrib/V8.4/files/
 
-DESTDIRNAME=		COQINSTALLPREFIX
+RUN_DEPENDS=	x11/lablgtk2
+BUILD_DEPENDS=	${RUN_DEPENDS}
 
-USE_GMAKE=		Yes
-USE_GROFF =		Yes
+DESTDIRNAME=	COQINSTALLPREFIX
 
-MODULES=		lang/ocaml
+USE_GMAKE=	Yes
+USE_GROFF=	Yes
 
-CONFIGURE_STYLE=	simple
-CONFIGURE_ARGS=		-prefix ${PREFIX} \
-			-emacslib ${PREFIX}/share/emacs/site-lisp \
-			${MODOCAML_NATIVE:S/Yes/-opt/:S/No/-byteonly/}
+MODULES=	lang/ocaml
+
+CONFIGURE_STYLE= simple
+CONFIGURE_ARGS=	-emacslib ${PREFIX}/share/emacs/site-lisp \
+		-makecmd ${GMAKE} \
+		-prefix ${PREFIX} \
+		-mandir ${PREFIX}/man \
+		-configdir ${SYSCONFDIR}/xdg/coq \
+		-usecamlp4 \
+
+.include <bsd.port.arch.mk>
+.if ${PROPERTIES:Mocaml_native_dynlink}
+CONFIGURE_ARGS+=	-opt
+.else
+CONFIGURE_ARGS+=	-byteonly
+.endif
 
 ALL_TARGET=		world
+# Order is important!
+INSTALL_TARGET=		install-byte install-ide-byte install
 REGRESS_TARGET=		check
 
-COQ_DOCHTMLFILES=       Changes.html
-COQ_DOCPSFILES=         RecTutorial.v.ps Reference-Manual-all.ps.gz
-
 post-install:
-	@${INSTALL_DATA_DIR} ${PREFIX}/share/doc/coq/html/library
-	@${INSTALL_DATA} ${WRKDIR}/coq-docs-html/* ${PREFIX}/share/doc/coq/html
-	@${INSTALL_DATA} ${WRKDIR}/library/* ${PREFIX}/share/doc/coq/html/library
-	@for ff in ${COQ_DOCHTMLFILES} ; do \
-	  ${INSTALL_DATA} ${FULLDISTDIR}/$${ff} ${PREFIX}/share/doc/coq/html ; \
-	done
-	@${INSTALL_DATA_DIR} ${PREFIX}/share/doc/coq/ps
-	@for ff in ${COQ_DOCPSFILES} ; do \
-	  ${INSTALL_DATA} ${FULLDISTDIR}/$${ff} ${PREFIX}/share/doc/coq/ps ; \
-	done
+	cd ${WRKDIST}; ${INSTALL_DATA} LICENSE COPYRIGHT CREDITS CHANGES \
+	    COMPATIBILITY ${PREFIX}/share/doc/coq/
+	${INSTALL_DATA_DIR} ${PREFIX}/share/examples/coq/
+	mv ${WRKINST}${SYSCONFDIR}/xdg/coq/* ${PREFIX}/share/examples/coq/
+	rmdir ${WRKINST}${SYSCONFDIR}/xdg/coq/ ${WRKINST}${SYSCONFDIR}/xdg/
 
 .include <bsd.port.mk>

math/coq/distinfo

@@ -1,35 +1,2 @@
-MD5 (coq/Changes.html) = +miJ2r3Id+Pc9VXOFTjODQ==
-MD5 (coq/RecTutorial.v.ps) = sOP2j6Mm5kysVp+bDaCYoQ==
-MD5 (coq/Reference-Manual-all.ps.gz) = 65ec0L22aVbp4apWWEHGwg==
-MD5 (coq/coq-7.3.1.tar.gz) = u0A0YLtR3oBgW3nfoE/oBw==
-MD5 (coq/doc-html-20040711.tar.gz) = CcNnA8oVupm/f0+0OAIkyQ==
-MD5 (coq/library.tar.gz) = 30TtwBeMZD4Pf55fi0rLRA==
-MD5 (coq/patch-coq-7.3.1-ocaml-3.07) = HXQeVH55aQ8acK3b8OEB0g==
-RMD160 (coq/Changes.html) = jQ3R6ZV2c+++OhY4+NdibYQMx5I=
-RMD160 (coq/RecTutorial.v.ps) = vMiWe/zy3w5LNnGikYGJ7Wi9oiU=
-RMD160 (coq/Reference-Manual-all.ps.gz) = /Nq/vpHUoBpbQqfQKBfnR1n3AuY=
-RMD160 (coq/coq-7.3.1.tar.gz) = oQSjeOJ/5gWr4wJQjxKULpRgzC8=
-RMD160 (coq/doc-html-20040711.tar.gz) = RzcaXBfpQmZwexjdSS9H1OThzf4=
-RMD160 (coq/library.tar.gz) = 8emthVwnuxpQRYZ9+bobVlU0cO0=
-RMD160 (coq/patch-coq-7.3.1-ocaml-3.07) = Omtp2dsQgz5yJMpc4buIAgAxz48=
-SHA1 (coq/Changes.html) = /j44sSpsrhQd4nxG6eHLFpmckPo=
-SHA1 (coq/RecTutorial.v.ps) = GPTQIqoAZbqzUG+aeeYm1qjKz9Q=
-SHA1 (coq/Reference-Manual-all.ps.gz) = F72cufugFXjep8Avwr7AdoChLHw=
-SHA1 (coq/coq-7.3.1.tar.gz) = hWJ+WuMfgKn3sd/Y0lc7/U6+KHE=
-SHA1 (coq/doc-html-20040711.tar.gz) = hMbkQhZD0IPQr5lydvH0vB+egnc=
-SHA1 (coq/library.tar.gz) = jcvFlrvNsxhswk9ZmcQ4ciJuykw=
-SHA1 (coq/patch-coq-7.3.1-ocaml-3.07) = ABGEvcbzn8Xt/yvw87J0VKIbheE=
-SHA256 (coq/Changes.html) = WMrFojl8y2nw3COeqwrKhhvDql7Rl3lVtmVzSbMAQu0=
-SHA256 (coq/RecTutorial.v.ps) = FQw8jMRBArgODWNMQ7l/F6Ptxz3zYTaJ8itDxuOb5Fc=
-SHA256 (coq/Reference-Manual-all.ps.gz) = l6f/3ktcgqa9LNvmGgwqpFdP2H4DJJwpP1VGmTWrhFM=
-SHA256 (coq/coq-7.3.1.tar.gz) = 8krB1GN8qdQ8L2/Jar/RePyUGVLfHTkWAqNnhPrsCPU=
-SHA256 (coq/doc-html-20040711.tar.gz) = mG7IaXjlc9p7SRkA/J8kNkSzBWHN3wnxxlP50ErJNhw=
-SHA256 (coq/library.tar.gz) = Z0pmWw8mEIjWkXvg4Q4Txh32NQz8GpocmPpmcpcsaWE=
-SHA256 (coq/patch-coq-7.3.1-ocaml-3.07) = /u/Ey4rbIjhu7rJIUEBFM7VxVPYZGmta4blzcSxn1f8=
-SIZE (coq/Changes.html) = 5018
-SIZE (coq/RecTutorial.v.ps) = 562794
-SIZE (coq/Reference-Manual-all.ps.gz) = 375587
-SIZE (coq/coq-7.3.1.tar.gz) = 1233035
-SIZE (coq/doc-html-20040711.tar.gz) = 254431
-SIZE (coq/library.tar.gz) = 441013
-SIZE (coq/patch-coq-7.3.1-ocaml-3.07) = 8950
+SHA256 (coq-8.4.tar.gz) = 9GrltvC+qdwpnebzwCDudcQFgeMqGDLpopDQmKaiQk0=
+SIZE (coq-8.4.tar.gz) = 4134779

math/coq/patches/patch-Makefile_build

@@ -0,0 +1,12 @@
+$OpenBSD: patch-Makefile_build,v 1.1 2013/01/04 11:07:29 chrisz Exp $
+--- Makefile.build.orig	Fri Dec 21 18:46:20 2012
++++ Makefile.build	Fri Dec 21 18:47:10 2012
+@@ -603,7 +603,7 @@ install-binaries:: install-$(BEST)  install-tools
+ 
+ install-byte::
+ 	$(MKDIR) $(FULLBINDIR)
+-	$(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(CHICKEN) $(FULLBINDIR)
++	$(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(CHICKEN) $(CHICKENBYTE) $(FULLBINDIR)
+ 	cd $(FULLBINDIR); ln -sf coqtop.byte$(EXE) coqtop$(EXE); ln -sf coqchk.byte$(EXE) coqchk$(EXE)
+ 
+ install-opt::

math/coq/patches/patch-configure

@@ -1,11 +1,12 @@
---- configure.orig	Thu Oct  3 14:46:22 2002
-+++ configure	Mon Nov  4 13:12:09 2002
-@@ -402,7 +402,7 @@ PRINTF=`which printf`
- 
- # Subdirectories of theories/ added in coq_config.ml
- subdirs () {
--    (cd $1; find . -type d ! -name CVS ! -regex ".*extraction/test.*" ! -name .  -exec $PRINTF "\"%s\";\n" {} \; >> $mlconfig_file)
-+    (cd $1; find . -type d ! -name CVS ! -path "*extraction/test*" ! -name .  -exec $PRINTF "\"%s\";\n" {} \; >> $mlconfig_file)
- }
- 
- echo "let theories_dirs = [" >> $mlconfig_file
+$OpenBSD: patch-configure,v 1.2 2013/01/04 11:07:29 chrisz Exp $
+--- configure.orig	Sun Aug 12 00:03:19 2012
++++ configure	Sat Aug 18 06:42:21 2012
+@@ -879,7 +879,7 @@ case $coqrunbyteflags_spec/$local/$custom_spec/$CUSTOM
+     */true/*/*) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$COQTOP'/kernel/byterun";;
+     *)
+         COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$LIBDIR'"
+-        BUILDLDPATH="export CAML_LD_LIBRARY_PATH='$COQTOP'/kernel/byterun";;
++        BUILDLDPATH="export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun";;
+ esac
+ case $coqtoolsbyteflags_spec/$custom_spec/$CUSTOM_OS in
+     yes/*/*) COQTOOLSBYTEFLAGS="$coqtoolsbyteflags";;

math/coq/patches/patch-ide_preferences_ml

@@ -0,0 +1,14 @@
+$OpenBSD: patch-ide_preferences_ml,v 1.1 2013/01/04 11:07:29 chrisz Exp $
+--- ide/preferences.ml.orig	Mon Oct 15 21:45:06 2012
++++ ide/preferences.ml	Mon Oct 15 21:46:19 2012
+@@ -35,6 +35,10 @@ let mod_to_str (m:Gdk.Tags.modifier) =
+     | `MOD5 -> "<Mod5>"
+     | `CONTROL -> "<Control>"
+     | `SHIFT -> "<Shift>"
++    | `HYPER -> "<Hyper>"
++    | `META -> "<Meta>"
++    | `SUPER -> "<Super>"
++    | `RELEASE
+     |  `BUTTON1| `BUTTON2| `BUTTON3| `BUTTON4| `BUTTON5| `LOCK -> ""
+ 
+ let mod_list_to_str l = List.fold_left (fun s m -> (mod_to_str m)^s) "" l

math/coq/patches/patch-ide_utils_okey_ml

@@ -0,0 +1,73 @@
+$OpenBSD: patch-ide_utils_okey_ml,v 1.1 2013/01/04 11:07:29 chrisz Exp $
+--- ide/utils/okey.ml.orig	Mon Oct 15 21:03:31 2012
++++ ide/utils/okey.ml	Mon Oct 15 21:41:25 2012
+@@ -30,23 +30,29 @@ type handler = {
+     cback : (unit -> unit) ;
+   }
+ 
+-type handler_spec = int * int * Gdk.keysym
++type handler_spec = int32 * int32 * Gdk.keysym
+       (** mods * mask * key *)
+ 
+-let int_of_modifier = function
+-    `SHIFT -> 1
+-  | `LOCK -> 2
+-  | `CONTROL -> 4
+-  | `MOD1 -> 8
+-  | `MOD2 -> 16
+-  | `MOD3 -> 32
+-  | `MOD4 -> 64
+-  | `MOD5 -> 128
+-  | `BUTTON1 -> 256
+-  | `BUTTON2 -> 512
+-  | `BUTTON3 -> 1024
+-  | `BUTTON4 -> 2048
+-  | `BUTTON5 -> 4096
++let int_of_modifier =
++  let power2 = Int32.shift_left 1l in
++  function
++    `SHIFT -> power2 0
++  | `LOCK -> power2 1
++  | `CONTROL -> power2 2
++  | `MOD1 -> power2 3
++  | `MOD2 -> power2 4
++  | `MOD3 -> power2 5
++  | `MOD4 -> power2 6
++  | `MOD5 -> power2 7
++  | `BUTTON1 -> power2 8
++  | `BUTTON2 -> power2 9
++  | `BUTTON3 -> power2 10
++  | `BUTTON4 -> power2 11
++  | `BUTTON5 -> power2 12
++  | `SUPER -> power2 26
++  | `HYPER -> power2 27
++  | `META -> power2 28
++  | `RELEASE -> power2 30
+ 
+ let print_modifier l =
+   List.iter
+@@ -72,13 +78,13 @@ let print_modifier l =
+   print_newline ()
+ 
+ let int_of_modifiers l =
+-  List.fold_left (fun acc -> fun m -> acc + (int_of_modifier m)) 0 l
++  List.fold_left (fun acc -> fun m -> Int32.add acc (int_of_modifier m)) 0l l
+ 
+ module H =
+   struct
+     type t = handler_spec * handler
+     let equal (m,k) (mods, mask, key) =
+-      (k = key) && ((m land mask) = mods)
++      (k = key) && (( Int32.logand m mask) = mods)
+ 
+     let filter_with_mask mods mask key l =
+       List.filter (fun a -> (fst a) <> (mods, mask, key)) l
+@@ -149,7 +155,7 @@ let add1 ?(remove=false) w
+       r
+   in
+   let n_mods = int_of_modifiers mods in
+-  let n_mask = lnot (int_of_modifiers mask) in
++  let n_mask = Int32.lognot (int_of_modifiers mask) in
+   let new_h = { cond = cond ; cback = callback } in
+   if remove then
+     (

math/coq/patches/patch-test-suite-Makefile

@@ -0,0 +1,19 @@
+--- test-suite/Makefile.orig	Tue Jan 17 17:10:51 2012
++++ test-suite/Makefile	Mon Oct 15 19:39:15 2012
+@@ -46,6 +46,7 @@ SHOW := $(if $(VERBOSE),@true,@echo)
+ HIDE := $(if $(VERBOSE),,@)
+ REDIR := $(if $(VERBOSE),,> /dev/null 2>&1)
+ 
++bogomips :=
+ ifneq (,$(wildcard /proc/cpuinfo))
+   sedbogo := -e "s/bogomips.*: \([0-9]*\).*/\1/p" # i386, ppc
+   sedbogo += -e "s/Cpu0Bogo.*: \([0-9]*\).*/\1/p" # sparc
+@@ -112,7 +113,7 @@ $(foreach S,$(VSUBSYSTEMS),$(eval $(call mkstamp,$(S))
+ # Summary
+ #######################################################################
+ 
+-summary_dir = echo $(1); find $(2) -name '*.log' -print0 | xargs -0 -n 1 tail -n1 | sort -g
++summary_dir = echo $(1); find $(2) -name '*.log' -print0 | xargs -0 -n 1 tail -n1 | sort -n
+ 
+ .PHONY: summary summary.log
+ 

math/coq/pkg/DESCR

@@ -1,2 +1,3 @@
-The Coq Proof Assistant is designed to write formal specifications, programs
-and to verify that programs are correct with respect to their specification.
+Coq is a formal proof management system. It provides a formal language to write
+mathematical definitions, executable algorithms and theorems together with an
+environment for semi-interactive development of machine-checked proofs.

math/coq/pkg/PFRAG.dynlink-native

@@ -0,0 +1,54 @@
+@comment $OpenBSD: PFRAG.dynlink-native,v 1.1 2013/01/04 11:07:29 chrisz Exp $
+@bin bin/coqchk.opt
+@bin bin/coqide.opt
+@bin bin/coqtop.opt
+lib/coq/config/coq_config.cmx
+lib/coq/config/coq_config.o
+lib/coq/ide/ide.a
+lib/coq/ide/ide.cmxa
+lib/coq/interp/interp.a
+lib/coq/interp/interp.cmxa
+lib/coq/kernel/kernel.a
+lib/coq/kernel/kernel.cmxa
+lib/coq/lib/lib.a
+lib/coq/lib/lib.cmxa
+lib/coq/libcoqrun.a
+lib/coq/library/library.a
+lib/coq/library/library.cmxa
+lib/coq/parsing/highparsing.a
+lib/coq/parsing/highparsing.cmxa
+lib/coq/parsing/parsing.a
+lib/coq/parsing/parsing.cmxa
+lib/coq/plugins/cc/cc_plugin.cmxs
+lib/coq/plugins/decl_mode/decl_mode_plugin.cmxs
+lib/coq/plugins/extraction/extraction_plugin.cmxs
+lib/coq/plugins/field/field_plugin.cmxs
+lib/coq/plugins/firstorder/ground_plugin.cmxs
+lib/coq/plugins/fourier/fourier_plugin.cmxs
+lib/coq/plugins/funind/recdef_plugin.cmxs
+lib/coq/plugins/micromega/micromega_plugin.cmxs
+lib/coq/plugins/nsatz/nsatz_plugin.cmxs
+lib/coq/plugins/omega/omega_plugin.cmxs
+lib/coq/plugins/quote/quote_plugin.cmxs
+lib/coq/plugins/ring/ring_plugin.cmxs
+lib/coq/plugins/romega/romega_plugin.cmxs
+lib/coq/plugins/rtauto/rtauto_plugin.cmxs
+lib/coq/plugins/setoid_ring/newring_plugin.cmxs
+lib/coq/plugins/subtac/subtac_plugin.cmxs
+lib/coq/plugins/syntax/ascii_syntax_plugin.cmxs
+lib/coq/plugins/syntax/nat_syntax_plugin.cmxs
+lib/coq/plugins/syntax/numbers_syntax_plugin.cmxs
+lib/coq/plugins/syntax/r_syntax_plugin.cmxs
+lib/coq/plugins/syntax/string_syntax_plugin.cmxs
+lib/coq/plugins/syntax/z_syntax_plugin.cmxs
+lib/coq/plugins/xml/xml_plugin.cmxs
+lib/coq/pretyping/pretyping.a
+lib/coq/pretyping/pretyping.cmxa
+lib/coq/proofs/proofs.a
+lib/coq/proofs/proofs.cmxa
+lib/coq/tactics/hightactics.a
+lib/coq/tactics/hightactics.cmxa
+lib/coq/tactics/tactics.a
+lib/coq/tactics/tactics.cmxa
+lib/coq/toplevel/toplevel.a
+lib/coq/toplevel/toplevel.cmxa

math/coq/pkg/PFRAG.native

@@ -1,2 +1,2 @@
-@comment $OpenBSD: PFRAG.native,v 1.1 2002/12/18 09:41:07 sturm Exp $
-bin/coqtop.opt
+@comment $OpenBSD: PFRAG.native,v 1.2 2013/01/04 11:07:29 chrisz Exp $
+%%dynlink%%

math/coq/pkg/PFRAG.shared

@@ -0,0 +1,2 @@
+@comment $OpenBSD: PFRAG.shared,v 1.1 2013/01/04 11:07:29 chrisz Exp $
+lib/coq/dllcoqrun.so