[pkgsrc/trunk]: pkgsrc/lang/coq Update lang/coq to 8.3pl1

To: pkgsrc-changes-hg%NetBSD.org@localhost
Subject: [pkgsrc/trunk]: pkgsrc/lang/coq Update lang/coq to 8.3pl1
From: tonio <tonio%pkgsrc.org@localhost>
Date: Thu, 14 Oct 2021 10:37:32 +0000

details:   https://anonhg.NetBSD.org/pkgsrc/rev/e3c266669874
branches:  trunk
changeset: 587069:e3c266669874
user:      tonio <tonio%pkgsrc.org@localhost>
date:      Mon Mar 28 20:39:26 2011 +0000

description:
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:

 lang/coq/Makefile         |   7 ++---
 lang/coq/distinfo         |  10 +++-----
 lang/coq/patches/patch-aa |  31 ----------------------------
 lang/coq/patches/patch-ab |  52 -----------------------------------------------
 4 files changed, 7 insertions(+), 93 deletions(-)

diffs (124 lines):

diff -r d69e1d0f3c82 -r e3c266669874 lang/coq/Makefile
--- a/lang/coq/Makefile Mon Mar 28 20:29:00 2011 +0000
+++ b/lang/coq/Makefile Mon Mar 28 20:39:26 2011 +0000
@@ -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@localhost
 HOMEPAGE=      http://coq.inria.fr/
diff -r d69e1d0f3c82 -r e3c266669874 lang/coq/distinfo
--- a/lang/coq/distinfo Mon Mar 28 20:29:00 2011 +0000
+++ b/lang/coq/distinfo Mon Mar 28 20:39:26 2011 +0000
@@ -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 -r d69e1d0f3c82 -r e3c266669874 lang/coq/patches/patch-aa
--- a/lang/coq/patches/patch-aa Mon Mar 28 20:29:00 2011 +0000
+++ /dev/null   Thu Jan 01 00:00:00 1970 +0000
@@ -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 -r d69e1d0f3c82 -r e3c266669874 lang/coq/patches/patch-ab
--- a/lang/coq/patches/patch-ab Mon Mar 28 20:29:00 2011 +0000
+++ /dev/null   Thu Jan 01 00:00:00 1970 +0000
@@ -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
- 
-

Prev by Date: [pkgsrc/trunk]: pkgsrc/misc/ec2-ami-tools Import misc/ec2-ami-tools.
Next by Date: [pkgsrc/trunk]: pkgsrc/meta-pkgs/boost Fix build of boost-libs in NetBSD/macp...
Previous by Thread: [pkgsrc/trunk]: pkgsrc/misc/ec2-ami-tools Import misc/ec2-ami-tools.
Next by Thread: [pkgsrc/trunk]: pkgsrc/meta-pkgs/boost Fix build of boost-libs in NetBSD/macp...
Indexes:

Home | Main Index | Thread Index | Old Index