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.9.0.



details:   https://anonhg.NetBSD.org/pkgsrc/rev/74ece27807e9
branches:  trunk
changeset: 392846:74ece27807e9
user:      jaapb <jaapb%pkgsrc.org@localhost>
date:      Wed Mar 06 09:28:23 2019 +0000

description:
Updated lang/coq to version 8.9.0.

Many improvements and fixes, but none that appear to break compatibility.
For more details see the CHANGES file.

diffstat:

 lang/coq/Makefile                      |    20 +-
 lang/coq/PLIST                         |  4242 ++++++++++++++++---------------
 lang/coq/distinfo                      |    12 +-
 lang/coq/options.mk                    |    50 +-
 lang/coq/patches/patch-Makefile.common |     8 +-
 5 files changed, 2202 insertions(+), 2130 deletions(-)

diffs (truncated from 5155 to 300 lines):

diff -r 754341cdce02 -r 74ece27807e9 lang/coq/Makefile
--- a/lang/coq/Makefile Wed Mar 06 08:48:49 2019 +0000
+++ b/lang/coq/Makefile Wed Mar 06 09:28:23 2019 +0000
@@ -1,23 +1,22 @@
-# $NetBSD: Makefile,v 1.117 2018/12/09 18:52:33 adam Exp $
+# $NetBSD: Makefile,v 1.118 2019/03/06 09:28:23 jaapb Exp $
 #
 
-DISTNAME=      coq-8.8.1
-PKGREVISION=   5
+DISTNAME=      coq-8.9.0
 CATEGORIES=    lang math
 MASTER_SITES=  ${MASTER_SITE_GITHUB:=coq/}
-GITHUB_TAG=    V${PKGVERSION_NOREV}
+GITHUB_TAG=    V${PKGVERSION_NOREV:S/_/+/}
 
 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}
+WRKSRC=                ${WRKDIR}/${GITHUB_PROJECT}-${PKGVERSION_NOREV:S/_/-/}
 
 USE_TOOLS+=            gmake
 HAS_CONFIGURE=         yes
 CONFIGURE_ARGS+=       -prefix ${PREFIX}
-CONFIGURE_ARGS+=       -emacslib ${PREFIX}/share/emacs/site-lisp
+#CONFIGURE_ARGS+=      -emacslib ${PREFIX}/share/emacs/site-lisp
 CONFIGURE_ARGS+=       -mandir ${PREFIX}/${PKGMANDIR}
 CONFIGURE_ARGS+=       -configdir ${PKG_SYSCONFDIR}/xdg/coq
 CONFIGURE_ARGS+=       -docdir ${PREFIX}/share/doc/coq
@@ -55,14 +54,11 @@
 .include "../../lang/python/pyversion.mk"
 
 REPLACE_SH=    configure install.sh
-REPLACE_INTERPRETER+=  python2 python
+REPLACE_INTERPRETER=   python
 REPLACE.python.old=    python
 REPLACE.python.new=    ${PYTHONBIN}
-REPLACE_FILES.python=  tools/TimeFileMaker.py
-
-REPLACE.python2.old=   python2
-REPLACE.python2.new=   ${PYTHONBIN}
-REPLACE_FILES.python2= tools/make-both-single-timing-files.py \
+REPLACE_FILES.python=  tools/TimeFileMaker.py \
+       tools/make-both-single-timing-files.py \
        tools/make-both-time-files.py \
        tools/make-one-time-file.py
 
diff -r 754341cdce02 -r 74ece27807e9 lang/coq/PLIST
--- a/lang/coq/PLIST    Wed Mar 06 08:48:49 2019 +0000
+++ b/lang/coq/PLIST    Wed Mar 06 09:28:23 2019 +0000
@@ -1,4 +1,4 @@
-@comment $NetBSD: PLIST,v 1.28 2018/08/02 12:57:03 jaapb Exp $
+@comment $NetBSD: PLIST,v 1.29 2019/03/06 09:28:23 jaapb Exp $
 bin/coq-tex
 bin/coq_makefile
 bin/coqc
@@ -6,10 +6,16 @@
 bin/coqdep
 bin/coqdoc
 ${PLIST.coqide}bin/coqide
+${PLIST.coqide}bin/coqidetop
+${PLIST.coqide}bin/coqidetop.opt
+bin/coqpp
+bin/coqproofworker.opt
+bin/coqqueryworker.opt
+bin/coqtacticworker.opt
 bin/coqtop
