pkgsrc-Changes-HG archive

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index][Old Index]

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



details:   https://anonhg.NetBSD.org/pkgsrc/rev/840b20fef660
branches:  trunk
changeset: 422335:840b20fef660
user:      jaapb <jaapb%pkgsrc.org@localhost>
date:      Fri Jan 24 15:54:48 2020 +0000

description:
Updated lang/coq to version 8.10.2.

Changes include:
- native 63-bit machine integers;
- a new sort of definitionally proof-irrelevant propositons: SProp;
- private universes for opaque polymorphic constants;
- string notations and numeral notations;
- a new simplex-based proof engine for the tactics lia, nia, lra and nra;
- new introduction patterns for SSReflect;
- a tactic to rewrite under binders: under;
- easy input of non-ASCII symbols in CoqIDE, which now uses GTK3.

and many small improvements and bugfixes.

diffstat:

 lang/coq/Makefile                      |   18 +-
 lang/coq/PLIST                         |  235 +++++++++++++++++++++-----------
 lang/coq/distinfo                      |   13 +-
 lang/coq/options.mk                    |    7 +-
 lang/coq/patches/patch-Makefile.build  |   15 --
 lang/coq/patches/patch-Makefile.common |    3 +-
 6 files changed, 175 insertions(+), 116 deletions(-)

diffs (truncated from 735 to 300 lines):

diff -r 6ee43a545959 -r 840b20fef660 lang/coq/Makefile
--- a/lang/coq/Makefile Fri Jan 24 15:36:39 2020 +0000
+++ b/lang/coq/Makefile Fri Jan 24 15:54:48 2020 +0000
@@ -1,18 +1,17 @@
-# $NetBSD: Makefile,v 1.127 2020/01/18 21:49:42 jperkin Exp $
+# $NetBSD: Makefile,v 1.128 2020/01/24 15:54:48 jaapb Exp $
 #
 
-DISTNAME=      coq-8.9.1
-PKGREVISION=   4
+DISTNAME=      coq-8.10.2
 CATEGORIES=    lang math
 MASTER_SITES=  ${MASTER_SITE_GITHUB:=coq/}
 GITHUB_TAG=    V${PKGVERSION_NOREV:S/_/+/}
 
 MAINTAINER=    jaapb%NetBSD.org@localhost
-HOMEPAGE=      http://coq.inria.fr/
+HOMEPAGE=      https://coq.inria.fr/
 COMMENT=       Theorem prover which extracts programs from proofs
 LICENSE=       gnu-lgpl-v2.1
 
-WRKSRC=                ${WRKDIR}/${GITHUB_PROJECT}-${PKGVERSION_NOREV:S/_/-/}
+WRKSRC=                ${WRKDIR}/${GITHUB_PROJECT}-${PKGVERSION_NOREV:S/+/-/}
 
 USE_TOOLS+=            gmake
 HAS_CONFIGURE=         yes
@@ -22,6 +21,7 @@
 CONFIGURE_ARGS+=       -configdir ${PKG_SYSCONFDIR}/xdg/coq
 CONFIGURE_ARGS+=       -docdir ${PREFIX}/share/doc/coq
 CONFIGURE_ARGS+=       -coqdocdir ${PREFIX}/share/texmf-dist/tex/latex/coq
+CONFIGURE_ARGS+=       -flambda-opts '-O3 -unbox-closures'
 
 BUILDLINK_API_DEPENDS.ocaml+=  ocaml>=3.10
 
@@ -30,17 +30,18 @@
 
 PLIST_VARS+=           native
 .if ${OCAML_USE_OPT_COMPILER} == "yes"
-PLIST_SUBST+=          COQIDE_TYPE="opt"
+COQIDE_TYPE=           opt
 PLIST.native=          yes
 CONFIGURE_ARGS+=       -native-compiler yes
 UNLIMIT_RESOURCES+=    stacksize # compilation of some files needs this
 BUILD_TARGET=          world
 .else
-PLIST_SUBST+=          COQIDE_TYPE="byte"
+COQIDE_TYPE=           byte
 CONFIGURE_ARGS+=       -native-compiler no
 BUILD_TARGET=          byte
 INSTALL_TARGET=                install-byte
 .endif
+PLIST_SUBST+=          COQIDE_TYPE=${COQIDE_TYPE}
 
 .if (${MACHINE_ARCH} == "i386") || (${MACHINE_ARCH} == "x86_64")
 .  if !empty(MACHINE_PLATFORM:MLinux-*-*) || \
@@ -56,7 +57,7 @@
 
 REPLACE_SH=            configure install.sh
 REPLACE_INTERPRETER=   python
