Update to 8.4pl4. Compilation problem with ocaml 4.02 noted by chrisz@;
fix taken from coq trunk. ok Yozo Toda (MAINTAINER) some time ago. ok chrisz@
This commit is contained in:
parent
af3d5de0e2
commit
ad7f6192e7
@ -1,10 +1,9 @@
|
||||
# $OpenBSD: Makefile,v 1.26 2014/08/23 07:09:18 chrisz Exp $
|
||||
# $OpenBSD: Makefile,v 1.27 2014/08/27 09:44:59 daniel Exp $
|
||||
|
||||
COMMENT= proof assistant based on a typed lambda calculus
|
||||
|
||||
V= 8.4pl3
|
||||
V= 8.4pl4
|
||||
DISTNAME= coq-$V
|
||||
REVISION = 0
|
||||
|
||||
CATEGORIES= math
|
||||
HOMEPAGE= http://coq.inria.fr/
|
||||
|
@ -1,2 +1,2 @@
|
||||
SHA256 (coq-8.4pl3.tar.gz) = l1g9Y3+YHFVUAH9Omc5kIOvHNxhrHQIb1xdm/Ykc+zg=
|
||||
SIZE (coq-8.4pl3.tar.gz) = 4064579
|
||||
SHA256 (coq-8.4pl4.tar.gz) = BsOuq3gZ7tjzXOeUyIenDPO09rce5SzTEQ+05SZxfwE=
|
||||
SIZE (coq-8.4pl4.tar.gz) = 4067355
|
||||
|
16
math/coq/patches/patch-kernel_univ_ml
Normal file
16
math/coq/patches/patch-kernel_univ_ml
Normal file
@ -0,0 +1,16 @@
|
||||
$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 =
|
@ -1,4 +1,7 @@
|
||||
$OpenBSD: patch-test-suite-Makefile,v 1.3 2014/03/26 03:27:26 daniel Exp $
|
||||
$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
|
||||
@ -16,7 +19,7 @@ $OpenBSD: patch-test-suite-Makefile,v 1.3 2014/03/26 03:27:26 daniel Exp $
|
||||
#######################################################################
|
||||
|
||||
-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
|
||||
+summary_dir = echo $(1); find $(2) -name '*.log' -print0 | xargs -0 -n 1 tail -n1 | sort
|
||||
|
||||
.PHONY: summary summary.log
|
||||
|
||||
|
Loading…
x
Reference in New Issue
Block a user