From 7e2189152704cdabc6cda66c3c4a3f0a709485a8 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 21 Feb 2011 15:05:38 +0100 Subject: Refresh patches --- debian/patches/0001-Disable-micromega-tests.patch | 2 +- debian/patches/0002-Remove-dependency-to-Unix-from-module-Profile.patch | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/debian/patches/0001-Disable-micromega-tests.patch b/debian/patches/0001-Disable-micromega-tests.patch index 8857a874..5979dc6d 100644 --- a/debian/patches/0001-Disable-micromega-tests.patch +++ b/debian/patches/0001-Disable-micromega-tests.patch @@ -1,6 +1,6 @@ From: Stephane Glondu Date: Mon, 22 Feb 2010 10:39:03 +0100 -Subject: [PATCH] Disable micromega tests +Subject: Disable micromega tests Workaround for bug #570920. --- diff --git a/debian/patches/0002-Remove-dependency-to-Unix-from-module-Profile.patch b/debian/patches/0002-Remove-dependency-to-Unix-from-module-Profile.patch index 7a84720b..fd1aaf13 100644 --- a/debian/patches/0002-Remove-dependency-to-Unix-from-module-Profile.patch +++ b/debian/patches/0002-Remove-dependency-to-Unix-from-module-Profile.patch @@ -1,6 +1,6 @@ From: Stephane Glondu Date: Fri, 2 Jul 2010 15:00:43 +0200 -Subject: [PATCH] Remove dependency to Unix from module Profile +Subject: Remove dependency to Unix from module Profile Applied-Upstream: https://gforge.inria.fr/scm/viewvc.php?view=rev&root=coq&revision=13234 Signed-off-by: Stephane Glondu -- cgit v1.2.3 From 6b3bd571d555c4db91ab210da9a302b2f2181e23 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 21 Feb 2011 15:05:27 +0100 Subject: Add Fix-build-with-camlp5-6.02.1.patch --- .../0003-Fix-build-with-camlp5-6.02.1.patch | 155 +++++++++++++++++++++ debian/patches/series | 1 + 2 files changed, 156 insertions(+) create mode 100644 debian/patches/0003-Fix-build-with-camlp5-6.02.1.patch diff --git a/debian/patches/0003-Fix-build-with-camlp5-6.02.1.patch b/debian/patches/0003-Fix-build-with-camlp5-6.02.1.patch new file mode 100644 index 00000000..908296ac --- /dev/null +++ b/debian/patches/0003-Fix-build-with-camlp5-6.02.1.patch @@ -0,0 +1,155 @@ +From: Stephane Glondu +Date: Wed, 17 Nov 2010 21:26:49 +0000 +Subject: Fix build with camlp5 6.02.1 + +This is a squash of upstream commits 13647 and 13706 in v8.2 branch. +--- + lib/compat.ml4 | 10 ++++++++++ + parsing/pcoq.ml4 | 11 ++++++++--- + parsing/pcoq.mli | 2 ++ + parsing/q_util.ml4 | 6 +++--- + toplevel/metasyntax.ml | 26 +++++++++++++------------- + 5 files changed, 36 insertions(+), 19 deletions(-) + +diff --git a/lib/compat.ml4 b/lib/compat.ml4 +index 40cffad..de049b2 100644 +--- a/lib/compat.ml4 ++++ b/lib/compat.ml4 +@@ -69,3 +69,13 @@ let join_loc = M.join_loc + type token = M.token + type lexer = M.lexer + let using = M.using ++ ++(** Compatibility with Camlp5 6.x *) ++ ++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 d2d81cd..3ab89cd 100644 +--- a/parsing/pcoq.ml4 ++++ b/parsing/pcoq.ml4 +@@ -159,6 +159,11 @@ module Gram = + errorlabstrm "Pcoq.delete_rule" (str "GDELETE_RULE forbidden.") + end + ++IFDEF CAMLP5_6_02_1 THEN ++let entry_print x = Gram.Entry.print !Pp_control.std_ft x ++ELSE ++let entry_print = Gram.Entry.print ++END + + let camlp4_verbosity silent f x = + let a = !Gramext.warning_verbose in +@@ -746,9 +751,9 @@ let rec symbol_of_production assoc from forpat typ = + | ETConstrList (typ',[]) -> + Gramext.Slist1 (symbol_of_production assoc from forpat (ETConstr typ')) + | ETConstrList (typ',tkl) -> +- Gramext.Slist1sep +- (symbol_of_production assoc from forpat (ETConstr typ'), +- Gramext.srules ++ Compat.slist1sep ++ (symbol_of_production assoc from forpat (ETConstr typ')) ++ (Gramext.srules + [List.map (fun x -> Gramext.Stoken x) tkl, + List.fold_right (fun _ v -> Gramext.action (fun _ -> v)) tkl + (Gramext.action (fun loc -> ()))]) +diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli +index 0a4b349..077f178 100644 +--- a/parsing/pcoq.mli ++++ b/parsing/pcoq.mli +@@ -24,6 +24,8 @@ val lexer : Compat.lexer + + module Gram : Grammar.S with type te = Compat.token + ++val entry_print : 'a Gram.Entry.e -> unit ++ + (* The superclass of all grammar entries *) + type grammar_object + +diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4 +index da4329b..0d2a890 100644 +--- a/parsing/q_util.ml4 ++++ b/parsing/q_util.ml4 +@@ -82,7 +82,7 @@ let modifiers e = + <:expr< Gramext.srules + [([], Gramext.action(fun _loc -> [])); + ([Gramext.Stoken ("", "("); +- Gramext.Slist1sep ($e$, Gramext.Stoken ("", ",")); ++ Compat.slist1sep $e$ (Gramext.Stoken ("", ",")); + Gramext.Stoken ("", ")")], + Gramext.action (fun _ l _ _loc -> l))] + >> +@@ -96,14 +96,14 @@ let rec interp_entry_name loc s sep = + String.sub s (l-9) 9 = "_list_sep" then + let t, g = interp_entry_name loc (String.sub s 3 (l-12)) "" in + let sep = <:expr< Gramext.Stoken("",$str:sep$) >> in +- List1ArgType t, <:expr< Gramext.Slist1sep $g$ $sep$ >> ++ List1ArgType t, <:expr< Compat.slist1sep $g$ $sep$ >> + else if l > 5 & String.sub s (l-5) 5 = "_list" then + let t, g = interp_entry_name loc (String.sub s 0 (l-5)) "" in + List0ArgType t, <:expr< Gramext.Slist0 $g$ >> + else if l > 9 & String.sub s (l-9) 9 = "_list_sep" then + let t, g = interp_entry_name loc (String.sub s 0 (l-9)) "" in + let sep = <:expr< Gramext.Stoken("",$str:sep$) >> in +- List0ArgType t, <:expr< Gramext.Slist0sep $g$ $sep$ >> ++ List0ArgType t, <:expr< Compat.slist0sep $g$ $sep$ >> + else if l > 4 & String.sub s (l-4) 4 = "_opt" then + let t, g = interp_entry_name loc (String.sub s 0 (l-4)) "" in + OptArgType t, <:expr< Gramext.Sopt $g$ >> +diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml +index 821a73f..ba10708 100644 +--- a/toplevel/metasyntax.ml ++++ b/toplevel/metasyntax.ml +@@ -100,33 +100,33 @@ let add_tactic_notation (n,prods,e) = + let print_grammar = function + | "constr" | "operconstr" | "binder_constr" -> + msgnl (str "Entry constr is"); +- Gram.Entry.print Pcoq.Constr.constr; ++ entry_print Pcoq.Constr.constr; + msgnl (str "and lconstr is"); +- Gram.Entry.print Pcoq.Constr.lconstr; ++ entry_print Pcoq.Constr.lconstr; + msgnl (str "where binder_constr is"); +- Gram.Entry.print Pcoq.Constr.binder_constr; ++ entry_print Pcoq.Constr.binder_constr; + msgnl (str "and operconstr is"); +- Gram.Entry.print Pcoq.Constr.operconstr; ++ entry_print Pcoq.Constr.operconstr; + | "pattern" -> +- Gram.Entry.print Pcoq.Constr.pattern ++ entry_print Pcoq.Constr.pattern + | "tactic" -> + msgnl (str "Entry tactic_expr is"); +- Gram.Entry.print Pcoq.Tactic.tactic_expr; ++ entry_print Pcoq.Tactic.tactic_expr; + msgnl (str "Entry binder_tactic is"); +- Gram.Entry.print Pcoq.Tactic.binder_tactic; ++ entry_print Pcoq.Tactic.binder_tactic; + msgnl (str "Entry simple_tactic is"); +- Gram.Entry.print Pcoq.Tactic.simple_tactic; ++ entry_print Pcoq.Tactic.simple_tactic; + | "vernac" -> + msgnl (str "Entry vernac is"); +- Gram.Entry.print Pcoq.Vernac_.vernac; ++ entry_print Pcoq.Vernac_.vernac; + msgnl (str "Entry command is"); +- Gram.Entry.print Pcoq.Vernac_.command; ++ entry_print Pcoq.Vernac_.command; + msgnl (str "Entry syntax is"); +- Gram.Entry.print Pcoq.Vernac_.syntax; ++ entry_print Pcoq.Vernac_.syntax; + msgnl (str "Entry gallina is"); +- Gram.Entry.print Pcoq.Vernac_.gallina; ++ entry_print Pcoq.Vernac_.gallina; + msgnl (str "Entry gallina_ext is"); +- Gram.Entry.print Pcoq.Vernac_.gallina_ext; ++ entry_print Pcoq.Vernac_.gallina_ext; + | _ -> error "Unknown or unprintable grammar entry." + + (**********************************************************************) +-- diff --git a/debian/patches/series b/debian/patches/series index d368c657..7ce5e4c8 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -1,2 +1,3 @@ 0001-Disable-micromega-tests.patch 0002-Remove-dependency-to-Unix-from-module-Profile.patch +0003-Fix-build-with-camlp5-6.02.1.patch -- cgit v1.2.3 From 9a65bba53c76358913f02222c968c5880ea34208 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 21 Feb 2011 15:07:55 +0100 Subject: Update changelog and prepare upload to unstable --- debian/changelog | 8 ++++++++ debian/control | 2 +- 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/debian/changelog b/debian/changelog index beef4fb5..22a134cd 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,3 +1,11 @@ +coq (8.2.pl2+dfsg-2) unstable; urgency=low + + * Add Fix-build-with-camlp5-6.02.1.patch + * Bump versioned build-dependency on liblablgtk2-ocaml-dev to ease + lablgtk2 transition + + -- Stéphane Glondu Mon, 21 Feb 2011 16:51:11 +0100 + coq (8.2.pl2+dfsg-1) unstable; urgency=low * New upstream release diff --git a/debian/control b/debian/control index b3db1413..8687770b 100644 --- a/debian/control +++ b/debian/control @@ -13,7 +13,7 @@ Build-Depends: ocaml-nox (>= 3.11.1-3~), ocaml-best-compilers, camlp5 (>= 5.12-2~), - liblablgtk2-ocaml-dev (>= 2.14), + liblablgtk2-ocaml-dev (>= 2.14.2), texlive-latex-extra, hevea (>= 1.10-7) Homepage: http://coq.inria.fr/ -- cgit v1.2.3