[pkgsrc/trunk]: pkgsrc/lang/coq Update lang/coq to 8.2pl2

To: pkgsrc-changes-hg%NetBSD.org@localhost
Subject: [pkgsrc/trunk]: pkgsrc/lang/coq Update lang/coq to 8.2pl2
From: tonio <tonio%pkgsrc.org@localhost>
Date: Thu, 14 Oct 2021 05:33:18 +0000

details:   https://anonhg.NetBSD.org/pkgsrc/rev/22a1a4d6b0c6
branches:  trunk
changeset: 536019:22a1a4d6b0c6
user:      tonio <tonio%pkgsrc.org@localhost>
date:      Sat Dec 01 13:05:36 2007 +0000

description:
Update lang/coq to 8.2pl2

As camlp5 is required with ocaml 3.10, bring it as a dependency anyway,
instead of requiring ocaml 3.10

Changes include:
* Installation
- Support for compilation with ocaml 3.10 and (transitional) camlp5.
- Many bugs have been fixed (cf coq-bugs web page)
- All known failures of ROmega have been fixed. It should now be a
  faithful and quicker replacement for Omega (except when nat parts
  are involved). ROmega and Omega now handle <->.
- Better computational behavior of some constants (eq_nat_dec and
  le_lt_dec more efficient, Z_lt_le_dec and Positive_as_OT.compare
  transparent) [exceptionally source of incompatibilities].
