adding compatibility patches for make-3.82 and camlp5-6.02.0, fixes bug #346061

Package-Manager: portage-2.1.9.24/cvs/Linux i686

5 files changed, 185 insertions, 4 deletions

diff --git a/sci-mathematics/coq/ChangeLog b/sci-mathematics/coq/ChangeLog
index c3ae250a5628..0ecaa31058bc 100644
--- a/sci-mathematics/coq/ChangeLog
+++ b/sci-mathematics/coq/ChangeLog
@@ -1,6 +1,11 @@
 # ChangeLog for sci-mathematics/coq
 # Copyright 1999-2010 Gentoo Foundation; Distributed under the GPL v2
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/ChangeLog,v 1.57 2010/11/18 22:12:07 tomka Exp $
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/ChangeLog,v 1.58 2010/11/20 12:44:09 tomka Exp $
+
+  20 Nov 2010; Thomas Kahle <tomka@gentoo.org> coq-8.3.ebuild,
+  +files/coq-8.3-camlp5-6-compat.patch, +files/coq-8.3-make-3.82-compat.patch:
+  adding compatibility patches for make-3.82 and camlp5-6.02.0, fixes bug
+  #346061
 
 *coq-8.3 (18 Nov 2010)
 
diff --git a/sci-mathematics/coq/Manifest b/sci-mathematics/coq/Manifest
index 94f1865f69e3..248f7b5909eb 100644
--- a/sci-mathematics/coq/Manifest
+++ b/sci-mathematics/coq/Manifest
@@ -1,10 +1,22 @@
+-----BEGIN PGP SIGNED MESSAGE-----
+Hash: SHA1
+
 AUX coq-8.2_p2-make-3.82.patch 293 RMD160 4b6d9126c93f9ff882a3aea7518529a09fdd2e69 SHA1 288b77f8ba94791c800a6395260273d96cf582e4 SHA256 9630602f54509704e447c8a306d7153a54937ae523ae7d06aeb3618a53cd1f21
+AUX coq-8.3-camlp5-6-compat.patch 3237 RMD160 e85d7d0a7c2516f56a3fe6a0b27825b0abd29478 SHA1 6eb6e1195a6dcd250415261e8e1dc2569c4dcf09 SHA256 de85dd8f80502d433e0c3100a96c7c64f5a11d797b115d4817a344a41a53ab43
+AUX coq-8.3-make-3.82-compat.patch 2748 RMD160 ed1245099eae9b81f695fc5f52dd736f09aed05e SHA1 9cc12f47cd76065e3f21f83e151e3ef9b2bc4be9 SHA256 728f51470cb45aaac5e1835a8049078a185f8b538d87aefb56be05a385ea0c6c
 AUX coqide.desktop 233 RMD160 3f9d112d7f55454f72c42b427005b37971c6e928 SHA1 40571b86c25793e7d4e9bef80f637d7440b03704 SHA256 dba2e81a408ae51e187c2a164794f9505c4abfa0b92f47a44d0e9f96e2b6dfac
 DIST coq-8.2pl1.tar.gz 3600620 RMD160 dd5758a94bb3de49967cec76baa33eb5169659ce SHA1 4aed3302adc2edbaa5d97984512c1c13014bd649 SHA256 7c15acfd369111e51d937cce632d22fc77a6718a5ac9f2dd2dcbdfab4256ae0c
 DIST coq-8.2pl2.tar.gz 3649761 RMD160 7ecd8a63d8c6f43c0f4c18737895d656f2275913 SHA1 97e1f3d458845cb2934fa0573521fa517994295a SHA256 0e66c2576150bf18828bfff94df50e3405acda6c728ad01a4906fdbdc6de0236
 DIST coq-8.3.tar.gz 3736420 RMD160 9e42266001c0a22b39662be86960a05e454fc2fb SHA1 6c6472b6a41429e78d979eacd8ff58bd6f6c9da4 SHA256 bd818e053948e6eed288753fe10fe2b23bdc6f277a8fe50a6233d8f07b263e0a
 EBUILD coq-8.2_p1-r1.ebuild 2082 RMD160 28db3f8eab31f791c998313fb4582f815959b5fc SHA1 0f3586ca49332156095e5e51dfeee722e268a382 SHA256 a0efb6515a0aec8cdc81badaf07f11c2a29248baa478525cd09941043aef2614
 EBUILD coq-8.2_p2.ebuild 2131 RMD160 00f1d0401ca733bc856956af6623aa28e70d4edd SHA1 032e693e3d65e71cc16ba6de7a3953e0df56159a SHA256 28e386072d15925371678bd52049c9b54b2b4bff2d65410699a88b5bc44f5f5f
