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/1a543d8c1378
branches: trunk
changeset: 410559:1a543d8c1378
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 93fcf3453164 -r 1a543d8c1378 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 93fcf3453164 -r 1a543d8c1378 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