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/26d5fd7e834b
branches: trunk
changeset: 330846:26d5fd7e834b
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 7a5c4e54aee6 -r 26d5fd7e834b 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 7a5c4e54aee6 -r 26d5fd7e834b 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