-EBUILD coq-8.3.ebuild 2142 RMD160 4ab675983b03fbd3e10a146c9ff668326d025661 SHA1 6029af3f1184610624f2b75fb6ec41b983eeb57a SHA256 695a16f6e5317d79680f1ea8aa3a91039a4e74944e922fe3adeca24ab83da328
-MISC ChangeLog 9351 RMD160 a0f0133c7347611b6ff740af14f9c5434f4c231e SHA1 9f30675ce10d38d46dcc203695dcad960b039269 SHA256 8512a489042ec9c58683b7885e5f958ada2ed40cb23df1561deb6463052a90a1
+EBUILD coq-8.3.ebuild 2290 RMD160 037e42a8799283e5a96692e389bbe8080915ef49 SHA1 e6632ae196b05781854988d388eeea190b9daee1 SHA256 e0bcafdeca60a6a54c8477fe00bade0855ec2029e5dd12c87c2db172420ac98e
+MISC ChangeLog 9578 RMD160 0b40ac37af42e1c65330d1f1314101e4218283bd SHA1 d7194e66f50ee5990b4082ca3dc8b4b182af5617 SHA256 e5a8e0f56e300711272ebcb7dbe7c74c8a78937ebc2375ff9cf2ae8697fd24b4
 MISC metadata.xml 978 RMD160 87ac5db98680ca1eef0b2d5fbdb2963b182a35cb SHA1 cef1c29019652dbe87c3ba5daeeaec63e0bb5e2d SHA256 dd2767eb316b5bf7c1c66c555f3b54b9d812f22631ab8d27151a1ce13b54d203
+-----BEGIN PGP SIGNATURE-----
+Version: GnuPG v2.0.16 (GNU/Linux)
+
+iEYEARECAAYFAkznwIcACgkQnZsgo/h8kNbNFgCglSrUC4n6PArzWwle0NpI5kWF
+HvoAnAmEGwOmiSBH48Dfzti8eKx+1w1t
+=pbkw
+-----END PGP SIGNATURE-----
diff --git a/sci-mathematics/coq/coq-8.3.ebuild b/sci-mathematics/coq/coq-8.3.ebuild
index 9092a70cd431..57f440b42075 100644
--- a/sci-mathematics/coq/coq-8.3.ebuild
+++ b/sci-mathematics/coq/coq-8.3.ebuild
@@ -1,6 +1,6 @@
 # Copyright 1999-2010 Gentoo Foundation
 # Distributed under the terms of the GNU General Public License v2
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.3.ebuild,v 1.1 2010/11/18 22:12:07 tomka Exp $
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.3.ebuild,v 1.2 2010/11/20 12:44:09 tomka Exp $
 
 EAPI="2"
 
