here is an update for math/coq, to 8.4pl5. confirmed on amd64. thanks chrisz and nigel for preparing this update. I just confirmed that the patch works. (and, as in previous revisions, "make test" fails without enough memory.)
-- yozo. diff -Nru -x CVS /usr/ports/math/coq/Makefile ./Makefile --- /usr/ports/math/coq/Makefile Sun Sep 14 16:33:29 2014 +++ ./Makefile Sat Nov 1 15:19:31 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 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 -