-REPLACE.python.old=    python
+REPLACE.python.old=    python3
 REPLACE.python.new=    ${PYTHONBIN}
 REPLACE_FILES.python=  tools/TimeFileMaker.py \
                        tools/make-both-single-timing-files.py \
@@ -78,7 +79,6 @@
 SUBST_FILES.fix-paths=         config/coq_config.ml
 SUBST_SED.fix-paths=           -e "s,${BUILDLINK_DIR},${PREFIX},g"
 
-.include "../../lang/camlp5/buildlink3.mk"
 .include "../../math/ocaml-num/buildlink3.mk"
 .include "../../mk/pthread.buildlink3.mk"
 .include "../../mk/bsd.pkg.mk"
diff -r 6ee43a545959 -r 840b20fef660 lang/coq/PLIST
--- a/lang/coq/PLIST    Fri Jan 24 15:36:39 2020 +0000
+++ b/lang/coq/PLIST    Fri Jan 24 15:54:48 2020 +0000
@@ -1,4 +1,4 @@
-@comment $NetBSD: PLIST,v 1.29 2019/03/06 09:28:23 jaapb Exp $
+@comment $NetBSD: PLIST,v 1.30 2020/01/24 15:54:48 jaapb Exp $
 bin/coq-tex
 bin/coq_makefile
 bin/coqc
@@ -88,6 +88,8 @@
 ${PLIST.ocaml-opt}lib/coq/clib/unicodetable.cmx
 lib/coq/clib/unionfind.cmi
 ${PLIST.ocaml-opt}lib/coq/clib/unionfind.cmx
+${PLIST.ocaml-opt}lib/coq/config/config.a
+${PLIST.ocaml-opt}lib/coq/config/config.cmxa
 lib/coq/config/coq_config.cmi
 ${PLIST.ocaml-opt}lib/coq/config/coq_config.cmx
 lib/coq/coqpp/coqpp_ast.cmi
@@ -128,12 +130,20 @@
 ${PLIST.ocaml-opt}lib/coq/engine/univProblem.cmx
 lib/coq/engine/univSubst.cmi
 ${PLIST.ocaml-opt}lib/coq/engine/univSubst.cmx
-lib/coq/engine/universes.cmi
-${PLIST.ocaml-opt}lib/coq/engine/universes.cmx
 lib/coq/engine/univops.cmi
 ${PLIST.ocaml-opt}lib/coq/engine/univops.cmx
-lib/coq/grammar/grammar.cma
-lib/coq/grammar/q_util.cmi
+${PLIST.ocaml-opt}lib/coq/gramlib/.pack/gramlib.a
+lib/coq/gramlib/.pack/gramlib.cmi
+${PLIST.ocaml-opt}lib/coq/gramlib/.pack/gramlib.cmx
+${PLIST.ocaml-opt}lib/coq/gramlib/.pack/gramlib.cmxa
+lib/coq/gramlib/.pack/gramlib__Gramext.cmi
+${PLIST.ocaml-opt}lib/coq/gramlib/.pack/gramlib__Gramext.cmx
+lib/coq/gramlib/.pack/gramlib__Grammar.cmi
+${PLIST.ocaml-opt}lib/coq/gramlib/.pack/gramlib__Grammar.cmx
+lib/coq/gramlib/.pack/gramlib__Plexing.cmi
+${PLIST.ocaml-opt}lib/coq/gramlib/.pack/gramlib__Plexing.cmx
+lib/coq/gramlib/.pack/gramlib__Ploc.cmi
+${PLIST.ocaml-opt}lib/coq/gramlib/.pack/gramlib__Ploc.cmx
 ${PLIST.coqide}lib/coq/ide/config_lexer.cmi
 ${PLIST.coqide}lib/coq/ide/configwin.cmi
 ${PLIST.coqide}lib/coq/ide/configwin_ihm.cmi
@@ -150,12 +160,13 @@
 ${PLIST.coqide}${PLIST.ocaml-opt}lib/coq/ide/ide.a
 ${PLIST.coqide}${PLIST.ocaml-opt}lib/coq/ide/ide.cmxa
 ${PLIST.coqide}lib/coq/ide/ideutils.cmi
+${PLIST.coqide}lib/coq/ide/microPG.cmi
 ${PLIST.coqide}lib/coq/ide/minilib.cmi
-${PLIST.coqide}lib/coq/ide/nanoPG.cmi
 ${PLIST.coqide}lib/coq/ide/preferences.cmi
 ${PLIST.coqide}lib/coq/ide/sentence.cmi
 ${PLIST.coqide}lib/coq/ide/session.cmi
 ${PLIST.coqide}lib/coq/ide/tags.cmi
