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

To: pkgsrc-changes-hg%NetBSD.org@localhost
Subject: [pkgsrc/trunk]: pkgsrc/lang/coq Updated lang/coq to version 8.7.0.
From: jaapb <jaapb%pkgsrc.org@localhost>
Date: Wed, 15 Jan 2020 08:13:30 +0000
details:   https://anonhg.NetBSD.org/pkgsrc/rev/50bdd3809ee1
branches:  trunk
changeset: 371092:50bdd3809ee1
user:      jaapb <jaapb%pkgsrc.org@localhost>
date:      Fri Nov 03 11:20:28 2017 +0000

description:
Updated lang/coq to version 8.7.0.

Includes many improvements and bugfixes (none that seem to be breaking
backwards compatibility though), see the CHANGELOG.
For packaging:
- camlp4 support removed, package now uses camlp5 exclusively
- fix for PR pkg/52651

diffstat:

 lang/coq/Makefile                      |   22 +-
 lang/coq/PLIST                         |  529 +++++++++++---------------------
 lang/coq/distinfo                      |   13 +-
 lang/coq/patches/patch-Makefile.common |   12 +-
 lang/coq/patches/patch-ide_ideutils.ml |   14 +
 5 files changed, 233 insertions(+), 357 deletions(-)

diffs (truncated from 1140 to 300 lines):

diff -r 6f0798c8d552 -r 50bdd3809ee1 lang/coq/Makefile
--- a/lang/coq/Makefile Fri Nov 03 11:17:21 2017 +0000
+++ b/lang/coq/Makefile Fri Nov 03 11:20:28 2017 +0000
@@ -1,8 +1,7 @@
-# $NetBSD: Makefile,v 1.100 2017/09/18 09:53:24 maya Exp $
+# $NetBSD: Makefile,v 1.101 2017/11/03 11:20:28 jaapb Exp $
 #
 
-DISTNAME=      coq-8.6.1
-PKGREVISION=   1
+DISTNAME=      coq-8.7.0
 CATEGORIES=    lang math
 MASTER_SITES=  http://coq.inria.fr/distrib/V${PKGVERSION_NOREV}/files/
 
@@ -19,7 +18,6 @@
 CONFIGURE_ARGS+=       -configdir ${PKG_SYSCONFDIR}/xdg/coq
 CONFIGURE_ARGS+=       -docdir ${PREFIX}/share/doc/coq
 CONFIGURE_ARGS+=       -coqdocdir ${PREFIX}/share/texmf-dist/tex/latex/coq
-BUILD_TARGET=          world
 
 BUILDLINK_API_DEPENDS.ocaml+=  ocaml>=3.10
 
@@ -32,9 +30,12 @@
 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"
 CONFIGURE_ARGS+=       -native-compiler no
+BUILD_TARGET=  byte
+INSTALL_TARGET=        install-byte
 .endif
 
 .if (${MACHINE_ARCH} == "i386") || (${MACHINE_ARCH} == "x86_64")
@@ -47,7 +48,17 @@
 .  endif
 .endif
 
+.include "../../lang/python/pyversion.mk"
+
 REPLACE_SH=    configure install.sh
+REPLACE_INTERPRETER+=  python
+REPLACE.python.old=    python
+REPLACE.python.new=    ${PYTHONBIN}
+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
+
 INSTALL_ENV+=  COQINSTALLPREFIX=${DESTDIR}
 
 PLIST_VARS+=           coqide natdynlink doc
@@ -63,6 +74,7 @@
 SUBST_FILES.fix-paths= config/coq_config.ml
 SUBST_SED.fix-paths=   -e "s,${BUILDLINK_DIR},${PREFIX},g"
 
-.include "../../lang/camlp4/buildlink3.mk"
+
+.include "../../lang/camlp5/buildlink3.mk"
 .include "../../mk/pthread.buildlink3.mk"
 .include "../../mk/bsd.pkg.mk"
