From 2b5269ef60233fc5c3ff720528126ae142356357 Mon Sep 17 00:00:00 2001 From: tonio Date: Sat, 1 Dec 2007 13:05:36 +0000 Subject: 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. --- 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(-) create mode 100644 lang/coq/patches/patch-ab (limited to 'lang/coq') diff --git a/lang/coq/Makefile b/lang/coq/Makefile index 040683823c9..f6f8b3ed7d1 100644 --- a/lang/coq/Makefile +++ b/lang/coq/Makefile @@ -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 HOMEPAGE= http://coq.inria.fr/ @@ -47,4 +46,5 @@ PLIST_SUBST+= WITH_IDE='@comment ' .include "../../mk/pthread.buildlink3.mk" .include "../../lang/ocaml/buildlink3.mk" +.include "../../lang/camlp5/buildlink3.mk" .include "../../mk/bsd.pkg.mk" diff --git a/lang/coq/PLIST b/lang/coq/PLIST index cd61278a593..e03005158b4 100644 --- a/lang/coq/PLIST +++ b/lang/coq/PLIST @@ -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/Ring_theory.vo 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 --git a/lang/coq/distinfo b/lang/coq/distinfo index 46bce0304cc..b7ef051cad8 100644 --- a/lang/coq/distinfo +++ b/lang/coq/distinfo @@ -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 --git a/lang/coq/patches/patch-aa b/lang/coq/patches/patch-aa index 2216aff94f0..f74c4f97d2b 100644 --- a/lang/coq/patches/patch-aa +++ b/lang/coq/patches/patch-aa @@ -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 @@ $NetBSD: patch-aa,v 1.5 2007/02/25 15:03:52 tonio Exp $ ########################################################################### # 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 @@ $NetBSD: patch-aa,v 1.5 2007/02/25 15:03:52 tonio Exp $ ########################################################################### # 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 @@ $NetBSD: patch-aa,v 1.5 2007/02/25 15:03:52 tonio Exp $ - $(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 @@ $NetBSD: patch-aa,v 1.5 2007/02/25 15:03:52 tonio Exp $ 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 @@ $NetBSD: patch-aa,v 1.5 2007/02/25 15:03:52 tonio Exp $ # -$(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 --git a/lang/coq/patches/patch-ab b/lang/coq/patches/patch-ab new file mode 100644 index 00000000000..60630877b49 --- /dev/null +++ b/lang/coq/patches/patch-ab @@ -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' ` + -- cgit v1.2.3