[pkgsrc/trunk]: pkgsrc/lang/coq Updated package to latest version, 8.5pl1. Al...

[jaapb <jaapb%pkgsrc.org@localhost>]

details:   https://anonhg.NetBSD.org/pkgsrc/rev/16ffaeccca42
branches:  trunk
changeset: 349207:16ffaeccca42
user:      jaapb <jaapb%pkgsrc.org@localhost>
date:      Sat Jul 02 10:17:18 2016 +0000

description:
Updated package to latest version, 8.5pl1. Also fixed a packaging bug
that had buildlink paths show up in the Coq_config module, and added a
patch from upstream to allow compilation with 4.03.

Changes:
Critical bugfix
- The subterm relation for the guard condition was incorrectly defined on
  primitive projections (#4588)

Plugin development tools
- add a .merlin target to the makefile

Various performance improvements (time, space used by .vo files)

Other bugfixes

- Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.v
- Added compatibility coercions from Specif.v which were present in Coq 8.4.
- Fixing a source of inefficiency and an artificial dependency in the printer in the congruence tactic.
- Allow to unset the refinement mode of Instance in ML
- Fixing an incorrect use of prod_appvect on a term which was not a product in setoid_rewrite.
- Add -compat 8.4 econstructor tactics, and tests
- Add compatibility Nonrecursive Elimination Schemes
- Fixing the "No applicable tactic" non informative error message regression on apply.
- Univs: fix get_current_context (bug #4603, part I)
- Fix a bug in Program coercion code
- Fix handling of arity of definitional classes.
- #4630: Some tactics are 20x slower in 8.5 than 8.4.
- #4627: records with no declared arity can be template polymorphic.
- #4623: set tactic too weak with universes (regression)
- Fix incorrect behavior of CS resolution
- #4591: Uncaught exception in directory browsing.
- CoqIDE is more resilient to initialization errors.
- #4614: "Fully check the document" is uninterruptable.
- Try eta-expansion of records only on non-recursive ones
- Fix bug when a sort is ascribed to a Record
- Primitive projections: protect kernel from erroneous definitions.
- Fixed bug #4533 with previous Keyed Unification commit
- Win: kill unreliable hence do not waitpid after kill -9 (Close #4369)
- Fix strategy of Keyed Unification
- #4608: Anomaly "output_value: abstract value (outside heap)".
- #4607: do not read native code files if native compiler was disabled.
- #4105: poor escaping in the protocol between CoqIDE and coqtop.
- #4596: [rewrite] broke in the past few weeks.
- #4533 (partial): respect declared global transparency of projections in unification.ml
- #4544: Backtrack on using full betaiota reduction during keyed unification.
- #4540: CoqIDE bottom progress bar does not update.
- Fix regression from 8.4 in reflexivity
- #4580: [Set Refine Instance Mode] also used for Program Instance.
- #4582: cannot override notation [ x ]. MAY CREATE INCOMPATIBILITIES, see #4683.
- STM: Print/Extraction have to be skipped if -quick
- #4542: CoqIDE: STOP button also stops workers
- STM: classify some variants of Instance as regular `Fork nodes.
- #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity").
- Do not give a name to anonymous evars anymore. See bug #4547.
- STM: always stock in vio files the first node (state) of a proof
- STM: not delegate proofs that contain Vernac(Module|Require|Import), #4530
- Don't fail fatally if PATH is not set.
- #4537: Coq 8.5 is slower in typeclass resolution.
- #4522: Incorrect "Warning..." on windows.
- #4373: coqdep does not know about .vio files.
- #3826: "Incompatible module types" is uninformative.
- #4495: Failed assertion in metasyntax.ml.
- #4511: evar tactic can create non-typed evars.
- #4503: mixing universe polymorphic and monomorphic variables and definitions in sections is unsupported.
- #4519: oops, global shadowed local universe level bindings.
- #4506: Anomaly: File "pretyping/indrec.ml", line 169, characters 14-20: Assertion failed.
- #4548: Coqide crashes when going back one command

diffstat:

 lang/coq/Makefile                      |  11 ++++++++---
 lang/coq/PLIST                         |   4 ++--
 lang/coq/distinfo                      |  12 ++++++------
 lang/coq/patches/patch-Makefile.common |  14 ++++++++++++--
 4 files changed, 28 insertions(+), 13 deletions(-)

diffs (98 lines):

diff -r e1da3e969641 -r 16ffaeccca42 lang/coq/Makefile
--- a/lang/coq/Makefile Sat Jul 02 10:11:24 2016 +0000
+++ b/lang/coq/Makefile Sat Jul 02 10:17:18 2016 +0000
@@ -1,8 +1,7 @@
-# $NetBSD: Makefile,v 1.89 2016/05/05 11:45:40 jaapb Exp $
+# $NetBSD: Makefile,v 1.90 2016/07/02 10:17:18 jaapb Exp $
 #
 
-DISTNAME=      coq-8.5
-PKGREVISION=   4
+DISTNAME=      coq-8.5pl1
 CATEGORIES=    lang math
 MASTER_SITES=  http://coq.inria.fr/distrib/V${PKGVERSION_NOREV}/files/
 
@@ -52,6 +51,12 @@
 EGDIR=         ${PREFIX}/share/coq/examples
 #CONF_FILES=   {EGDIR}/coqide-gtk2rc ${PKG_SYSCONFDIR}/xdg/coq/coqide-gtk2rc
 
+SUBST_CLASSES+=        fix-paths
+SUBST_STAGE.fix-paths= post-configure
+SUBST_MESSAGE.fix-paths=       Remove buildlink references from Coq_config module
+SUBST_FILES.fix-paths= config/coq_config.ml
+SUBST_SED.fix-paths=   -e "s,${BUILDLINK_DIR},${PREFIX},g"
+
 .include "../../mk/pthread.buildlink3.mk"
 .include "../../lang/camlp5/buildlink3.mk"
 .include "../../mk/bsd.pkg.mk"
diff -r e1da3e969641 -r 16ffaeccca42 lang/coq/PLIST
--- a/lang/coq/PLIST    Sat Jul 02 10:11:24 2016 +0000
+++ b/lang/coq/PLIST    Sat Jul 02 10:17:18 2016 +0000
@@ -1,4 +1,4 @@
-@comment $NetBSD: PLIST,v 1.18 2016/02/06 16:08:36 jaapb Exp $
+@comment $NetBSD: PLIST,v 1.19 2016/07/02 10:17:18 jaapb Exp $
 bin/coq-tex
 bin/coq_makefile
 bin/coqc
@@ -142,6 +142,7 @@
 lib/coq/lib/backtrace.cmi
 lib/coq/lib/bigint.cmi
 lib/coq/lib/cArray.cmi
+lib/coq/lib/cEphemeron.cmi
 lib/coq/lib/cList.cmi
 lib/coq/lib/cMap.cmi
 lib/coq/lib/cObj.cmi
@@ -159,7 +160,6 @@
 lib/coq/lib/deque.cmi
 lib/coq/lib/dyn.cmi
 lib/coq/lib/envars.cmi
-lib/coq/lib/ephemeron.cmi
 lib/coq/lib/errors.cmi
 lib/coq/lib/exninfo.cmi
 lib/coq/lib/explore.cmi
diff -r e1da3e969641 -r 16ffaeccca42 lang/coq/distinfo
--- a/lang/coq/distinfo Sat Jul 02 10:11:24 2016 +0000
+++ b/lang/coq/distinfo Sat Jul 02 10:17:18 2016 +0000
@@ -1,9 +1,9 @@
-$NetBSD: distinfo,v 1.24 2016/02/06 16:08:36 jaapb Exp $
+$NetBSD: distinfo,v 1.25 2016/07/02 10:17:18 jaapb Exp $
 
-SHA1 (coq-8.5.tar.gz) = 0a0d124b1869d7e20cfcf3f71f086488c146f883
-RMD160 (coq-8.5.tar.gz) = 551d35ac96436d98112fa1a17bcc075ee307c627
-SHA512 (coq-8.5.tar.gz) = 28835a9dc4c926f97b14d23fe746e45e17942003e29807ec59f301eb0b697d704f05afc4cccd31b83bc27e9877d079d00e94a2101ba16ae32f4134e90ad011fb
-Size (coq-8.5.tar.gz) = 5346653 bytes
+SHA1 (coq-8.5pl1.tar.gz) = 92722ffc2be6948e0074b211bb556ad4b911ebd6
+RMD160 (coq-8.5pl1.tar.gz) = 04c540ab1033fd6b0e4c121b73ed56557708e7a5
+SHA512 (coq-8.5pl1.tar.gz) = c9a5bba1abc3b2216cb43595230387751277412988b44af1555ffccdc109a9eef69422867e0062d92dfc73ffcbbe24f53ff583224c28cae3f9bda1ae21dd547b
+Size (coq-8.5pl1.tar.gz) = 5366774 bytes
 SHA1 (patch-Makefile.build) = 1b711ef9490a07c9d02b5a8ca9a38c252e322b4f
-SHA1 (patch-Makefile.common) = 67131e197d25a087d845dfa6fa93729f0b2eaa00
+SHA1 (patch-Makefile.common) = f53dd334d3e14a0e0c3ef91bac9a6c1745cbb591
 SHA1 (patch-configure.ml) = 6e2f44091216348a12131592bf29f0f7fd93a4fe
diff -r e1da3e969641 -r 16ffaeccca42 lang/coq/patches/patch-Makefile.common
--- a/lang/coq/patches/patch-Makefile.common    Sat Jul 02 10:11:24 2016 +0000
+++ b/lang/coq/patches/patch-Makefile.common    Sat Jul 02 10:17:18 2016 +0000
@@ -1,7 +1,8 @@
-$NetBSD: patch-Makefile.common,v 1.1 2016/02/06 16:08:36 jaapb Exp $
+$NetBSD: patch-Makefile.common,v 1.2 2016/07/02 10:17:18 jaapb Exp $
 
 Use BSD_INSTALL_*
---- Makefile.common.orig       2015-12-16 23:44:44.000000000 +0000
+Compile with OCaml 4.03
+--- Makefile.common.orig       2016-04-11 13:12:51.000000000 +0000
 +++ Makefile.common
 @@ -35,7 +35,7 @@ else
  endif
@@ -12,3 +13,12 @@
  INSTALLSH:=./install.sh
  MKDIR:=install -d
  
+@@ -231,7 +231,7 @@ endif
+ LINKCMO:=$(CORECMA) $(STATICPLUGINS)
+ LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa)
+ 
+-IDEDEPS:=lib/clib.cma lib/xml_lexer.cmo lib/xml_parser.cmo lib/xml_printer.cmo lib/errors.cmo lib/spawn.cmo
++IDEDEPS:=lib/clib.cma lib/errors.cmo lib/spawn.cmo
+ IDECMA:=ide/ide.cma
+ IDETOPLOOPCMA=ide/coqidetop.cma
+