@@ -30,6 +30,9 @@ DEPEND="${RDEPEND}
 		)"
 
 src_prepare() {
+	# From upstream CVS, remove on next patchlevel:
+	epatch "${FILESDIR}/${P}-camlp5-6-compat.patch"
+	epatch "${FILESDIR}/${P}-make-3.82-compat.patch"
 	# configure has an error at line 640 leading to closing a string
 	# to early in the generated coq_config.ml. Here is a wild sed :)
 	# It replaces \"$LABLGTKLIB\" by $LABLGTKLIB
diff --git a/sci-mathematics/coq/files/coq-8.3-camlp5-6-compat.patch b/sci-mathematics/coq/files/coq-8.3-camlp5-6-compat.patch
new file mode 100644
index 000000000000..50ae78340dbc
--- /dev/null
+++ b/sci-mathematics/coq/files/coq-8.3-camlp5-6-compat.patch
@@ -0,0 +1,77 @@
+From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
+Date: Tue, 16 Nov 2010 20:25:56 +0000 (+0000)
+Subject: Support for camlp5 6.02.0 (Closes: #2432)
+X-Git-Url: https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq%2Fcoq-svn.git;a=commitdiff_plain;h=501c9cb6ff7c903974123284fe795cdcaab8f300
+
+Support for camlp5 6.02.0 (Closes: #2432)
+
+git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@13641 85f007b7-540e-0410-9357-904b9bb8a0f7
+---
+
+diff --git a/lib/compat.ml4 b/lib/compat.ml4
+index 9b6bb19..a77c2bc 100644
+--- a/lib/compat.ml4
++++ b/lib/compat.ml4
+@@ -65,3 +65,15 @@ let unloc = M.unloc
+ let join_loc = M.join_loc
+ type token = M.token
+ type lexer = M.lexer
++
++IFDEF CAMLP5_6_00 THEN
++
++let slist0sep x y = Gramext.Slist0sep (x, y, false)
++let slist1sep x y = Gramext.Slist1sep (x, y, false)
++
++ELSE
++
++let slist0sep x y = Gramext.Slist0sep (x, y)
++let slist1sep x y = Gramext.Slist1sep (x, y)
++
++END
+diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
+index 4719e6d..5d37f4a 100644
+--- a/parsing/pcoq.ml4
++++ b/parsing/pcoq.ml4
+@@ -631,16 +631,16 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ =
+     | ETConstrList (typ',[]) ->
+         Gramext.Slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'))
+     | ETConstrList (typ',tkl) ->
+-        Gramext.Slist1sep
+-          (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'),
+-	   make_sep_rules tkl)
++        Compat.slist1sep
++          (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'))
++          (make_sep_rules tkl)
+     | ETBinderList (false,[]) ->
+         Gramext.Slist1
+ 	  (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false))
+     | ETBinderList (false,tkl) ->
+-        Gramext.Slist1sep
+-	  (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false),
+-	   make_sep_rules tkl)
++        Compat.slist1sep
++          (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false))
++          (make_sep_rules tkl)
+     | _ ->
+     match interp_constr_prod_entry_key assoc from forpat typ with
+       | (eobj,None,_) -> Gramext.Snterm (Gram.Entry.obj eobj)
+@@ -654,16 +654,16 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ =
+ let rec symbol_of_prod_entry_key = function
+   | Alist1 s -> Gramext.Slist1 (symbol_of_prod_entry_key s)
+   | Alist1sep (s,sep) ->
+-      Gramext.Slist1sep (symbol_of_prod_entry_key s, Gramext.Stoken ("",sep))
++      Compat.slist1sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", sep))
+   | Alist0 s -> Gramext.Slist0 (symbol_of_prod_entry_key s)
+   | Alist0sep (s,sep) ->
+-      Gramext.Slist0sep (symbol_of_prod_entry_key s, Gramext.Stoken ("",sep))
++      Compat.slist0sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", sep))
+   | Aopt s -> Gramext.Sopt (symbol_of_prod_entry_key s)
+   | Amodifiers s ->
+        Gramext.srules
+         [([], Gramext.action(fun _loc -> []));
+          ([Gramext.Stoken ("", "(");
+-           Gramext.Slist1sep ((symbol_of_prod_entry_key s), Gramext.Stoken ("", ","));
++           Compat.slist1sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", ","));
+            Gramext.Stoken ("", ")")],
+ 	   Gramext.action (fun _ l _ _loc -> l))]
+   | Aself -> Gramext.Sself
diff --git a/sci-mathematics/coq/files/coq-8.3-make-3.82-compat.patch b/sci-mathematics/coq/files/coq-8.3-make-3.82-compat.patch
new file mode 100644
index 000000000000..5176aa33ec8a
--- /dev/null
+++ b/sci-mathematics/coq/files/coq-8.3-make-3.82-compat.patch
@@ -0,0 +1,84 @@
+From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
+Date: Tue, 19 Oct 2010 13:22:08 +0000 (+0000)
+Subject: Fix mixed implicit and normal rules
+X-Git-Url: https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq%2Fcoq-svn.git;a=commitdiff_plain;h=86eb08bad450dd3fa77b11e4a34d2f493ab80d85
+
+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
+
+git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@13566 85f007b7-540e-0410-9357-904b9bb8a0f7
+---
+
+diff --git a/Makefile b/Makefile
+index b1edc01..ea73c51 100644
+--- a/Makefile
++++ b/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/Makefile.common b/Makefile.common
+index cc38980..46bf217 100644
+--- a/Makefile.common
++++ b/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 %.cma %.cmxa %.cmxs %.dep.ps %.dot
+ 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 kernel byterun library proofs tactics \
+   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
+ 
+