diff options
author | jaapb <jaapb@pkgsrc.org> | 2018-04-09 11:29:23 +0000 |
---|---|---|
committer | jaapb <jaapb@pkgsrc.org> | 2018-04-09 11:29:23 +0000 |
commit | b6abaac6d05d00d70e8214118561fbfa704f2631 (patch) | |
tree | 8e5af044e1a9f43d58e6dc0799682a4aa13c70e0 /lang/coq | |
parent | 486e62655d680f291d322c842dee8d49edfb76ca (diff) | |
download | pkgsrc-b6abaac6d05d00d70e8214118561fbfa704f2631.tar.gz |
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 (limited to 'lang/coq')
-rw-r--r-- | lang/coq/Makefile | 10 | ||||
-rw-r--r-- | lang/coq/PLIST | 28 | ||||
-rw-r--r-- | lang/coq/distinfo | 10 |
3 files changed, 37 insertions, 11 deletions
diff --git a/lang/coq/Makefile b/lang/coq/Makefile index 6cffec3f659..2f77ce0d9bd 100644 --- a/lang/coq/Makefile +++ b/lang/coq/Makefile @@ -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 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 --git a/lang/coq/PLIST b/lang/coq/PLIST index 814dee5bf4c..167fa50fbc0 100644 --- a/lang/coq/PLIST +++ b/lang/coq/PLIST @@ -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.glob 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.vo 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 @@ ${PLIST.ocaml-opt}lib/coq/plugins/extraction/extract_env.cmx 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 @@ ${PLIST.ocaml-opt}lib/coq/plugins/firstorder/g_ground.cmx 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 @@ lib/coq/plugins/fourier/Fourier_util.vo ${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 @@ ${PLIST.ocaml-opt}lib/coq/plugins/funind/merge.cmx 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_obligations.cmx ${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 @@ ${PLIST.ocaml-opt}lib/coq/plugins/ltac/tactic_option.cmx 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 @@ ${PLIST.ocaml-opt}lib/coq/plugins/micromega/mfourier.cmx 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 @@ ${PLIST.ocaml-opt}lib/coq/plugins/nsatz/ideal.cmx 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/coq_omega.cmx ${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 @@ lib/coq/plugins/quote/Quote.vo ${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/const_omega.cmx ${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 @@ ${PLIST.ocaml-opt}lib/coq/plugins/rtauto/proof_search.cmx 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 @@ lib/coq/plugins/setoid_ring/newring.cmi ${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.glob 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.glob 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-ssreflect.lang ${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/coq-inferior.el 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 --git a/lang/coq/distinfo b/lang/coq/distinfo index 30d3feec67e..66bea3a9a3b 100644 --- a/lang/coq/distinfo +++ b/lang/coq/distinfo @@ -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 |