The patch below is mostly from Yozo Toda. I've been running it for weeks
on i386. Be great to get this in.
Port changes:
- Update math/coq from 8.4pl2 to 8.4pl3
- Remove patches already integrated into upstream
- Add missing $OpenBSD$ tag to patch-test-suite-Makefile
- Move coqtop.opt.1 from PLIST to PFRAG.dynlink-native
which is where coqtop.opt lives.
Index: Makefile
===================================================================
RCS file: /home/cvs/ports/math/coq/Makefile,v
retrieving revision 1.24
diff -u -p -u -r1.24 Makefile
--- Makefile 8 Nov 2013 23:11:48 -0000 1.24
+++ Makefile 2 Jan 2014 01:10:45 -0000
@@ -2,7 +2,7 @@
COMMENT= proof assistant based on a typed lambda calculus
-V= 8.4pl2
+V= 8.4pl3
DISTNAME= coq-$V
CATEGORIES= math
@@ -13,14 +13,14 @@ MAINTAINER= Yozo Toda <y...@v007.vaio.n
# LGPL 2.1
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 += 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
-WANTLIB += pangoft2-1.0 pixman-1 png pthread pthread-stubs
-WANTLIB += xcb xcb-render xcb-shm z
+WANTLIB += pangoft2-1.0 pthread
+WANTLIB += z
-MASTER_SITES= ${HOMEPAGE}distrib/V${V}/files/
+MASTER_SITES= http://coq.inria.fr/distrib/V${V}/files/
RUN_DEPENDS= x11/lablgtk2
BUILD_DEPENDS= ${RUN_DEPENDS} \
Index: distinfo
===================================================================
RCS file: /home/cvs/ports/math/coq/distinfo,v
retrieving revision 1.9
diff -u -p -u -r1.9 distinfo
--- distinfo 8 Nov 2013 23:11:48 -0000 1.9
+++ distinfo 30 Dec 2013 23:39:10 -0000
@@ -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
Index: patches/patch-configure
===================================================================
RCS file: /home/cvs/ports/math/coq/patches/patch-configure,v
retrieving revision 1.4
diff -u -p -u -r1.4 patch-configure
--- patches/patch-configure 26 Oct 2013 07:38:19 -0000 1.4
+++ patches/patch-configure 31 Dec 2013 00:05:03 -0000
@@ -1,24 +1,13 @@
$OpenBSD: patch-configure,v 1.4 2013/10/26 07:38:19 brad Exp $
-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 03:03:14 2013
++++ configure Mon Dec 30 19:04:42 2013
+@@ -897,7 +897,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";;
+- 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";;
Index: patches/patch-test-suite-Makefile
===================================================================
RCS file: /home/cvs/ports/math/coq/patches/patch-test-suite-Makefile,v
retrieving revision 1.2
diff -u -p -u -r1.2 patch-test-suite-Makefile
--- patches/patch-test-suite-Makefile 8 Nov 2013 23:11:48 -0000 1.2
+++ patches/patch-test-suite-Makefile 2 Jan 2014 00:51:34 -0000
@@ -1,14 +1,8 @@
---- 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))
+$OpenBSD$
+
+--- test-suite/Makefile.orig Mon Dec 30 19:05:22 2013
++++ test-suite/Makefile Mon Dec 30 19:06:15 2013
+@@ -55,7 +55,7 @@ ifneq (,$(wildcard /proc/cpuinfo))
endif
ifeq (,$(bogomips))
@@ -17,7 +11,7 @@
endif
log_success = "==========> SUCCESS <=========="
-@@ -112,7 +113,7 @@ $(foreach S,$(VSUBSYSTEMS),$(eval $(call mkstamp,$(S))
+@@ -113,7 +113,7 @@ $(foreach S,$(VSUBSYSTEMS),$(eval $(call mkstamp,$(S))
# Summary
#######################################################################
Index: pkg/PFRAG.dynlink-native
===================================================================
RCS file: /home/cvs/ports/math/coq/pkg/PFRAG.dynlink-native,v
retrieving revision 1.1
diff -u -p -u -r1.1 PFRAG.dynlink-native
--- pkg/PFRAG.dynlink-native 4 Jan 2013 11:07:29 -0000 1.1
+++ pkg/PFRAG.dynlink-native 2 Jan 2014 01:01:14 -0000
@@ -52,3 +52,4 @@ lib/coq/tactics/tactics.a
lib/coq/tactics/tactics.cmxa
lib/coq/toplevel/toplevel.a
lib/coq/toplevel/toplevel.cmxa
+@man man/man1/coqtop.opt.1
Index: pkg/PLIST
===================================================================
RCS file: /home/cvs/ports/math/coq/pkg/PLIST,v
retrieving revision 1.6
diff -u -p -u -r1.6 PLIST
--- pkg/PLIST 8 Nov 2013 23:11:48 -0000 1.6
+++ pkg/PLIST 2 Jan 2014 01:00:54 -0000
@@ -992,7 +992,6 @@ lib/coq/user-contrib/
@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/