- Loading FSets/FMap used to open unwanted scopes of integer datatypes
  (see bug #1347). These scopes may need to be manually opened now.

diffstat:

 lang/coq/Makefile         |   8 ++++----
 lang/coq/PLIST            |   4 +++-
 lang/coq/distinfo         |  11 ++++++-----
 lang/coq/patches/patch-aa |  22 ++++++++++++++++------
 lang/coq/patches/patch-ab |  13 +++++++++++++
 5 files changed, 42 insertions(+), 16 deletions(-)

diffs (138 lines):

diff -r efe29dfeccaa -r 22a1a4d6b0c6 lang/coq/Makefile
--- a/lang/coq/Makefile Sat Dec 01 13:03:27 2007 +0000
+++ b/lang/coq/Makefile Sat Dec 01 13:05:36 2007 +0000
@@ -1,10 +1,9 @@
-# $NetBSD: Makefile,v 1.17 2007/09/21 13:03:56 wiz Exp $
+# $NetBSD: Makefile,v 1.18 2007/12/01 13:05:36 tonio Exp $
 #
 
-DISTNAME=      coq-8.1
-PKGREVISION=   1
+DISTNAME=      coq-8.1pl2
 CATEGORIES=    lang math
-MASTER_SITES=  ftp://ftp.inria.fr/INRIA/coq/V8.1/
+MASTER_SITES=  ftp://ftp.inria.fr/INRIA/coq/V8.1pl2/
 
 MAINTAINER=    richards+netbsd%CS.Princeton.EDU@localhost
 HOMEPAGE=      http://coq.inria.fr/
@@ -47,4 +46,5 @@
 
 .include "../../mk/pthread.buildlink3.mk"
 .include "../../lang/ocaml/buildlink3.mk"
+.include "../../lang/camlp5/buildlink3.mk"
 .include "../../mk/bsd.pkg.mk"
diff -r efe29dfeccaa -r 22a1a4d6b0c6 lang/coq/PLIST
--- a/lang/coq/PLIST    Sat Dec 01 13:03:27 2007 +0000
+++ b/lang/coq/PLIST    Sat Dec 01 13:05:36 2007 +0000
@@ -1,4 +1,4 @@
-@comment $NetBSD: PLIST,v 1.5 2007/02/25 15:03:52 tonio Exp $
+@comment $NetBSD: PLIST,v 1.6 2007/12/01 13:05:36 tonio Exp $
 bin/coq-interface
 bin/coq-tex
 bin/coq_makefile
@@ -55,7 +55,9 @@
 lib/coq/contrib/setoid_ring/ZArithRing.vo
 lib/coq/contrib/subtac/FixSub.vo
 lib/coq/contrib/subtac/FunctionalExtensionality.vo
+lib/coq/contrib/subtac/Heq.vo
 lib/coq/contrib/subtac/Subtac.vo
+lib/coq/contrib/subtac/SubtacTactics.vo
 lib/coq/contrib/subtac/Utils.vo
 lib/coq/ide/.coqide-gtk2rc
 lib/coq/ide/FAQ
diff -r efe29dfeccaa -r 22a1a4d6b0c6 lang/coq/distinfo
--- a/lang/coq/distinfo Sat Dec 01 13:03:27 2007 +0000
+++ b/lang/coq/distinfo Sat Dec 01 13:05:36 2007 +0000
@@ -1,6 +1,7 @@
-$NetBSD: distinfo,v 1.6 2007/02/25 15:03:52 tonio Exp $
+$NetBSD: distinfo,v 1.7 2007/12/01 13:05:36 tonio Exp $
 
-SHA1 (coq-8.1.tar.gz) = 151aca5b7c919eeb39ba3c6fecec836b7953b206
-RMD160 (coq-8.1.tar.gz) = 548d2e25e7813567252f9b176f318619a780d729
-Size (coq-8.1.tar.gz) = 2977142 bytes
-SHA1 (patch-aa) = 4cc1fdee8074aaa3d1af24151c2d2277522ec9bc
+SHA1 (coq-8.1pl2.tar.gz) = 33ab31abffe42559a5c8341b66a0520805337526
+RMD160 (coq-8.1pl2.tar.gz) = e45451fdd41b1f979febcfb2c0dbd19a39d09256
+Size (coq-8.1pl2.tar.gz) = 2997185 bytes
+SHA1 (patch-aa) = 4a518e52aea4a2e239754b6a8123b9a2fdaefa00
+SHA1 (patch-ab) = b252096b0bef5fee0a2f719ddc17021fd013ed64
diff -r efe29dfeccaa -r 22a1a4d6b0c6 lang/coq/patches/patch-aa
--- a/lang/coq/patches/patch-aa Sat Dec 01 13:03:27 2007 +0000
+++ b/lang/coq/patches/patch-aa Sat Dec 01 13:05:36 2007 +0000
@@ -1,8 +1,8 @@
-$NetBSD: patch-aa,v 1.5 2007/02/25 15:03:52 tonio Exp $
+$NetBSD: patch-aa,v 1.6 2007/12/01 13:05:37 tonio Exp $
 
---- Makefile.orig      2007-02-07 13:21:01.000000000 +0100
+--- Makefile.orig      Thu Oct 11 15:44:00 2007
 +++ Makefile
-@@ -697,22 +697,22 @@ install-coqide:: install-ide-$(HASCOQIDE
+@@ -690,22 +690,22 @@ install-coqide:: install-ide-$(HASCOQIDE
  install-ide-no:
  
  install-ide-byte: 
@@ -33,7 +33,7 @@
  
  ###########################################################################
  # Pcoq: special binaries for debugging (coq-interface, parser)
-@@ -782,18 +782,18 @@ clean::
+@@ -775,18 +775,18 @@ clean::
  install-pcoq:: install-pcoq-binaries install-pcoq-files install-pcoq-manpages
  
  install-pcoq-binaries::
@@ -58,7 +58,7 @@
  
  ###########################################################################
  # tests
-@@ -1248,21 +1248,21 @@ install-coqlight: install-binaries insta
+@@ -1244,22 +1244,21 @@ install-coqlight: install-binaries insta
  install-binaries:: install-$(BEST) install-tools
  
  install-byte::
@@ -79,6 +79,7 @@
 -      $(MKDIR) $(FULLBINDIR)
        # recopie des fichiers de style pour coqide
 -      $(MKDIR) $(FULLCOQLIB)/tools/coqdoc
+-      touch $(FULLCOQLIB)/tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc/coqdoc.css # to have the mode according to umask (bug #1715)
 -      cp tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc
 -      cp $(TOOLS) $(FULLBINDIR)
 +      ${BSD_INSTALL_PROGRAM_DIR} $(FULLBINDIR)
@@ -88,7 +89,7 @@
  
  LIBFILES=$(THEORIESVO) $(CONTRIBVO)
  LIBFILESLIGHT=$(THEORIESLIGHTVO)
-@@ -1275,52 +1275,55 @@ OBJECTCMA=lib/lib.cma kernel/kernel.cma 
+@@ -1272,52 +1271,55 @@ OBJECTCMA=lib/lib.cma kernel/kernel.cma 
  OBJECTCMXA=$(OBJECTCMA:.cma=.cmxa)
  
  install-library:
@@ -165,3 +166,12 @@
  #     -$(UPDATETEX)
  
  ###########################################################################
+@@ -1758,7 +1760,7 @@ depend: dependp4 ml4filesml $(BEFOREDEPE
+       for f in $(ML4FILES); do \
+         bn=`dirname $$f`/`basename $$f .ml4`; \
+         deps=`$(CAMLP4DEPS) $$f`; \
+-        if [[ $${deps} != "" ]]; then \
++        if [ "$${deps}" != "" ]; then \
+           /bin/mv -f .depend .depend.tmp; \
+           sed -e "\|^$${bn}.cmo|s|^$${bn}.cmo: \(.*\)$$|$${bn}.cmo: $${deps} \1|" \
+               -e "\|^$${bn}.cmx|s|^$${bn}.cmx: \(.*\)$$|$${bn}.cmx: $${deps} \1|" \
diff -r efe29dfeccaa -r 22a1a4d6b0c6 lang/coq/patches/patch-ab
--- /dev/null   Thu Jan 01 00:00:00 1970 +0000
+++ b/lang/coq/patches/patch-ab Sat Dec 01 13:05:36 2007 +0000
@@ -0,0 +1,13 @@
+$NetBSD: patch-ab,v 1.1 2007/12/01 13:05:37 tonio Exp $
+
+--- configure.orig     Thu Oct 11 15:13:51 2007
++++ configure
+@@ -326,7 +326,7 @@ esac
+ 
+ # this fixes a camlp4 bug under FreeBSD
+ # ("native-code program cannot do a dynamic load")
+-if [ `uname -s` = "FreeBSD" ]; then camlp4oexec=$camlp4oexec.byte; fi
++#if [ `uname -s` = "FreeBSD" ]; then camlp4oexec=$camlp4oexec.byte; fi
+ 
+ CAMLVERSION=`"$bytecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
+

Prev by Date: [pkgsrc/trunk]: pkgsrc/net/tcpdpriv static functions must not be declared ins...
Next by Date: [pkgsrc/trunk]: pkgsrc/net/xmftp Fixed invalid lvalue cast and reminded the p...
Previous by Thread: [pkgsrc/trunk]: pkgsrc/net/tcpdpriv static functions must not be declared ins...
Next by Thread: [pkgsrc/trunk]: pkgsrc/net/xmftp Fixed invalid lvalue cast and reminded the p...
Indexes:

Home | Main Index | Thread Index | Old Index