Here is an update of math/coq to 8.4pl2. This was tested on i386 by
running the regression tests which ran fine.
Highlights of changes:
- patch-scripts_coqmktop_ml was backported to 8.4pl1 and can now be
removed.
- The -silent flag was removed from the regression tests as it's nice
to see things progressing (regress tests take hours to run).
Here are the changes as per the coq website
(http://coq.inria.fr/distrib/V8.4pl2/CHANGES):
==
Bug fixes
- Solved bugs :
#2466 #2629 #2668 #2750 #2839 #2869 #2954 #2955 #2959 #2962 #2966 #2967
#2969 #2970 #2975 #2976 #2977 #2978 #2981 #2983 #2995 #3000 #3004 #3008
- Partially fixed bugs : #2830 #2949
- Coqtop should now react more reliably when receiving interrupt signals:
all the try...with constructs have been protected against undue
handling of the Sys.Break exception.
Coqide
- The Windows-specific code handling the interrupt button of Coqide
had to be reworked (cf. bug #2869). Now, in Win32 this button does
not target a specific coqtop client, but instead sends a Ctrl-C to
any process sharing its console with Coqide. To avoid awkward
effects, it is recommended to launch Coqide via its icon, its menu,
or in a dedicated console window.
Extraction
- The option Extraction AccessOpaque is now set by default,
restoring compatibility of older versions of Coq (cf bug #2952).
Index: Makefile
===
RCS file: /home/cvs/ports/math/coq/Makefile,v
retrieving revision 1.23
diff -u -p -u -r1.23 Makefile
--- Makefile16 May 2013 09:16:43 - 1.23
+++ Makefile27 Oct 2013 23:12:45 -
@@ -2,9 +2,9 @@
COMMENT= proof assistant based on a typed lambda calculus
-V= 8.4pl1
+V= 8.4pl2
DISTNAME= coq-$V
-REVISION= 0
+
CATEGORIES=math
HOMEPAGE= http://coq.inria.fr/
Index: distinfo
===
RCS file: /home/cvs/ports/math/coq/distinfo,v
retrieving revision 1.8
diff -u -p -u -r1.8 distinfo
--- distinfo7 Feb 2013 09:43:15 - 1.8
+++ distinfo27 Oct 2013 23:12:45 -
@@ -1,2 +1,2 @@
-SHA256 (coq-8.4pl1.tar.gz) = XQ5FU6tQZ3qUtNXKFlCpBxjpNiCCpkm6lb5AEDkKD4A=
-SIZE (coq-8.4pl1.tar.gz) = 4139808
+SHA256 (coq-8.4pl2.tar.gz) = +3GaOPYTsBhh47JR50WlyO85WibOcClmjoWsdfy8otg=
+SIZE (coq-8.4pl2.tar.gz) = 4145112
Index: patches/patch-Makefile_build
===
RCS file: /home/cvs/ports/math/coq/patches/patch-Makefile_build,v
retrieving revision 1.2
diff -u -p -u -r1.2 patch-Makefile_build
--- patches/patch-Makefile_build7 Feb 2013 09:43:15 - 1.2
+++ patches/patch-Makefile_build27 Oct 2013 23:12:45 -
@@ -1,6 +1,19 @@
$OpenBSD: patch-Makefile_build,v 1.2 2013/02/07 09:43:15 chrisz Exp $
Makefile.build.origMon Oct 29 15:46:37 2012
-+++ Makefile.build Sat Feb 2 18:06:08 2013
+
+Remove the -silent flag to see what the validation suite is doing as it
+runs for eons.
+
+--- Makefile.build.origMon Oct 29 10:46:37 2012
Makefile.build Sun Apr 7 14:14:26 2013
+@@ -381,7 +381,7 @@ install-ide-info:
+
+ .PHONY: validate check test-suite $(ALLSTDLIB).v
+
+-VALIDOPTS=-silent -o -m
++VALIDOPTS=-o -m
+
+ validate:: $(BESTCHICKEN) $(ALLVO)
+ $(SHOW)'COQCHK theories plugins'
@@ -612,7 +612,7 @@ install-binaries:: install-$(BEST) install-tools
install-byte::
Index: patches/patch-scripts_coqmktop_ml
===
RCS file: /home/cvs/ports/math/coq/patches/patch-scripts_coqmktop_ml,v
retrieving revision 1.1
diff -u -p -u -r1.1 patch-scripts_coqmktop_ml
--- patches/patch-scripts_coqmktop_ml 7 Feb 2013 09:43:15 - 1.1
+++ patches/patch-scripts_coqmktop_ml 27 Oct 2013 23:12:45 -
@@ -1,23 +0,0 @@
-$OpenBSD: patch-scripts_coqmktop_ml,v 1.1 2013/02/07 09:43:15 chrisz Exp $
-
-Compiling with camlp4 is broken in 8.4 and 8.4pl1. The patch below is needed
-for things to work. A better approach is to migrate to camlp5.
-
-Discussion here:
-https://sympa.inria.fr/sympa/arc/coq-club/2013-01/msg00067.html
-
-Patch here:
-https://gforge.inria.fr/scm/viewvc.php/branches/v8.4/scripts/coqmktop.ml?root=coqr1=16015r2=16122pathrev=16122
-
scripts/coqmktop.ml.orig Tue Dec 4 14:40:45 2012
-+++ scripts/coqmktop.mlSat Feb 2 18:44:09 2013
-@@ -45,8 +45,7 @@ let camlp4topobjs =
- [ Camlp4Top.cmo;
- Camlp4Parsers/Camlp4OCamlRevisedParser.cmo;
- Camlp4Parsers/Camlp4OCamlParser.cmo;
-- Camlp4Parsers/Camlp4GrammarParser.cmo;
-- q_util.cmo; q_coqast.cmo ]
-+ Camlp4Parsers/Camlp4GrammarParser.cmo]
- let topobjs = camlp4topobjs
-
- let gramobjs = []
Index: patches/patch-test-suite-Makefile
===
RCS file:
