[pkgsrc/trunk]: pkgsrc/lang/coq Updated lang/coq to version 8.7.2.

[jaapb <jaapb%pkgsrc.org@localhost>]

details:   https://anonhg.NetBSD.org/pkgsrc/rev/5a8280111b7b
branches:  trunk
changeset: 378503:5a8280111b7b
user:      jaapb <jaapb%pkgsrc.org@localhost>
date:      Mon Apr 09 11:29:23 2018 +0000

description:
Updated lang/coq to version 8.7.2.

This fixes a critical bug in the VM handling of universes, and adds
various other minor fixes and improvements.

diffstat:

 lang/coq/Makefile |  10 ++++++----
 lang/coq/PLIST    |  28 ++++++++++++++++++++++++++--
 lang/coq/distinfo |  10 +++++-----
 3 files changed, 37 insertions(+), 11 deletions(-)

diffs (238 lines):

diff -r fc95ce879829 -r 5a8280111b7b lang/coq/Makefile
--- a/lang/coq/Makefile Mon Apr 09 11:26:02 2018 +0000
+++ b/lang/coq/Makefile Mon Apr 09 11:29:23 2018 +0000
@@ -1,16 +1,18 @@
-# $NetBSD: Makefile,v 1.106 2018/03/12 11:16:58 wiz Exp $
+# $NetBSD: Makefile,v 1.107 2018/04/09 11:29:23 jaapb Exp $
 #
 
-DISTNAME=      coq-8.7.1
-PKGREVISION=   2
+DISTNAME=      coq-8.7.2
 CATEGORIES=    lang math
-MASTER_SITES=  http://coq.inria.fr/distrib/V${PKGVERSION_NOREV}/files/
+MASTER_SITES=  ${MASTER_SITE_GITHUB:=coq/}
+GITHUB_TAG=    V${PKGVERSION_NOREV}
 
 MAINTAINER=    jaapb%NetBSD.org@localhost
 HOMEPAGE=      http://coq.inria.fr/
 COMMENT=       Theorem prover which extracts programs from proofs
 LICENSE=       gnu-lgpl-v2.1
 
+WRKSRC=                ${WRKDIR}/${DISTNAME}
+
 USE_TOOLS+=            gmake
 HAS_CONFIGURE=         yes
 CONFIGURE_ARGS+=       -prefix ${PREFIX}
diff -r fc95ce879829 -r 5a8280111b7b lang/coq/PLIST
--- a/lang/coq/PLIST    Mon Apr 09 11:26:02 2018 +0000
+++ b/lang/coq/PLIST    Mon Apr 09 11:29:23 2018 +0000
@@ -1,4 +1,4 @@
-@comment $NetBSD: PLIST,v 1.25 2018/01/22 11:54:43 jaapb Exp $
+@comment $NetBSD: PLIST,v 1.26 2018/04/09 11:29:23 jaapb Exp $
 bin/coq-tex
 bin/coq_makefile
 bin/coqc
@@ -440,11 +440,13 @@
 lib/coq/plugins/btauto/Reflect.v
 lib/coq/plugins/btauto/Reflect.vo
 lib/coq/plugins/btauto/btauto_plugin.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/btauto/btauto_plugin.cmx
 ${PLIST.natdynlink}lib/coq/plugins/btauto/btauto_plugin.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/btauto/btauto_plugin.o
 ${PLIST.ocaml-opt}lib/coq/plugins/btauto/g_btauto.cmx
 ${PLIST.ocaml-opt}lib/coq/plugins/btauto/refl_btauto.cmx
 lib/coq/plugins/cc/cc_plugin.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/cc/cc_plugin.cmx
 ${PLIST.natdynlink}lib/coq/plugins/cc/cc_plugin.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/cc/cc_plugin.o
 lib/coq/plugins/cc/ccalgo.cmi
@@ -464,6 +466,7 @@
 lib/coq/plugins/derive/derive.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/derive/derive.cmx
 lib/coq/plugins/derive/derive_plugin.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/derive/derive_plugin.cmx
 ${PLIST.natdynlink}lib/coq/plugins/derive/derive_plugin.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/derive/derive_plugin.o
 ${PLIST.ocaml-opt}lib/coq/plugins/derive/g_derive.cmx
@@ -593,6 +596,7 @@
 lib/coq/plugins/extraction/extraction.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/extraction/extraction.cmx
 lib/coq/plugins/extraction/extraction_plugin.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/extraction/extraction_plugin.cmx
 ${PLIST.natdynlink}lib/coq/plugins/extraction/extraction_plugin.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/extraction/extraction_plugin.o
 ${PLIST.ocaml-opt}lib/coq/plugins/extraction/g_extraction.cmx
@@ -617,6 +621,7 @@
 lib/coq/plugins/firstorder/ground.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/firstorder/ground.cmx
 lib/coq/plugins/firstorder/ground_plugin.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/firstorder/ground_plugin.cmx
 ${PLIST.natdynlink}lib/coq/plugins/firstorder/ground_plugin.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/firstorder/ground_plugin.o
 lib/coq/plugins/firstorder/instances.cmi
@@ -644,6 +649,7 @@
 ${PLIST.ocaml-opt}lib/coq/plugins/fourier/fourier.cmx
 ${PLIST.ocaml-opt}lib/coq/plugins/fourier/fourierR.cmx
 lib/coq/plugins/fourier/fourier_plugin.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/fourier/fourier_plugin.cmx
 ${PLIST.natdynlink}lib/coq/plugins/fourier/fourier_plugin.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/fourier/fourier_plugin.o
 ${PLIST.ocaml-opt}lib/coq/plugins/fourier/g_fourier.cmx
@@ -679,6 +685,7 @@
 lib/coq/plugins/funind/recdef.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/funind/recdef.cmx
 lib/coq/plugins/funind/recdef_plugin.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/funind/recdef_plugin.cmx
 ${PLIST.natdynlink}lib/coq/plugins/funind/recdef_plugin.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/funind/recdef_plugin.o
 ${PLIST.native}lib/coq/plugins/ltac/.coq-native/NCoq_ltac_Ltac.cmi
@@ -703,6 +710,7 @@
 ${PLIST.ocaml-opt}lib/coq/plugins/ltac/g_rewrite.cmx
 ${PLIST.ocaml-opt}lib/coq/plugins/ltac/g_tactic.cmx
 lib/coq/plugins/ltac/ltac_plugin.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/ltac_plugin.cmx
 ${PLIST.natdynlink}lib/coq/plugins/ltac/ltac_plugin.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/ltac/ltac_plugin.o
 lib/coq/plugins/ltac/pltac.cmi
@@ -738,6 +746,7 @@
 lib/coq/plugins/ltac/tauto.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/ltac/tauto.cmx
 lib/coq/plugins/ltac/tauto_plugin.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ltac/tauto_plugin.cmx
 ${PLIST.natdynlink}lib/coq/plugins/ltac/tauto_plugin.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/ltac/tauto_plugin.o
 ${PLIST.native}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmi
@@ -861,6 +870,7 @@
 lib/coq/plugins/micromega/micromega.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/micromega/micromega.cmx
 lib/coq/plugins/micromega/micromega_plugin.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/micromega/micromega_plugin.cmx
 ${PLIST.natdynlink}lib/coq/plugins/micromega/micromega_plugin.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/micromega/micromega_plugin.o
 ${PLIST.ocaml-opt}lib/coq/plugins/micromega/mutils.cmx
@@ -884,6 +894,7 @@
 lib/coq/plugins/nsatz/nsatz.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/nsatz/nsatz.cmx
 lib/coq/plugins/nsatz/nsatz_plugin.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/nsatz/nsatz_plugin.cmx
 ${PLIST.natdynlink}lib/coq/plugins/nsatz/nsatz_plugin.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/nsatz/nsatz_plugin.o
 lib/coq/plugins/nsatz/polynom.cmi
@@ -929,6 +940,7 @@
 ${PLIST.ocaml-opt}lib/coq/plugins/omega/g_omega.cmx
 ${PLIST.ocaml-opt}lib/coq/plugins/omega/omega.cmx
 lib/coq/plugins/omega/omega_plugin.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/omega/omega_plugin.cmx
 ${PLIST.natdynlink}lib/coq/plugins/omega/omega_plugin.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/omega/omega_plugin.o
 ${PLIST.native}lib/coq/plugins/quote/.coq-native/NCoq_quote_Quote.cmi
@@ -941,6 +953,7 @@
 ${PLIST.ocaml-opt}lib/coq/plugins/quote/g_quote.cmx
 ${PLIST.ocaml-opt}lib/coq/plugins/quote/quote.cmx
 lib/coq/plugins/quote/quote_plugin.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/quote/quote_plugin.cmx
 ${PLIST.natdynlink}lib/coq/plugins/quote/quote_plugin.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/quote/quote_plugin.o
 ${PLIST.native}lib/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.cmi
@@ -962,6 +975,7 @@
 ${PLIST.ocaml-opt}lib/coq/plugins/romega/g_romega.cmx
 ${PLIST.ocaml-opt}lib/coq/plugins/romega/refl_omega.cmx
 lib/coq/plugins/romega/romega_plugin.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/romega/romega_plugin.cmx
 ${PLIST.natdynlink}lib/coq/plugins/romega/romega_plugin.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/romega/romega_plugin.o
 ${PLIST.native}lib/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmi
@@ -984,6 +998,7 @@
 lib/coq/plugins/rtauto/refl_tauto.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/rtauto/refl_tauto.cmx
 lib/coq/plugins/rtauto/rtauto_plugin.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/rtauto/rtauto_plugin.cmx
 ${PLIST.natdynlink}lib/coq/plugins/rtauto/rtauto_plugin.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/rtauto/rtauto_plugin.o
 ${PLIST.native}lib/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.cmi
@@ -1159,6 +1174,7 @@
 ${PLIST.ocaml-opt}lib/coq/plugins/setoid_ring/newring.cmx
 lib/coq/plugins/setoid_ring/newring_ast.cmi
 lib/coq/plugins/setoid_ring/newring_plugin.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/setoid_ring/newring_plugin.cmx
 ${PLIST.natdynlink}lib/coq/plugins/setoid_ring/newring_plugin.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/setoid_ring/newring_plugin.o
 ${PLIST.native}lib/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrbool.cmi
@@ -1185,6 +1201,7 @@
 lib/coq/plugins/ssr/ssreflect.v
 lib/coq/plugins/ssr/ssreflect.vo
 lib/coq/plugins/ssr/ssreflect_plugin.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ssr/ssreflect_plugin.cmx
 ${PLIST.natdynlink}lib/coq/plugins/ssr/ssreflect_plugin.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/ssr/ssreflect_plugin.o
 lib/coq/plugins/ssr/ssrelim.cmi
@@ -1218,30 +1235,37 @@
 lib/coq/plugins/ssrmatching/ssrmatching.v
 lib/coq/plugins/ssrmatching/ssrmatching.vo
 lib/coq/plugins/ssrmatching/ssrmatching_plugin.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ssrmatching/ssrmatching_plugin.cmx
 ${PLIST.natdynlink}lib/coq/plugins/ssrmatching/ssrmatching_plugin.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/ssrmatching/ssrmatching_plugin.o
 ${PLIST.ocaml-opt}lib/coq/plugins/syntax/ascii_syntax.cmx
 lib/coq/plugins/syntax/ascii_syntax_plugin.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/syntax/ascii_syntax_plugin.cmx
 ${PLIST.natdynlink}lib/coq/plugins/syntax/ascii_syntax_plugin.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/syntax/ascii_syntax_plugin.o
 ${PLIST.ocaml-opt}lib/coq/plugins/syntax/int31_syntax.cmx
 lib/coq/plugins/syntax/int31_syntax_plugin.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/syntax/int31_syntax_plugin.cmx
 ${PLIST.natdynlink}lib/coq/plugins/syntax/int31_syntax_plugin.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/syntax/int31_syntax_plugin.o
 ${PLIST.ocaml-opt}lib/coq/plugins/syntax/nat_syntax.cmx
 lib/coq/plugins/syntax/nat_syntax_plugin.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/syntax/nat_syntax_plugin.cmx
 ${PLIST.natdynlink}lib/coq/plugins/syntax/nat_syntax_plugin.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/syntax/nat_syntax_plugin.o
 ${PLIST.ocaml-opt}lib/coq/plugins/syntax/r_syntax.cmx
 lib/coq/plugins/syntax/r_syntax_plugin.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/syntax/r_syntax_plugin.cmx
 ${PLIST.natdynlink}lib/coq/plugins/syntax/r_syntax_plugin.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/syntax/r_syntax_plugin.o
 ${PLIST.ocaml-opt}lib/coq/plugins/syntax/string_syntax.cmx
 lib/coq/plugins/syntax/string_syntax_plugin.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/syntax/string_syntax_plugin.cmx
 ${PLIST.natdynlink}lib/coq/plugins/syntax/string_syntax_plugin.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/syntax/string_syntax_plugin.o
 ${PLIST.ocaml-opt}lib/coq/plugins/syntax/z_syntax.cmx
 lib/coq/plugins/syntax/z_syntax_plugin.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/syntax/z_syntax_plugin.cmx
 ${PLIST.natdynlink}lib/coq/plugins/syntax/z_syntax_plugin.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/syntax/z_syntax_plugin.o
 lib/coq/pretyping/arguments_renaming.cmi
@@ -4319,6 +4343,7 @@
 ${PLIST.coqide}share/coq/coq.lang
 ${PLIST.coqide}share/coq/coq.png
 ${PLIST.coqide}share/coq/coq_style.xml
+${PLIST.doc}share/coq/index_urls.txt
 ${PLIST.coqide}share/doc/coq/FAQ-CoqIde
 ${PLIST.doc}share/doc/coq/LICENSE.doc
 ${PLIST.doc}share/doc/coq/html/RecTutorial.html
@@ -5293,6 +5318,5 @@
 share/emacs/site-lisp/gallina-db.el
 share/emacs/site-lisp/gallina-syntax.el
 share/emacs/site-lisp/gallina.el
-share/texmf-dist/tex/latex/coq/coqdoc.sty
 @pkgdir lib/coq/user-contrib
 @pkgdir etc/xdg/coq
diff -r fc95ce879829 -r 5a8280111b7b lang/coq/distinfo
--- a/lang/coq/distinfo Mon Apr 09 11:26:02 2018 +0000
+++ b/lang/coq/distinfo Mon Apr 09 11:29:23 2018 +0000
@@ -1,7 +1,7 @@
-$NetBSD: distinfo,v 1.29 2018/01/10 16:26:53 jaapb Exp $
+$NetBSD: distinfo,v 1.30 2018/04/09 11:29:23 jaapb Exp $
 
-SHA1 (coq-8.7.1.tar.gz) = ea4c4bbed3dc1a5550bbb7e2923ed751f9ad2be6
-RMD160 (coq-8.7.1.tar.gz) = 405d24ba9f0eda5b72e8bd0ed0778390cc444bf0
-SHA512 (coq-8.7.1.tar.gz) = 43ef086de93bf99f94d74b9827dd16c79f4d24f5dd4332ee53bbd4588941cb602a64672638a3b3a56bfb612e4dbf7b2a3b5fd4921182dabbbe96e4fef07455b5
-Size (coq-8.7.1.tar.gz) = 5671130 bytes
+SHA1 (coq-8.7.2.tar.gz) = 0175cc658aa2c93167572a33e9e39fc63f591258
+RMD160 (coq-8.7.2.tar.gz) = 2fd5c59e0143061e4253d68e8839ae3822d7a614
+SHA512 (coq-8.7.2.tar.gz) = 6117ef243c62805996a21952016acaaf21db6d1b539fc813c19c897e100f45cde2bee7c9fb045b269a241b79306c656969ca8051e3212ea2090f6d7c1afad5a8
+Size (coq-8.7.2.tar.gz) = 5754360 bytes
 SHA1 (patch-Makefile.common) = d84cb2a94227e163855f35abebe71f4ec51839fc