+${PLIST.coqide}lib/coq/ide/unicode_bindings.cmi
 ${PLIST.coqide}lib/coq/ide/utf8_convert.cmi
 ${PLIST.coqide}lib/coq/ide/wg_Command.cmi
 ${PLIST.coqide}lib/coq/ide/wg_Completion.cmi
@@ -183,8 +194,6 @@
 ${PLIST.ocaml-opt}lib/coq/interp/dumpglob.cmx
 lib/coq/interp/genintern.cmi
 ${PLIST.ocaml-opt}lib/coq/interp/genintern.cmx
-lib/coq/interp/genredexpr.cmi
-${PLIST.ocaml-opt}lib/coq/interp/genredexpr.cmx
 lib/coq/interp/impargs.cmi
 ${PLIST.ocaml-opt}lib/coq/interp/impargs.cmx
 lib/coq/interp/implicit_quantifiers.cmi
@@ -199,8 +208,8 @@
 ${PLIST.ocaml-opt}lib/coq/interp/notation_ops.cmx
 lib/coq/interp/notation_term.cmi
 ${PLIST.ocaml-opt}lib/coq/interp/notation_term.cmx
-lib/coq/interp/redops.cmi
-${PLIST.ocaml-opt}lib/coq/interp/redops.cmx
+lib/coq/interp/numTok.cmi
+${PLIST.ocaml-opt}lib/coq/interp/numTok.cmx
 lib/coq/interp/reserve.cmi
 ${PLIST.ocaml-opt}lib/coq/interp/reserve.cmx
 lib/coq/interp/smartlocate.cmi
@@ -221,7 +230,6 @@
 ${PLIST.ocaml-opt}lib/coq/kernel/cbytegen.cmx
 lib/coq/kernel/cemitcodes.cmi
 ${PLIST.ocaml-opt}lib/coq/kernel/cemitcodes.cmx
-lib/coq/kernel/cinstr.cmi
 lib/coq/kernel/clambda.cmi
 ${PLIST.ocaml-opt}lib/coq/kernel/clambda.cmx
 lib/coq/kernel/constr.cmi
@@ -248,6 +256,8 @@
 ${PLIST.ocaml-opt}lib/coq/kernel/esubst.cmx
 lib/coq/kernel/evar.cmi
 ${PLIST.ocaml-opt}lib/coq/kernel/evar.cmx
+lib/coq/kernel/indTyping.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/indTyping.cmx
 lib/coq/kernel/indtypes.cmi
 ${PLIST.ocaml-opt}lib/coq/kernel/indtypes.cmx
 lib/coq/kernel/inductive.cmi
@@ -266,7 +276,6 @@
 ${PLIST.ocaml-opt}lib/coq/kernel/nativecode.cmx
 lib/coq/kernel/nativeconv.cmi
 ${PLIST.ocaml-opt}lib/coq/kernel/nativeconv.cmx
-lib/coq/kernel/nativeinstr.cmi
 lib/coq/kernel/nativelambda.cmi
 ${PLIST.ocaml-opt}lib/coq/kernel/nativelambda.cmx
 lib/coq/kernel/nativelib.cmi
@@ -277,10 +286,14 @@
 ${PLIST.ocaml-opt}lib/coq/kernel/nativevalues.cmx
 lib/coq/kernel/opaqueproof.cmi
 ${PLIST.ocaml-opt}lib/coq/kernel/opaqueproof.cmx
+lib/coq/kernel/primred.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/primred.cmx
 lib/coq/kernel/reduction.cmi
 ${PLIST.ocaml-opt}lib/coq/kernel/reduction.cmx
 lib/coq/kernel/retroknowledge.cmi
 ${PLIST.ocaml-opt}lib/coq/kernel/retroknowledge.cmx
+lib/coq/kernel/retypeops.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/retypeops.cmx
 lib/coq/kernel/safe_typing.cmi
 ${PLIST.ocaml-opt}lib/coq/kernel/safe_typing.cmx
 lib/coq/kernel/sorts.cmi
@@ -291,14 +304,16 @@
 ${PLIST.ocaml-opt}lib/coq/kernel/term.cmx
 lib/coq/kernel/term_typing.cmi
 ${PLIST.ocaml-opt}lib/coq/kernel/term_typing.cmx
+lib/coq/kernel/transparentState.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/transparentState.cmx
 lib/coq/kernel/type_errors.cmi
 ${PLIST.ocaml-opt}lib/coq/kernel/type_errors.cmx
 lib/coq/kernel/typeops.cmi
 ${PLIST.ocaml-opt}lib/coq/kernel/typeops.cmx
 lib/coq/kernel/uGraph.cmi
 ${PLIST.ocaml-opt}lib/coq/kernel/uGraph.cmx