+bin/coqtop.opt
 bin/coqwc
 bin/coqworkmgr
-bin/gallina
 lib/coq/META
 lib/coq/clib/backtrace.cmi
 ${PLIST.ocaml-opt}lib/coq/clib/backtrace.cmx
@@ -36,10 +42,10 @@
 ${PLIST.ocaml-opt}lib/coq/clib/cThread.cmx
 lib/coq/clib/cUnix.cmi
 ${PLIST.ocaml-opt}lib/coq/clib/cUnix.cmx
-lib/coq/clib/canary.cmi
-${PLIST.ocaml-opt}lib/coq/clib/canary.cmx
 ${PLIST.ocaml-opt}lib/coq/clib/clib.a
 ${PLIST.ocaml-opt}lib/coq/clib/clib.cmxa
+lib/coq/clib/diff2.cmi
+${PLIST.ocaml-opt}lib/coq/clib/diff2.cmx
 lib/coq/clib/dyn.cmi
 ${PLIST.ocaml-opt}lib/coq/clib/dyn.cmx
 lib/coq/clib/exninfo.cmi
@@ -84,10 +90,14 @@
 ${PLIST.ocaml-opt}lib/coq/clib/unionfind.cmx
 lib/coq/config/coq_config.cmi
 ${PLIST.ocaml-opt}lib/coq/config/coq_config.cmx
+lib/coq/coqpp/coqpp_ast.cmi
+lib/coq/coqpp/coqpp_parse.cmi
 lib/coq/engine/eConstr.cmi
 ${PLIST.ocaml-opt}lib/coq/engine/eConstr.cmx
 ${PLIST.ocaml-opt}lib/coq/engine/engine.a
 ${PLIST.ocaml-opt}lib/coq/engine/engine.cmxa
+lib/coq/engine/evar_kinds.cmi
+${PLIST.ocaml-opt}lib/coq/engine/evar_kinds.cmx
 lib/coq/engine/evarutil.cmi
 ${PLIST.ocaml-opt}lib/coq/engine/evarutil.cmx
 lib/coq/engine/evd.cmi
@@ -108,6 +118,16 @@
 ${PLIST.ocaml-opt}lib/coq/engine/termops.cmx
 lib/coq/engine/uState.cmi
 ${PLIST.ocaml-opt}lib/coq/engine/uState.cmx
