diff options
author | tonio <tonio> | 2011-03-28 20:39:26 +0000 |
---|---|---|
committer | tonio <tonio> | 2011-03-28 20:39:26 +0000 |
commit | 892e342f7b3cbd4554a34fc0dc823c42c9eaeb5f (patch) | |
tree | 5a3d0fe7c8d5c8c57db80f6add51c2cc56f16b04 /lang/coq | |
parent | 89ef0ebce28954db20e754e9c6a69c1368fc7d3b (diff) | |
download | pkgsrc-892e342f7b3cbd4554a34fc0dc823c42c9eaeb5f.tar.gz |
Update lang/coq to 8.3pl1
Changes from V8.3 to V8.3pl1
o Type inference, notations and implicit arguments bug fixes
- #2448 (alpha-renaming problems with notations internally using binders)
- #2454 (pattern-matching sometimes not supporting type casts)
- fixing combined use of non-implicit and explictly-declared implicit arguments
in inductive arities
- restored support for using some ident with different scopes in notations
o Ltac and tactics bug fixes
- #2414 (rewrite in not looking for eq_ind in the right module)
- #2433 (new "is_evar"/"has_evar" to restore support for matching evars in Ltac)
- #2453 (dependent destruction)
- loop in dependent destruction
- new "constr_eq" tactic for restoring support for term equality test in Ltac
- setoid rewrite under cases and abstraction fixed
o Coqdoc and documentation bugs
- #2418 (wrong URLs in documentation)
- #2441 (coqdoc bug in Mergesort.v)
- #2445 (correct support for "'" character in coqdoc links to notations)
- fixed wrong use of "moduleid" instead of "module" in coqdoc html indexes
- fixing parsing of Multiplication and Division signs (unicode 0xD7 and 0xF7)
o Compilation
- #2432 (support for compilation with camlp5 6.02.0)
- support for compilation with ocaml >= 3.09.3 restored
o Extraction
- #2413 (prevent type-unsafe optimisations of pattern matching)
- Identifiers of a development aimed to be extracted should
avoid containing "__", since the extraction make various use of
this sub-string, leading to potential name clashes. This was
already so in V8.3, but not announced, as mentionned by #2421.
o Miscellaneous bug fixes
- #2412 (anomaly Ploc.Exc when using Ltac Debug)
- #2419 (redundant opp_compare removed)
- #2427 (Module Functor claims Signature does not match)
- #2431 (compliance of CoqIDE use of mutexes with FreeBSD)
- #2434 (anomaly DuringSyntaxChecking with Local/Global prefixes)
- a few improvements in efficiency
Diffstat (limited to 'lang/coq')
-rw-r--r-- | lang/coq/Makefile | 7 | ||||
-rw-r--r-- | lang/coq/distinfo | 10 | ||||
-rw-r--r-- | lang/coq/patches/patch-aa | 31 | ||||
-rw-r--r-- | lang/coq/patches/patch-ab | 52 |
4 files changed, 7 insertions, 93 deletions
diff --git a/lang/coq/Makefile b/lang/coq/Makefile index 10354d736d7..2eab2854f0e 100644 --- a/lang/coq/Makefile +++ b/lang/coq/Makefile @@ -1,10 +1,9 @@ -# $NetBSD: Makefile,v 1.29 2011/01/13 13:38:33 wiz Exp $ +# $NetBSD: Makefile,v 1.30 2011/03/28 20:39:26 tonio Exp $ # -DISTNAME= coq-8.3 -PKGREVISION= 2 +DISTNAME= coq-8.3pl1 CATEGORIES= lang math -MASTER_SITES= http://coq.inria.fr/distrib/V8.3/files/ +MASTER_SITES= http://coq.inria.fr/distrib/V8.3pl1/files/ MAINTAINER= richards+netbsd@CS.Princeton.EDU HOMEPAGE= http://coq.inria.fr/ diff --git a/lang/coq/distinfo b/lang/coq/distinfo index 85aff64b172..8a6e9a540f7 100644 --- a/lang/coq/distinfo +++ b/lang/coq/distinfo @@ -1,8 +1,6 @@ -$NetBSD: distinfo,v 1.12 2010/11/14 20:53:02 tonio Exp $ +$NetBSD: distinfo,v 1.13 2011/03/28 20:39:26 tonio Exp $ -SHA1 (coq-8.3.tar.gz) = 6c6472b6a41429e78d979eacd8ff58bd6f6c9da4 -RMD160 (coq-8.3.tar.gz) = 9e42266001c0a22b39662be86960a05e454fc2fb -Size (coq-8.3.tar.gz) = 3736420 bytes -SHA1 (patch-aa) = 851efa1859b4d8dc7bad549792a5966b549f868e -SHA1 (patch-ab) = f20f78c936e18ca195933375f37fc5b816827604 +SHA1 (coq-8.3pl1.tar.gz) = 3fae9fa2fd6f39c9fb3c0b67fcd5e71f1e7a5f9f +RMD160 (coq-8.3pl1.tar.gz) = 687983bcaca723299b6ea902a1e1b07338209d55 +Size (coq-8.3pl1.tar.gz) = 3756961 bytes SHA1 (patch-ac) = 59516eb44aa6cedb4f897b5ac3e8fe0aa69aba0f diff --git a/lang/coq/patches/patch-aa b/lang/coq/patches/patch-aa deleted file mode 100644 index db825e53d81..00000000000 --- a/lang/coq/patches/patch-aa +++ /dev/null @@ -1,31 +0,0 @@ -$NetBSD: patch-aa,v 1.9 2010/11/14 20:53:03 tonio Exp $ - -Fix mixed implicit and normal rules -This fixes build with GNU Make 3.82. See threads: - https://sympa-roc.inria.fr/wws/arc/coqdev/2010-10/msg00025.html - http://thread.gmane.org/gmane.comp.gnu.make.bugs/4912 - -Patch from https://gforge.inria.fr/scm/viewvc.php?diff_format=s&view=rev&root=coq&sortby=file&revision=13566 - ---- Makefile.orig 2010-10-13 19:53:28.000000000 +0000 -+++ Makefile -@@ -160,9 +160,19 @@ else - stage1 $(STAGE1_TARGETS) : always - $(call stage-template,1) - -+ifneq (,$(STAGE1_IMPLICITS)) -+$(STAGE1_IMPLICITS) : always -+ $(call stage-template,1) -+endif -+ - stage2 $(STAGE2_TARGETS) : stage1 - $(call stage-template,2) - -+ifneq (,$(STAGE2_IMPLICITS)) -+$(STAGE2_IMPLICITS) : stage1 -+ $(call stage-template,2) -+endif -+ - # Nota: - # - world is one of the targets in $(STAGE2_TARGETS), hence launching - # "make" or "make world" leads to recursion into stage1 then stage2 diff --git a/lang/coq/patches/patch-ab b/lang/coq/patches/patch-ab deleted file mode 100644 index 7fdf8549107..00000000000 --- a/lang/coq/patches/patch-ab +++ /dev/null @@ -1,52 +0,0 @@ -$NetBSD: patch-ab,v 1.4 2010/11/14 20:53:03 tonio Exp $ - -Fix mixed implicit and normal rules -This fixes build with GNU Make 3.82. See threads: - https://sympa-roc.inria.fr/wws/arc/coqdev/2010-10/msg00025.html - http://thread.gmane.org/gmane.comp.gnu.make.bugs/4912 - -Patch from https://gforge.inria.fr/scm/viewvc.php?diff_format=s&view=rev&root=coq&sortby=file&revision=13566 - ---- Makefile.common.orig 2010-06-23 13:17:17.000000000 +0000 -+++ Makefile.common -@@ -365,7 +365,7 @@ DATE=$(shell LANG=C date +"%B %Y") - - SOURCEDOCDIR=dev/source-doc - --CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot -+CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.o %.cmi %.cma %.cmxa %.a %.cmxs %.dep.ps %.dot - - ### Targets forwarded by Makefile to a specific stage: - -@@ -374,10 +374,12 @@ CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi - STAGE1_TARGETS:= $(STAGE1) $(COQDEPBOOT) \ - $(GENFILES) \ - source-doc revision toplevel/mltop.byteml toplevel/mltop.optml \ -- $(STAGE1_ML4:.ml4=.ml4-preprocessed) %.o -+ $(STAGE1_ML4:.ml4=.ml4-preprocessed) -+ -+STAGE1_IMPLICITS:= - - ifdef CM_STAGE1 -- STAGE1_TARGETS+=$(CAML_OBJECT_PATTERNS) -+ STAGE1_IMPLICITS+=$(CAML_OBJECT_PATTERNS) - endif - - ## Enumeration of targets that require being done at stage2 -@@ -402,12 +404,13 @@ STAGE2_TARGETS:=$(COQBINARIES) lib kerne - printers debug initplugins plugins \ - world install coqide coqide-files coq coqlib \ - coqlight states check init theories theories-light \ -- $(DOC_TARGETS) $(VO_TARGETS) validate \ -- %.vo %.glob states/% install-% %.ml4-preprocessed \ -+ $(DOC_TARGETS) $(VO_TARGETS) validate -+ -+STAGE2_IMPLICITS:= %.vo %.glob states/% install-% %.ml4-preprocessed \ - $(DOC_TARGET_PATTERNS) - - ifndef CM_STAGE1 -- STAGE2_TARGETS+=$(CAML_OBJECT_PATTERNS) -+ STAGE2_IMPLICITS+=$(CAML_OBJECT_PATTERNS) - endif - - |