diff options
author | jaapb <jaapb@pkgsrc.org> | 2016-07-02 10:17:18 +0000 |
---|---|---|
committer | jaapb <jaapb@pkgsrc.org> | 2016-07-02 10:17:18 +0000 |
commit | ab91c2ee2876831f57ff12397f021fc5b51482a8 (patch) | |
tree | 999279642fd2fe5dda8e74ebb90b51c60d706889 /lang/coq | |
parent | 6069fd62e39a8d4344210f463e68ca2e1e51fb78 (diff) | |
download | pkgsrc-ab91c2ee2876831f57ff12397f021fc5b51482a8.tar.gz |
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 (limited to 'lang/coq')
-rw-r--r-- | lang/coq/Makefile | 11 | ||||
-rw-r--r-- | lang/coq/PLIST | 4 | ||||
-rw-r--r-- | lang/coq/distinfo | 12 | ||||
-rw-r--r-- | lang/coq/patches/patch-Makefile.common | 14 |
4 files changed, 28 insertions, 13 deletions
diff --git a/lang/coq/Makefile b/lang/coq/Makefile index d5e8d374f4a..0b8a63e08e1 100644 --- a/lang/coq/Makefile +++ b/lang/coq/Makefile @@ -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 @@ PLIST_VARS+= coqide natdynlink doc 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 --git a/lang/coq/PLIST b/lang/coq/PLIST index 2b9a4f3a94e..d9bf11cc798 100644 --- a/lang/coq/PLIST +++ b/lang/coq/PLIST @@ -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/aux_file.cmi 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/control.cmi 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 --git a/lang/coq/distinfo b/lang/coq/distinfo index 15da4310035..b2e9ac07091 100644 --- a/lang/coq/distinfo +++ b/lang/coq/distinfo @@ -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 --git a/lang/coq/patches/patch-Makefile.common b/lang/coq/patches/patch-Makefile.common index ed1aac76310..19806bbbaec 100644 --- a/lang/coq/patches/patch-Makefile.common +++ b/lang/coq/patches/patch-Makefile.common @@ -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 @@ Use BSD_INSTALL_* 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 + |