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

2 files changed, 161 insertions, 0 deletions

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
+ 
+