-lib/coq/kernel/uint31.cmi
-${PLIST.ocaml-opt}lib/coq/kernel/uint31.cmx
+lib/coq/kernel/uint63.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/uint63.cmx
 lib/coq/kernel/univ.cmi
 ${PLIST.ocaml-opt}lib/coq/kernel/univ.cmx
 lib/coq/kernel/vars.cmi
@@ -309,6 +324,8 @@
 ${PLIST.ocaml-opt}lib/coq/kernel/vm.cmx
 lib/coq/kernel/vmvalues.cmi
 ${PLIST.ocaml-opt}lib/coq/kernel/vmvalues.cmx
+lib/coq/lib/acyclicGraph.cmi
+${PLIST.ocaml-opt}lib/coq/lib/acyclicGraph.cmx
 lib/coq/lib/aux_file.cmi
 ${PLIST.ocaml-opt}lib/coq/lib/aux_file.cmx
 lib/coq/lib/cAst.cmi
@@ -368,8 +385,6 @@
 ${PLIST.ocaml-opt}lib/coq/library/declaremods.cmx
 lib/coq/library/decls.cmi
 ${PLIST.ocaml-opt}lib/coq/library/decls.cmx
-lib/coq/library/dischargedhypsmap.cmi
-${PLIST.ocaml-opt}lib/coq/library/dischargedhypsmap.cmx
 lib/coq/library/global.cmi
 ${PLIST.ocaml-opt}lib/coq/library/global.cmx
 lib/coq/library/globnames.cmi
@@ -444,6 +459,7 @@
 ${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
+lib/coq/plugins/btauto/refl_btauto.cmi
 ${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
@@ -502,6 +518,10 @@
 ${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmx
 ${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.o
+lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmx
+${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmxs
+${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.o
 lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmx
 ${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmxs
@@ -562,6 +582,9 @@
 lib/coq/plugins/extraction/ExtrHaskellZNum.glob
 lib/coq/plugins/extraction/ExtrHaskellZNum.v
 lib/coq/plugins/extraction/ExtrHaskellZNum.vo
+lib/coq/plugins/extraction/ExtrOCamlInt63.glob
+lib/coq/plugins/extraction/ExtrOCamlInt63.v
+lib/coq/plugins/extraction/ExtrOCamlInt63.vo
 lib/coq/plugins/extraction/ExtrOcamlBasic.glob
 lib/coq/plugins/extraction/ExtrOcamlBasic.v
 lib/coq/plugins/extraction/ExtrOcamlBasic.vo
@@ -730,6 +753,10 @@
 ${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
+lib/coq/plugins/micromega/.coq-native/NCoq_micromega_DeclConstant.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_DeclConstant.cmx
+${PLIST.natdynlink}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_DeclConstant.cmxs
+${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_DeclConstant.o
 lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmx
 ${PLIST.natdynlink}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmxs
@@ -802,6 +829,9 @@
 ${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_ZMicromega.cmx
 ${PLIST.natdynlink}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_ZMicromega.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_ZMicromega.o
+lib/coq/plugins/micromega/DeclConstant.glob
+lib/coq/plugins/micromega/DeclConstant.v
+lib/coq/plugins/micromega/DeclConstant.vo
 lib/coq/plugins/micromega/Env.glob
 lib/coq/plugins/micromega/Env.v
 lib/coq/plugins/micromega/Env.vo
@@ -865,6 +895,8 @@
 ${PLIST.ocaml-opt}lib/coq/plugins/micromega/csdpcert.cmx
 lib/coq/plugins/micromega/g_micromega.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/micromega/g_micromega.cmx
+lib/coq/plugins/micromega/itv.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/micromega/itv.cmx
 lib/coq/plugins/micromega/mfourier.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/micromega/mfourier.cmx
 lib/coq/plugins/micromega/micromega.cmi
@@ -879,12 +911,16 @@
 ${PLIST.ocaml-opt}lib/coq/plugins/micromega/persistent_cache.cmx
 lib/coq/plugins/micromega/polynomial.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/micromega/polynomial.cmx
+lib/coq/plugins/micromega/simplex.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/micromega/simplex.cmx
 lib/coq/plugins/micromega/sos.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/micromega/sos.cmx
 lib/coq/plugins/micromega/sos_lib.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/micromega/sos_lib.cmx
 lib/coq/plugins/micromega/sos_types.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/micromega/sos_types.cmx
+lib/coq/plugins/micromega/vect.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/micromega/vect.cmx



Home | Main Index | Thread Index | Old Index