summaryrefslogtreecommitdiff
path: root/debian/patches
diff options
context:
space:
mode:
Diffstat (limited to 'debian/patches')
-rw-r--r--debian/patches/0001-Disable-micromega-tests.patch25
-rw-r--r--debian/patches/0002-Remove-dependency-to-Unix-from-module-Profile.patch74
-rw-r--r--debian/patches/0003-Fix-build-with-camlp5-6.02.1.patch155
-rw-r--r--debian/patches/series3
4 files changed, 0 insertions, 257 deletions
diff --git a/debian/patches/0001-Disable-micromega-tests.patch b/debian/patches/0001-Disable-micromega-tests.patch
deleted file mode 100644
index 5979dc6d..00000000
--- a/debian/patches/0001-Disable-micromega-tests.patch
+++ /dev/null
@@ -1,25 +0,0 @@
-From: Stephane Glondu <steph@glondu.net>
-Date: Mon, 22 Feb 2010 10:39:03 +0100
-Subject: Disable micromega tests
-
-Workaround for bug #570920.
----
- test-suite/check | 4 ++--
- 1 files changed, 2 insertions(+), 2 deletions(-)
-
-diff --git a/test-suite/check b/test-suite/check
-index bed86c4..e7889cf 100755
---- a/test-suite/check
-+++ b/test-suite/check
-@@ -248,8 +248,8 @@ echo "Parser tests"
- test_parser parser
- echo "Interactive tests"
- test_interactive interactive
--echo "Micromega tests"
--test_success micromega
-+#echo "Micromega tests"
-+#test_success micromega
-
- # We give a chance to disable the complexity tests which may cause
- # random build failures on build farms
---
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
deleted file mode 100644
index fd1aaf13..00000000
--- a/debian/patches/0002-Remove-dependency-to-Unix-from-module-Profile.patch
+++ /dev/null
@@ -1,74 +0,0 @@
-From: Stephane Glondu <steph@glondu.net>
-Date: Fri, 2 Jul 2010 15:00:43 +0200
-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 <steph@glondu.net>
----
- Makefile.build | 4 ++--
- lib/profile.ml | 8 +++++---
- lib/profile.mli | 4 +---
- 3 files changed, 8 insertions(+), 8 deletions(-)
-
-diff --git a/Makefile.build b/Makefile.build
-index 148bb62..c4358ce 100644
---- a/Makefile.build
-+++ b/Makefile.build
-@@ -782,10 +782,10 @@ dev/printers.cma: $(PRINTERSCMO)
- parsing/grammar.cma: $(GRAMMARCMO)
- $(SHOW)'Testing $@'
- @touch test.ml4
-- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) -I $(CAMLLIB) unix.cma $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
-+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) -I $(CAMLLIB) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
- @rm -f test-grammar test.*
- $(SHOW)'OCAMLC -a $@'
-- $(HIDE)$(OCAMLC) $(BYTEFLAGS) unix.cma $(GRAMMARCMO) -linkall -a -o $@
-+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@
-
- # toplevel/mltop.ml4 (ifdef Byte)
-
-diff --git a/lib/profile.ml b/lib/profile.ml
-index dd7e977..40bfba3 100644
---- a/lib/profile.ml
-+++ b/lib/profile.ml
-@@ -17,8 +17,7 @@ let float_of_time t = float_of_int t /. 100.
- let time_of_float f = int_of_float (f *. 100.)
-
- let get_time () =
-- let {Unix.tms_utime = ut;Unix.tms_stime = st} = Unix.times () in
-- time_of_float (ut +. st)
-+ time_of_float (Sys.time ())
-
- (* Since ocaml 3.01, gc statistics are in float *)
- let get_alloc () =
-@@ -157,7 +156,10 @@ let merge_profile filename (curr_table, curr_outside, curr_total as new_data) =
- (* Unix measure of time is approximative and shoitt delays are often
- unperceivable; therefore, total times are measured in one (big)
- step to avoid rounding errors and to get the best possible
-- approximation *)
-+ approximation.
-+ Note: Sys.time is the same as:
-+ Unix.(let x = times () in x.tms_utime +. x.tms_stime)
-+ *)
-
- (*
- ---------- start profile for f1
-diff --git a/lib/profile.mli b/lib/profile.mli
-index 0937e9e..1e28834 100644
---- a/lib/profile.mli
-+++ b/lib/profile.mli
-@@ -10,12 +10,10 @@
-
- (*s This program is a small time and allocation profiler for Objective Caml *)
-
--(*i It requires the UNIX library *)
-
- (* Adapted from Christophe Raffalli *)
-
--(* To use it, link it with the program you want to profile (do not forget
--"-cclib -lunix -custom unix.cma" among the link options).
-+(* To use it, link it with the program you want to profile.
-
- To trace a function "f" you first need to get a key for it by using :
-
---
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
deleted file mode 100644
index 908296ac..00000000
--- a/debian/patches/0003-Fix-build-with-camlp5-6.02.1.patch
+++ /dev/null
@@ -1,155 +0,0 @@
-From: Stephane Glondu <steph@glondu.net>
-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
deleted file mode 100644
index 7ce5e4c8..00000000
--- a/debian/patches/series
+++ /dev/null
@@ -1,3 +0,0 @@
-0001-Disable-micromega-tests.patch
-0002-Remove-dependency-to-Unix-from-module-Profile.patch
-0003-Fix-build-with-camlp5-6.02.1.patch
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 10:00:34 +0000