diff -r 6f0798c8d552 -r 50bdd3809ee1 lang/coq/PLIST
--- a/lang/coq/PLIST    Fri Nov 03 11:17:21 2017 +0000
+++ b/lang/coq/PLIST    Fri Nov 03 11:20:28 2017 +0000
@@ -1,4 +1,4 @@
-@comment $NetBSD: PLIST,v 1.21 2017/09/08 17:19:01 jaapb Exp $
+@comment $NetBSD: PLIST,v 1.22 2017/11/03 11:20:28 jaapb Exp $
 bin/coq-tex
 bin/coq_makefile
 bin/coqc
@@ -8,14 +8,13 @@
 ${PLIST.coqide}bin/coqide
 bin/coqmktop
 bin/coqtop
-bin/coqtop.byte
 bin/coqwc
 bin/coqworkmgr
 bin/gallina
 lib/coq/META
-lib/coq/dllcoqrun.so
+lib/coq/config/coq_config.cmi
+lib/coq/engine/eConstr.cmi
 ${PLIST.ocaml-opt}lib/coq/engine/engine.a
-lib/coq/engine/engine.cma
 ${PLIST.ocaml-opt}lib/coq/engine/engine.cmxa
 lib/coq/engine/evarutil.cmi
 lib/coq/engine/evd.cmi
@@ -25,13 +24,12 @@
 lib/coq/engine/namegen.cmi
 lib/coq/engine/proofview.cmi
 lib/coq/engine/proofview_monad.cmi
-lib/coq/engine/sigma.cmi
 lib/coq/engine/termops.cmi
 lib/coq/engine/uState.cmi
+lib/coq/engine/universes.cmi
 lib/coq/config/coq_config.cmi
 lib/coq/grammar/grammar.cma
 lib/coq/grammar/q_util.cmi
-lib/coq/grammar/compat5.cmo
 ${PLIST.coqide}lib/coq/ide/config_lexer.cmi
 ${PLIST.coqide}lib/coq/ide/coq.cmi
 ${PLIST.coqide}lib/coq/ide/coqOps.cmi
@@ -42,28 +40,21 @@
 ${PLIST.coqide}lib/coq/ide/document.cmi
 ${PLIST.coqide}lib/coq/ide/fileOps.cmi
 ${PLIST.coqide}lib/coq/ide/gtk_parsing.cmi