+lib/coq/engine/univGen.cmi
+${PLIST.ocaml-opt}lib/coq/engine/univGen.cmx
+lib/coq/engine/univMinim.cmi
+${PLIST.ocaml-opt}lib/coq/engine/univMinim.cmx
+lib/coq/engine/univNames.cmi
+${PLIST.ocaml-opt}lib/coq/engine/univNames.cmx
+lib/coq/engine/univProblem.cmi
+${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
@@ -115,6 +135,9 @@
 lib/coq/grammar/grammar.cma
 lib/coq/grammar/q_util.cmi
 ${PLIST.coqide}lib/coq/ide/config_lexer.cmi
+${PLIST.coqide}lib/coq/ide/configwin.cmi
+${PLIST.coqide}lib/coq/ide/configwin_ihm.cmi
+${PLIST.coqide}lib/coq/ide/configwin_messages.cmi
 ${PLIST.coqide}lib/coq/ide/coq.cmi
 ${PLIST.coqide}lib/coq/ide/coqOps.cmi
 ${PLIST.coqide}lib/coq/ide/coq_commands.cmi
@@ -130,15 +153,10 @@
 ${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/richpp.cmi
 ${PLIST.coqide}lib/coq/ide/sentence.cmi
-${PLIST.coqide}lib/coq/ide/serialize.cmi
 ${PLIST.coqide}lib/coq/ide/session.cmi
 ${PLIST.coqide}lib/coq/ide/tags.cmi
 ${PLIST.coqide}lib/coq/ide/utf8_convert.cmi
-${PLIST.coqide}lib/coq/ide/utils/configwin.cmi
-${PLIST.coqide}lib/coq/ide/utils/configwin_ihm.cmi
-${PLIST.coqide}lib/coq/ide/utils/configwin_messages.cmi
 ${PLIST.coqide}lib/coq/ide/wg_Command.cmi
 ${PLIST.coqide}lib/coq/ide/wg_Completion.cmi
 ${PLIST.coqide}lib/coq/ide/wg_Detachable.cmi
@@ -149,10 +167,8 @@
 ${PLIST.coqide}lib/coq/ide/wg_RoutedMessageViews.cmi
 ${PLIST.coqide}lib/coq/ide/wg_ScriptView.cmi
 ${PLIST.coqide}lib/coq/ide/wg_Segment.cmi
-${PLIST.coqide}lib/coq/ide/xml_lexer.cmi
-${PLIST.coqide}lib/coq/ide/xml_parser.cmi
-${PLIST.coqide}lib/coq/ide/xml_printer.cmi
-${PLIST.coqide}lib/coq/ide/xmlprotocol.cmi
+lib/coq/interp/constrexpr.cmi
+${PLIST.ocaml-opt}lib/coq/interp/constrexpr.cmx
 lib/coq/interp/constrexpr_ops.cmi
 ${PLIST.ocaml-opt}lib/coq/interp/constrexpr_ops.cmx
 lib/coq/interp/constrextern.cmi
@@ -167,6 +183,8 @@
 ${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
@@ -179,8 +197,10 @@
 ${PLIST.ocaml-opt}lib/coq/interp/notation.cmx
 lib/coq/interp/notation_ops.cmi
 ${PLIST.ocaml-opt}lib/coq/interp/notation_ops.cmx
-lib/coq/interp/ppextend.cmi
-${PLIST.ocaml-opt}lib/coq/interp/ppextend.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/reserve.cmi
 ${PLIST.ocaml-opt}lib/coq/interp/reserve.cmx
 lib/coq/interp/smartlocate.cmi
@@ -189,34 +209,6 @@
 ${PLIST.ocaml-opt}lib/coq/interp/stdarg.cmx
 lib/coq/interp/syntax_def.cmi
 ${PLIST.ocaml-opt}lib/coq/interp/syntax_def.cmx
-lib/coq/interp/tactypes.cmi
-${PLIST.ocaml-opt}lib/coq/interp/tactypes.cmx
-lib/coq/interp/topconstr.cmi
-${PLIST.ocaml-opt}lib/coq/interp/topconstr.cmx
-lib/coq/intf/constrexpr.cmi
-${PLIST.ocaml-opt}lib/coq/intf/constrexpr.cmx
-lib/coq/intf/decl_kinds.cmi
-${PLIST.ocaml-opt}lib/coq/intf/decl_kinds.cmx
-lib/coq/intf/evar_kinds.cmi
-${PLIST.ocaml-opt}lib/coq/intf/evar_kinds.cmx
-lib/coq/intf/extend.cmi
-${PLIST.ocaml-opt}lib/coq/intf/extend.cmx
-lib/coq/intf/genredexpr.cmi
-${PLIST.ocaml-opt}lib/coq/intf/genredexpr.cmx
-lib/coq/intf/glob_term.cmi
-${PLIST.ocaml-opt}lib/coq/intf/glob_term.cmx
-${PLIST.ocaml-opt}lib/coq/intf/intf.a
-${PLIST.ocaml-opt}lib/coq/intf/intf.cmxa
-lib/coq/intf/locus.cmi
-${PLIST.ocaml-opt}lib/coq/intf/locus.cmx
-lib/coq/intf/misctypes.cmi
-${PLIST.ocaml-opt}lib/coq/intf/misctypes.cmx
-lib/coq/intf/notation_term.cmi
-${PLIST.ocaml-opt}lib/coq/intf/notation_term.cmx
-lib/coq/intf/pattern.cmi
-${PLIST.ocaml-opt}lib/coq/intf/pattern.cmx
-lib/coq/intf/vernacexpr.cmi
-${PLIST.ocaml-opt}lib/coq/intf/vernacexpr.cmx
 lib/coq/kernel/byterun/dllcoqrun.so
 ${PLIST.ocaml-opt}lib/coq/kernel/byterun/libcoqrun.a
 lib/coq/kernel/cClosure.cmi
@@ -285,8 +277,6 @@
 ${PLIST.ocaml-opt}lib/coq/kernel/nativevalues.cmx
 lib/coq/kernel/opaqueproof.cmi
 ${PLIST.ocaml-opt}lib/coq/kernel/opaqueproof.cmx
-lib/coq/kernel/pre_env.cmi
-${PLIST.ocaml-opt}lib/coq/kernel/pre_env.cmx
 lib/coq/kernel/reduction.cmi
 ${PLIST.ocaml-opt}lib/coq/kernel/reduction.cmx
 lib/coq/kernel/retroknowledge.cmi
@@ -355,6 +345,8 @@
 ${PLIST.ocaml-opt}lib/coq/lib/loc.cmx
 lib/coq/lib/pp.cmi
 ${PLIST.ocaml-opt}lib/coq/lib/pp.cmx
+lib/coq/lib/pp_diff.cmi
+${PLIST.ocaml-opt}lib/coq/lib/pp_diff.cmx
 lib/coq/lib/remoteCounter.cmi
 ${PLIST.ocaml-opt}lib/coq/lib/remoteCounter.cmx
 lib/coq/lib/rtree.cmi
@@ -370,6 +362,8 @@
 lib/coq/lib/xml_datatype.cmi
 lib/coq/library/coqlib.cmi
 ${PLIST.ocaml-opt}lib/coq/library/coqlib.cmx
+lib/coq/library/decl_kinds.cmi
+${PLIST.ocaml-opt}lib/coq/library/decl_kinds.cmx
 lib/coq/library/declaremods.cmi
 ${PLIST.ocaml-opt}lib/coq/library/declaremods.cmx
 lib/coq/library/decls.cmi
@@ -382,8 +376,6 @@
 ${PLIST.ocaml-opt}lib/coq/library/globnames.cmx
 lib/coq/library/goptions.cmi
 ${PLIST.ocaml-opt}lib/coq/library/goptions.cmx
-lib/coq/library/heads.cmi
-${PLIST.ocaml-opt}lib/coq/library/heads.cmx
 lib/coq/library/keys.cmi
 ${PLIST.ocaml-opt}lib/coq/library/keys.cmx
 lib/coq/library/kindops.cmi
@@ -408,36 +400,36 @@
 ${PLIST.ocaml-opt}lib/coq/library/summary.cmx
 lib/coq/parsing/cLexer.cmi
 ${PLIST.ocaml-opt}lib/coq/parsing/cLexer.cmx
-lib/coq/parsing/egramcoq.cmi
-${PLIST.ocaml-opt}lib/coq/parsing/egramcoq.cmx
-lib/coq/parsing/egramml.cmi
-${PLIST.ocaml-opt}lib/coq/parsing/egramml.cmx
+lib/coq/parsing/extend.cmi
+${PLIST.ocaml-opt}lib/coq/parsing/extend.cmx
 lib/coq/parsing/g_constr.cmi
 ${PLIST.ocaml-opt}lib/coq/parsing/g_constr.cmx
 lib/coq/parsing/g_prim.cmi
 ${PLIST.ocaml-opt}lib/coq/parsing/g_prim.cmx
-lib/coq/parsing/g_proofs.cmi
-${PLIST.ocaml-opt}lib/coq/parsing/g_proofs.cmx
-lib/coq/parsing/g_vernac.cmi
-${PLIST.ocaml-opt}lib/coq/parsing/g_vernac.cmx
+lib/coq/parsing/notation_gram.cmi
+${PLIST.ocaml-opt}lib/coq/parsing/notation_gram.cmx
+lib/coq/parsing/notgram_ops.cmi
+${PLIST.ocaml-opt}lib/coq/parsing/notgram_ops.cmx
 ${PLIST.ocaml-opt}lib/coq/parsing/parsing.a
 ${PLIST.ocaml-opt}lib/coq/parsing/parsing.cmxa
 lib/coq/parsing/pcoq.cmi
 ${PLIST.ocaml-opt}lib/coq/parsing/pcoq.cmx
+lib/coq/parsing/ppextend.cmi
+${PLIST.ocaml-opt}lib/coq/parsing/ppextend.cmx
 lib/coq/parsing/tok.cmi
 ${PLIST.ocaml-opt}lib/coq/parsing/tok.cmx
-${PLIST.native}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.o
-${PLIST.native}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Btauto.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Btauto.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Btauto.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Btauto.o
-${PLIST.native}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Reflect.cmi
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Reflect.cmx
-${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Reflect.cmxs
-${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Reflect.o
+lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmx
+${PLIST.natdynlink}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmxs
+${PLIST.ocaml-opt}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.o



Home | Main Index | Thread Index | Old Index