Here's an update to the latest beta of coq 8.10. Tested on i386.
Bug fixes from the release notes:
- improved warnings on coercion path ambiguity
- support for ocaml extraction of primitive machine ints
- fix for the soundness issue with template polymorphism
- fix extraction of depenent record projections to ocaml
I've also made the regress tests verbose like we used to have, but which
seems to have gotten lost in one of the recent updates.
ok?
Index: Makefile
===================================================================
RCS file: /cvs/ports/math/coq/Makefile,v
retrieving revision 1.42
diff -u -p -u -r1.42 Makefile
--- Makefile 10 Sep 2019 14:09:17 -0000 1.42
+++ Makefile 17 Sep 2019 04:20:51 -0000
@@ -2,7 +2,7 @@
COMMENT= proof assistant based on a typed lambda calculus
-V= 8.10+beta2
+V= 8.10+beta3
GH_ACCOUNT = coq
GH_PROJECT = coq
GH_TAGNAME = V${V}
@@ -50,6 +50,7 @@ ALL_TARGET= byte coq documentation \
INSTALL_TARGET= install-coq install-byte install-meta
.endif
+TEST_ENV= VERBOSE=1
TEST_TARGET= check
do-build:
Index: distinfo
===================================================================
RCS file: /cvs/ports/math/coq/distinfo,v
retrieving revision 1.15
diff -u -p -u -r1.15 distinfo
--- distinfo 6 Sep 2019 22:10:18 -0000 1.15
+++ distinfo 17 Sep 2019 04:20:51 -0000
@@ -1,2 +1,2 @@
-SHA256 (coq-8.10beta2.tar.gz) = LIK7Tew3o/+lfuDWQm8OfezMbLM0AA2+Z7DNUV2FUBY=
-SIZE (coq-8.10beta2.tar.gz) = 6211659
+SHA256 (coq-8.10beta3.tar.gz) = bg4NOETRztaP1HlgLSQ5QBLSLEfSrbTJoBtNCGoYAxg=
+SIZE (coq-8.10beta3.tar.gz) = 6220619
Index: pkg/PFRAG.dynlink-native
===================================================================
RCS file: /cvs/ports/math/coq/pkg/PFRAG.dynlink-native,v
retrieving revision 1.5
diff -u -p -u -r1.5 PFRAG.dynlink-native
--- pkg/PFRAG.dynlink-native 6 Sep 2019 22:10:18 -0000 1.5
+++ pkg/PFRAG.dynlink-native 17 Sep 2019 04:20:52 -0000
@@ -14,6 +14,7 @@
@bin
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInt.cmxs
@bin
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInteger.cmxs
@bin
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmxs
+@bin
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmxs
@bin
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmxs
@bin
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBigIntConv.cmxs
@bin
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlIntConv.cmxs
Index: pkg/PFRAG.native
===================================================================
RCS file: /cvs/ports/math/coq/pkg/PFRAG.native,v
retrieving revision 1.4
diff -u -p -u -r1.4 PFRAG.native
--- pkg/PFRAG.native 6 Sep 2019 22:10:18 -0000 1.4
+++ pkg/PFRAG.native 17 Sep 2019 04:20:54 -0000
@@ -241,6 +241,8 @@ lib/ocaml/coq/plugins/extraction/.coq-na
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInteger.o
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmx
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.o
+lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmx
+lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.o
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmx
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.o
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBigIntConv.cmx
Index: pkg/PLIST
===================================================================
RCS file: /cvs/ports/math/coq/pkg/PLIST,v
retrieving revision 1.12
diff -u -p -u -r1.12 PLIST
--- pkg/PLIST 6 Sep 2019 22:10:18 -0000 1.12
+++ pkg/PLIST 17 Sep 2019 04:20:56 -0000
@@ -287,6 +287,7 @@ lib/ocaml/coq/plugins/extraction/.coq-na
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInt.cmi
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInteger.cmi
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmi
+lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmi
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmi
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBigIntConv.cmi
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlIntConv.cmi
@@ -320,6 +321,9 @@ lib/ocaml/coq/plugins/extraction/ExtrHas
lib/ocaml/coq/plugins/extraction/ExtrHaskellZNum.glob
lib/ocaml/coq/plugins/extraction/ExtrHaskellZNum.v
lib/ocaml/coq/plugins/extraction/ExtrHaskellZNum.vo
+lib/ocaml/coq/plugins/extraction/ExtrOCamlInt63.glob
+lib/ocaml/coq/plugins/extraction/ExtrOCamlInt63.v
+lib/ocaml/coq/plugins/extraction/ExtrOCamlInt63.vo
lib/ocaml/coq/plugins/extraction/ExtrOcamlBasic.glob
lib/ocaml/coq/plugins/extraction/ExtrOcamlBasic.v
lib/ocaml/coq/plugins/extraction/ExtrOcamlBasic.vo