-${PLIST.coqide}lib/coq/ide/ide.a
-${PLIST.coqide}lib/coq/ide/ide.cma
-${PLIST.coqide}lib/coq/ide/ide.cmxa
+${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/minilib.cmi
 ${PLIST.coqide}lib/coq/ide/nanoPG.cmi
 ${PLIST.coqide}lib/coq/ide/preferences.cmi
-${PLIST.coqide}lib/coq/ide/project_file.cmi
-${PLIST.coqide}lib/coq/ide/richprinter.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/serialize.cmi
 ${PLIST.coqide}lib/coq/ide/tags.cmi
 ${PLIST.coqide}lib/coq/ide/utf8_convert.cmi
-${PLIST.coqide}lib/coq/ide/utils/config_file.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_keys.cmi
 ${PLIST.coqide}lib/coq/ide/utils/configwin_messages.cmi
-${PLIST.coqide}lib/coq/ide/utils/configwin_types.cmi
-${PLIST.coqide}lib/coq/ide/utils/editable_cells.cmi
-${PLIST.coqide}lib/coq/ide/utils/okey.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
@@ -73,21 +64,20 @@
 ${PLIST.coqide}lib/coq/ide/wg_ProofView.cmi
 ${PLIST.coqide}lib/coq/ide/wg_ScriptView.cmi
 ${PLIST.coqide}lib/coq/ide/wg_Segment.cmi
-${PLIST.coqide}lib/coq/ide/xmlprotocol.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
-lib/coq/interp/constrarg.cmi
+${PLIST.coqide}lib/coq/ide/xmlprotocol.cmi
 lib/coq/interp/constrexpr_ops.cmi
 lib/coq/interp/constrextern.cmi
 lib/coq/interp/constrintern.cmi
-lib/coq/interp/coqlib.cmi
+lib/coq/interp/declare.cmi
 lib/coq/interp/dumpglob.cmi
 lib/coq/interp/genintern.cmi
+lib/coq/interp/impargs.cmi
 lib/coq/interp/implicit_quantifiers.cmi
-lib/coq/interp/interp.a
-lib/coq/interp/interp.cma
-lib/coq/interp/interp.cmxa
+${PLIST.ocaml-opt}lib/coq/interp/interp.a
+${PLIST.ocaml-opt}lib/coq/interp/interp.cmxa
 lib/coq/interp/modintern.cmi
 lib/coq/interp/notation.cmi
 lib/coq/interp/notation_ops.cmi
@@ -103,12 +93,16 @@
 lib/coq/intf/extend.cmi
 lib/coq/intf/genredexpr.cmi
 lib/coq/intf/glob_term.cmi
+${PLIST.ocaml-opt}lib/coq/intf/intf.a
+${PLIST.ocaml-opt}lib/coq/intf/intf.cmxa
 lib/coq/intf/locus.cmi
 lib/coq/intf/misctypes.cmi
 lib/coq/intf/notation_term.cmi
 lib/coq/intf/pattern.cmi
-lib/coq/intf/tacexpr.cmi
+lib/coq/intf/tactypes.cmi
 lib/coq/intf/vernacexpr.cmi
+lib/coq/kernel/byterun/dllcoqrun.so
+lib/coq/kernel/byterun/libcoqrun.a
 lib/coq/kernel/cClosure.cmi
 lib/coq/kernel/cbytecodes.cmi
 lib/coq/kernel/cbytegen.cmi
@@ -125,12 +119,10 @@
 lib/coq/kernel/environ.cmi
 lib/coq/kernel/esubst.cmi
 lib/coq/kernel/evar.cmi
-lib/coq/kernel/fast_typeops.cmi
 lib/coq/kernel/indtypes.cmi
 lib/coq/kernel/inductive.cmi
-lib/coq/kernel/kernel.a
-lib/coq/kernel/kernel.cma
-lib/coq/kernel/kernel.cmxa
+${PLIST.ocaml-opt}lib/coq/kernel/kernel.a
+${PLIST.ocaml-opt}lib/coq/kernel/kernel.cmxa
 lib/coq/kernel/mod_subst.cmi
 lib/coq/kernel/mod_typing.cmi
 lib/coq/kernel/modops.cmi
@@ -164,6 +156,7 @@
 lib/coq/lib/backtrace.cmi
 lib/coq/lib/bigint.cmi
 lib/coq/lib/cArray.cmi
+lib/coq/lib/cAst.cmi
 lib/coq/lib/cEphemeron.cmi
 lib/coq/lib/cErrors.cmi
 lib/coq/lib/cList.cmi
@@ -177,10 +170,10 @@
 lib/coq/lib/cUnix.cmi
 lib/coq/lib/cWarnings.cmi
 lib/coq/lib/canary.cmi
-lib/coq/lib/clib.a
-lib/coq/lib/clib.cma
-lib/coq/lib/clib.cmxa
+${PLIST.ocaml-opt}lib/coq/lib/clib.a
+${PLIST.ocaml-opt}lib/coq/lib/clib.cmxa
 lib/coq/lib/control.cmi
+lib/coq/lib/coqProject_file.cmi
 lib/coq/lib/deque.cmi
 lib/coq/lib/dyn.cmi
 lib/coq/lib/envars.cmi
@@ -197,20 +190,16 @@
 lib/coq/lib/hook.cmi
 lib/coq/lib/iStream.cmi
 lib/coq/lib/int.cmi
-lib/coq/lib/lib.a
-lib/coq/lib/lib.cma
-lib/coq/lib/lib.cmxa
+${PLIST.ocaml-opt}lib/coq/lib/lib.a
+${PLIST.ocaml-opt}lib/coq/lib/lib.cmxa
 lib/coq/lib/loc.cmi
 lib/coq/lib/minisys.cmi
 lib/coq/lib/monad.cmi
 lib/coq/lib/option.cmi
 lib/coq/lib/pp.cmi
-lib/coq/lib/pp_control.cmi
-lib/coq/lib/ppstyle.cmi
 lib/coq/lib/predicate.cmi
 lib/coq/lib/profile.cmi
 lib/coq/lib/remoteCounter.cmi
-lib/coq/lib/richpp.cmi
 lib/coq/lib/rtree.cmi
 lib/coq/lib/segmenttree.cmi
 lib/coq/lib/spawn.cmi
@@ -224,8 +213,7 @@
 lib/coq/lib/unionfind.cmi
 lib/coq/lib/util.cmi
 lib/coq/lib/xml_datatype.cmi
-lib/coq/libcoqrun.a
-lib/coq/library/declare.cmi
+lib/coq/library/coqlib.cmi
 lib/coq/library/declaremods.cmi
 lib/coq/library/decls.cmi
 lib/coq/library/dischargedhypsmap.cmi
@@ -233,62 +221,31 @@
 lib/coq/library/globnames.cmi
 lib/coq/library/goptions.cmi
 lib/coq/library/heads.cmi
-lib/coq/library/impargs.cmi
 lib/coq/library/keys.cmi
 lib/coq/library/kindops.cmi
 lib/coq/library/lib.cmi
 lib/coq/library/libnames.cmi
 lib/coq/library/libobject.cmi
-lib/coq/library/library.a
-lib/coq/library/library.cma
+${PLIST.ocaml-opt}lib/coq/library/library.a
 lib/coq/library/library.cmi
-lib/coq/library/library.cmxa
+${PLIST.ocaml-opt}lib/coq/library/library.cmxa
 lib/coq/library/loadpath.cmi
 lib/coq/library/nameops.cmi
 lib/coq/library/nametab.cmi
 lib/coq/library/states.cmi
 lib/coq/library/summary.cmi
-lib/coq/library/universes.cmi
-lib/coq/ltac/coretactics.cmi
-lib/coq/ltac/evar_tactics.cmi
-lib/coq/ltac/extraargs.cmi
-lib/coq/ltac/extratactics.cmi
-lib/coq/ltac/g_auto.cmi
-lib/coq/ltac/g_class.cmi
-lib/coq/ltac/g_eqdecide.cmi
-lib/coq/ltac/g_ltac.cmi
-lib/coq/ltac/g_obligations.cmi
-lib/coq/ltac/g_rewrite.cmi
-${PLIST.ocaml-opt}lib/coq/ltac/ltac.a
-lib/coq/ltac/ltac.cma
-${PLIST.ocaml-opt}lib/coq/ltac/ltac.cmxa
-lib/coq/ltac/profile_ltac.cmi
-lib/coq/ltac/profile_ltac_tactics.cmi
-lib/coq/ltac/rewrite.cmi
-lib/coq/ltac/taccoerce.cmi
-lib/coq/ltac/tacentries.cmi
-lib/coq/ltac/tacenv.cmi
-lib/coq/ltac/tacintern.cmi
-lib/coq/ltac/tacinterp.cmi
-lib/coq/ltac/tacsubst.cmi
-lib/coq/ltac/tactic_debug.cmi
-lib/coq/ltac/tactic_option.cmi
-lib/coq/ltac/tauto.cmi
+lib/coq/library/univops.cmi
 lib/coq/parsing/cLexer.cmi
Prev by Date: [pkgsrc/trunk]: pkgsrc/www/py-websockets py-websockets: updated to 4.0.1
Next by Date: [pkgsrc/trunk]: pkgsrc/databases/py-sqlalchemy-utils py-sqlalchemy-utils: upd...
Previous by Thread: [pkgsrc/trunk]: pkgsrc/www/py-websockets py-websockets: updated to 4.0.1
Next by Thread: [pkgsrc/trunk]: pkgsrc/databases/py-sqlalchemy-utils py-sqlalchemy-utils: upd...
Indexes:
Home | Main Index | Thread Index | Old Index