> Looks like in this case adding "--with-doc=no" should do the
> trick.
yeah, right!
I re-created the update patch for coq 8.4pl5, adding "-with-doc no".
Works on my amd64 environment (without latex, hevea).
please check and commit this to the ports tree?
-- yozo.
diff -Nru -x CVS /usr/ports/math/coq/Makefile ./Makefile
--- /usr/ports/math/coq/Makefile Sun Sep 14 16:33:29 2014
+++ ./Makefile Mon Nov 17 08:46:03 2014
@@ -2,7 +2,7 @@
COMMENT= proof assistant based on a typed lambda calculus
-V= 8.4pl4
+V= 8.4pl5
DISTNAME= coq-$V
CATEGORIES= math
@@ -45,9 +45,9 @@
.include <bsd.port.arch.mk>
.if ${PROPERTIES:Mocaml_native_dynlink}
-CONFIGURE_ARGS+= -opt
+CONFIGURE_ARGS+= -opt -with-doc no
.else
-CONFIGURE_ARGS+= -byteonly
+CONFIGURE_ARGS+= -byteonly -with-doc no
.endif
ALL_TARGET= world
diff -Nru -x CVS /usr/ports/math/coq/distinfo ./distinfo
--- /usr/ports/math/coq/distinfo Fri Aug 29 01:22:24 2014
+++ ./distinfo Sat Nov 1 15:19:31 2014
@@ -1,2 +1,2 @@
-SHA256 (coq-8.4pl4.tar.gz) = BsOuq3gZ7tjzXOeUyIenDPO09rce5SzTEQ+05SZxfwE=
-SIZE (coq-8.4pl4.tar.gz) = 4067355
+SHA256 (coq-8.4pl5.tar.gz) = NYFat4pY1yeZ6sqrFVQnYgqwcWd4gspsmNe/7JfSUkU=
+SIZE (coq-8.4pl5.tar.gz) = 4070062
diff -Nru -x CVS /usr/ports/math/coq/patches/patch-kernel_univ_ml
./patches/patch-kernel_univ_ml
--- /usr/ports/math/coq/patches/patch-kernel_univ_ml Wed Aug 27 18:44:59 2014
+++ ./patches/patch-kernel_univ_ml Thu Jan 1 09:00:00 1970
@@ -1,16 +0,0 @@
-$OpenBSD: patch-kernel_univ_ml,v 1.1 2014/08/27 09:44:59 daniel Exp $
-
-Backport fix for new string syntax in OCaml 4.02 comments:
-commit a3beca520724057a010a4b972b43d12bcf09f27e
-
---- kernel/univ.ml.orig Tue Aug 26 23:39:35 2014
-+++ kernel/univ.ml Tue Aug 26 23:40:14 2014
-@@ -226,7 +226,7 @@ let reprleq g arcu =
-
-
- (* between : UniverseLevel.t -> canonical_arc -> canonical_arc list *)
--(* between u v = {w|u<=w<=v, w canonical} *)
-+(* between u v = { w | u<=w<=v, w canonical } *)
- (* between is the most costly operation *)
-
- let between g arcu arcv =
diff -Nru -x CVS /usr/ports/math/coq/patches/patch-test-suite-Makefile
./patches/patch-test-suite-Makefile
--- /usr/ports/math/coq/patches/patch-test-suite-Makefile Fri Aug 29
01:22:24 2014
+++ ./patches/patch-test-suite-Makefile Thu Jan 1 09:00:00 1970
@@ -1,25 +0,0 @@
-$OpenBSD: patch-test-suite-Makefile,v 1.4 2014/08/27 09:44:59 daniel Exp $
-
-The 2nd hunk is backported from:
-commit b8e76c36b0fd4016c4d5b4098a11dc733872ff5f
-
---- 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))
-- $(warning cannot run complexity tests (no bogomips found))
-+ $(warning cannot run complexity tests on OpenBSD)
- endif
-
- log_success = "==========> SUCCESS <=========="
-@@ -113,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
-
- .PHONY: summary summary.log
-
