here is a patch for math/coq updating to 8.4pl3. I compiled and run on amd64. please check and commit to the tree.
-- yozo. x---x---x---x---x---x---x---x---x---x---x---x---x---x---x---x-----x---x---x---x --- coq.OLD/Makefile Sun Nov 10 16:16:00 2013 +++ coq/Makefile Tue Dec 24 08:41:49 2013 @@ -1,46 +1,45 @@ -# $OpenBSD: Makefile,v 1.24 2013/11/08 23:11:48 sthen Exp $ +# $OpenBSD: Makefile.template,v 1.68 2013/10/02 07:34:45 ajacoutot Exp $ COMMENT= proof assistant based on a typed lambda calculus -V= 8.4pl2 -DISTNAME= coq-$V +V = 8.4pl3 +DISTNAME = coq-$V -CATEGORIES= math -HOMEPAGE= http://coq.inria.fr/ +CATEGORIES = math -MAINTAINER= Yozo Toda <y...@v007.vaio.ne.jp> +HOMEPAGE = http://coq.inria.fr/ +MAINTAINER = Yozo TODA <y...@v007.vaio.ne.jp> + # LGPL 2.1 -PERMIT_PACKAGE_CDROM= Yes +PERMIT_PACKAGE_CDROM = Yes -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 m pango-1.0 pangocairo-1.0 -WANTLIB += pangoft2-1.0 pixman-1 png pthread pthread-stubs -WANTLIB += xcb xcb-render xcb-shm z +WANTLIB += X11 Xcomposite Xcursor Xdamage Xext Xfixes Xi Xinerama +WANTLIB += Xrandr Xrender atk-1.0 c cairo 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 m pango-1.0 pangocairo-1.0 pangoft2-1.0 +WANTLIB += pthread z -MASTER_SITES= ${HOMEPAGE}distrib/V${V}/files/ +MASTER_SITES = ${HOMEPAGE}distrib/V${V}/files/ -RUN_DEPENDS= x11/lablgtk2 -BUILD_DEPENDS= ${RUN_DEPENDS} \ - sysutils/findlib - DESTDIRNAME= COQINSTALLPREFIX -USE_GMAKE= Yes -USE_GROFF= Yes +MODULES = devel/gettext \ + lang/ocaml +RUN_DEPENDS = x11/lablgtk2 +BUILD_DEPENDS = ${RUN_DEPENDS} \ + sysutils/findlib -MODULES= devel/gettext \ - lang/ocaml +USE_GMAKE = Yes +USE_GROFF = Yes -CONFIGURE_STYLE= simple -CONFIGURE_ARGS= -emacslib ${PREFIX}/share/emacs/site-lisp \ - -makecmd ${GMAKE} \ - -prefix ${PREFIX} \ - -mandir ${PREFIX}/man \ - -configdir ${SYSCONFDIR}/xdg/coq \ - -usecamlp4 +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} @@ -49,10 +48,10 @@ CONFIGURE_ARGS+= -byteonly .endif -ALL_TARGET= world +ALL_TARGET = world # Order is important! INSTALL_TARGET= install-byte install-ide-byte install -TEST_TARGET= check +TEST_TARGET = check post-install: cd ${WRKDIST}; ${INSTALL_DATA} LICENSE COPYRIGHT CREDITS CHANGES \ diff -urd coq.OLD/distinfo coq/distinfo --- coq.OLD/distinfo Sun Nov 10 16:16:00 2013 +++ coq/distinfo Mon Dec 23 13:56:47 2013 @@ -1,2 +1,2 @@ -SHA256 (coq-8.4pl2.tar.gz) = +3GaOPYTsBhh47JR50WlyO85WibOcClmjoWsdfy8otg= -SIZE (coq-8.4pl2.tar.gz) = 4145112 +SHA256 (coq-8.4pl3.tar.gz) = l1g9Y3+YHFVUAH9Omc5kIOvHNxhrHQIb1xdm/Ykc+zg= +SIZE (coq-8.4pl3.tar.gz) = 4064579 diff -urd coq.OLD/patches/patch-Makefile_build coq/patches/patch-Makefile_build --- coq.OLD/patches/patch-Makefile_build Sun Nov 10 16:16:00 2013 +++ coq/patches/patch-Makefile_build Tue Dec 24 01:16:00 2013 @@ -1,11 +1,9 @@ -$OpenBSD: patch-Makefile_build,v 1.3 2013/11/08 23:11:48 sthen Exp $ - Remove the -silent flag to see what the validation suite is doing as it runs for eons. ---- Makefile.build.orig Mon Oct 29 10:46:37 2012 -+++ Makefile.build Sun Apr 7 14:14:26 2013 -@@ -381,7 +381,7 @@ install-ide-info: +--- Makefile.build.orig Sat Dec 21 17:03:14 2013 ++++ Makefile.build Tue Dec 24 01:09:39 2013 +@@ -381,7 +381,7 @@ .PHONY: validate check test-suite $(ALLSTDLIB).v @@ -14,7 +12,7 @@ validate:: $(BESTCHICKEN) $(ALLVO) $(SHOW)'COQCHK <theories & plugins>' -@@ -612,7 +612,7 @@ install-binaries:: install-$(BEST) install-tools +@@ -612,7 +612,7 @@ install-byte:: $(MKDIR) $(FULLBINDIR) diff -urd coq.OLD/patches/patch-configure coq/patches/patch-configure --- coq.OLD/patches/patch-configure Wed Oct 30 01:24:31 2013 +++ coq/patches/patch-configure Tue Dec 24 01:18:56 2013 @@ -1,24 +1,13 @@ -$OpenBSD: patch-configure,v 1.4 2013/10/26 07:38:19 brad Exp $ +Remove unnecessary single quotes. -Fix GNU make check with newer versions. - ---- configure.orig Sat Dec 22 05:06:16 2012 -+++ configure Fri Oct 25 14:38:49 2013 -@@ -335,7 +335,7 @@ if [ "$MAKE" != "" ]; then - MAKEVERSION=`$MAKE -v | head -1 | cut -d" " -f3` - MAKEVERSIONMAJOR=`echo $MAKEVERSION | cut -d. -f1` - MAKEVERSIONMINOR=`echo $MAKEVERSION | cut -d. -f2` -- if [ "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 ]; then -+ if [ "$MAKEVERSIONMAJOR" -gt 3 -o "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 ]; then - echo "You have GNU Make $MAKEVERSION. Good!" - else - OK="no" -@@ -887,7 +887,7 @@ case $coqrunbyteflags_spec/$local/$custom_spec/$CUSTOM +--- configure.orig Sat Dec 21 17:03:14 2013 ++++ configure Tue Dec 24 01:07:12 2013 +@@ -897,7 +897,7 @@ */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";; +- BUILDLDPATH="export CAML_LD_LIBRARY_PATH='$COQTOP'/kernel/byterun:$CAML_LD_LIBRARY_PATH";; ++ BUILDLDPATH="export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH";; esac case $coqtoolsbyteflags_spec/$custom_spec/$CUSTOM_OS in yes/*/*) COQTOOLSBYTEFLAGS="$coqtoolsbyteflags";; diff -urd coq.OLD/patches/patch-test-suite-Makefile coq/patches/patch-test-suite-Makefile --- coq.OLD/patches/patch-test-suite-Makefile Sun Nov 10 16:16:00 2013 +++ coq/patches/patch-test-suite-Makefile Tue Dec 24 01:19:29 2013 @@ -1,14 +1,6 @@ ---- test-suite/Makefile.orig Tue Jan 17 11:10:51 2012 -+++ test-suite/Makefile Tue Apr 23 14:56:48 2013 -@@ -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 -@@ -54,7 +55,7 @@ ifneq (,$(wildcard /proc/cpuinfo)) +--- test-suite/Makefile.orig Sat Dec 21 17:03:14 2013 ++++ test-suite/Makefile Tue Dec 24 01:12:50 2013 +@@ -55,7 +55,7 @@ endif ifeq (,$(bogomips)) @@ -17,7 +9,7 @@ endif log_success = "==========> SUCCESS <==========" -@@ -112,7 +113,7 @@ $(foreach S,$(VSUBSYSTEMS),$(eval $(call mkstamp,$(S)) +@@ -113,7 +113,7 @@ # Summary ####################################################################### diff -urd coq.OLD/pkg/PFRAG.dynlink-native coq/pkg/PFRAG.dynlink-native --- coq.OLD/pkg/PFRAG.dynlink-native Fri Jan 4 20:07:29 2013 +++ coq/pkg/PFRAG.dynlink-native Tue Dec 24 02:39:34 2013 @@ -52,3 +52,4 @@ lib/coq/tactics/tactics.cmxa lib/coq/toplevel/toplevel.a lib/coq/toplevel/toplevel.cmxa +@man man/man1/coqtop.opt.1 diff -urd coq.OLD/pkg/PFRAG.shared coq/pkg/PFRAG.shared --- coq.OLD/pkg/PFRAG.shared Fri Jan 4 20:07:29 2013 +++ coq/pkg/PFRAG.shared Tue Dec 24 02:06:14 2013 @@ -1,2 +1,2 @@ -@comment $OpenBSD: PFRAG.shared,v 1.1 2013/01/04 11:07:29 chrisz Exp $ +@comment $OpenBSD$ lib/coq/dllcoqrun.so diff -urd coq.OLD/pkg/PLIST coq/pkg/PLIST --- coq.OLD/pkg/PLIST Sun Nov 10 16:16:00 2013 +++ coq/pkg/PLIST Tue Dec 24 02:40:10 2013 @@ -1,4 +1,4 @@ -@comment $OpenBSD: PLIST,v 1.6 2013/11/08 23:11:48 sthen Exp $ +@comment $OpenBSD$ %%SHARED%% %%native%% @bin bin/coq-tex @@ -992,7 +992,6 @@ @man man/man1/coqmktop.1 @man man/man1/coqtop.1 @man man/man1/coqtop.byte.1 -@man man/man1/coqtop.opt.1 @man man/man1/coqwc.1 @man man/man1/gallina.1 share/coq/ x---x---x---x---x---x---x---x---x---x---x---x---x---x---x---x-----x---x---x---x
