[Pkg-ocaml-maint-commits] [SCM] why packaging branch, master, updated. debian/2.26+dfsg-4-8-gf677c3a

Mehdi Dogguy mehdi at debian.org
Sun Apr 24 21:40:06 UTC 2011


The following commit has been merged in the master branch:
commit 803f7b7acf5b92ee48c8ced028e6af49118a82b7
Author: Mehdi Dogguy <mehdi at debian.org>
Date:   Sat Apr 23 19:21:35 2011 +0200

    Remove some old patches

diff --git a/debian/changelog b/debian/changelog
index 5c48c2c..3c55bab 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,8 +1,11 @@
 why (2.29+dfsg-1) unstable; urgency=low
 
   * New upstream release.
+    - Remove old patches, which are not needed anymore.
+    - Remove build-depends on coq-float (upstream switched to Flocq which
+      is not packaged yet).
 
- -- Mehdi Dogguy <mehdi at debian.org>  Sat, 23 Apr 2011 19:18:07 +0200
+ -- Mehdi Dogguy <mehdi at debian.org>  Sat, 23 Apr 2011 19:45:08 +0200
 
 why (2.26+dfsg-4) unstable; urgency=low
 
diff --git a/debian/control b/debian/control
index 692cca3..c9fb630 100644
--- a/debian/control
+++ b/debian/control
@@ -14,7 +14,6 @@ Build-Depends:
   camlp4,
   liblablgtk2-ocaml-dev (>= 2.12.0-3~),
   coq (>= 8.2.pl1~),
-  libfloat-coq (>= 1:8.2-1.2-3~),
   libocamlgraph-ocaml-dev (>= 1.4~),
   frama-c-base (>= 20100401+boron+dfsg-4~),
   libapron-ocaml-dev (>= 0.9.10-4~),
diff --git a/debian/patches/0001-Do-not-run-tests-on-non-existant-files.patch b/debian/patches/0001-Do-not-run-tests-on-non-existant-files.patch
deleted file mode 100644
index 77ceb43..0000000
--- a/debian/patches/0001-Do-not-run-tests-on-non-existant-files.patch
+++ /dev/null
@@ -1,22 +0,0 @@
-From: Mehdi Dogguy <mehdi at debian.org>
-Date: Sun, 10 Jan 2010 21:34:05 +0100
-Subject: [PATCH] Do not run tests on non-existant files
-
----
- Makefile.in |    2 +-
- 1 files changed, 1 insertions(+), 1 deletions(-)
-
-diff --git a/Makefile.in b/Makefile.in
-index c058478..587e8cd 100644
---- a/Makefile.in
-+++ b/Makefile.in
-@@ -735,7 +735,7 @@ bench-tc:: $(BINARY) $(WHYVO)
- 	cd bench; sh ./bench "../$(BINARY) -tc"
- 
- test:: $(BINARY) $(WHYVO)
--	$(BINARY) -d -V -coq bench/test.ml
-+	[ ! -f bench/test.ml ] || $(BINARY) -d -V -coq bench/test.ml
- 
- .PHONY: examples examples-c
- 
--- 
diff --git a/debian/patches/0002-Enable-Apron-support.patch b/debian/patches/0002-Enable-Apron-support.patch
deleted file mode 100644
index 88deac6..0000000
--- a/debian/patches/0002-Enable-Apron-support.patch
+++ /dev/null
@@ -1,38 +0,0 @@
-From: Mehdi Dogguy <mehdi at debian.org>
-Date: Mon, 24 May 2010 23:28:57 +0200
-Subject: [PATCH] Enable Apron support
-
----
- configure.in |    6 +++---
- 1 files changed, 3 insertions(+), 3 deletions(-)
-
-diff --git a/configure.in b/configure.in
-index d931e5b..2d3872a 100644
---- a/configure.in
-+++ b/configure.in
-@@ -261,7 +261,7 @@ APRONLIBS=
- AC_ARG_ENABLE(apron,[  --enable-apron=[no/yes]  use APRON library for abstract interpretation [default=yes]],,enable_apron=$default_apron)
- 
- if test "$enable_apron" = "yes" ; then
--   AC_CHECK_FILE(/usr/local/lib/apron.cmxa,APRONLIB="-I /usr/local/lib -I /usr/lib",APRONLIB=no)
-+   AC_CHECK_FILE($OCAMLLIB/apron/apron.cmxa,APRONLIB="-I +apron",APRONLIB=no)
-    if test "$APRONLIB" = no ; then
-       AC_CHECK_FILE(/usr/lib/apron.cmxa,APRONLIB="-I /usr/lib -I /usr/local/lib",APRONLIB=no)
-       if test "$APRONLIB" = no ; then
-@@ -272,7 +272,7 @@ if test "$enable_apron" = "yes" ; then
- fi
- 
- if test "$enable_apron" = "yes" ; then
--   APRONLIBS="-cclib ' -lpolka_caml -lpolkaMPQ -loct_caml -loctMPQ -lbox_caml -lboxMPQ -lapron_caml -lapron -lgmp_caml -lmpfr -lgmp -lbigarray -lcamlidl' bigarray.cmxa gmp.cmxa apron.cmxa box.cmxa polka.cmxa"
-+   APRONLIBS="-cclib ' -lpolkaMPQ_caml -lpolkaMPQ -loctMPQ_caml -loctMPQ -lboxMPQ_caml -lboxMPQ -lapron_caml -lapron -lgmp_caml -lmpfr -lgmp -lbigarray -lcamlidl' bigarray.cmxa gmp.cmxa apron.cmxa box.cmxa polka.cmxa"
-    ATPCMO=atp/atp.cmo
- else
-    APRONLIB=""
-@@ -541,4 +541,4 @@ if test "$PVS" = "yes" ; then
-    echo "    Lib                  : $PVSLIB"
- fi
- echo "Mizar support            : $MIZAR"
--echo "Other provers support    : at run-time (use why-config to configure)"
-\ No newline at end of file
-+echo "Other provers support    : at run-time (use why-config to configure)"
--- 
diff --git a/debian/patches/0003-Fix-spelling-errors.patch b/debian/patches/0003-Fix-spelling-errors.patch
deleted file mode 100644
index f85054d..0000000
--- a/debian/patches/0003-Fix-spelling-errors.patch
+++ /dev/null
@@ -1,50 +0,0 @@
-From: Mehdi Dogguy <mehdi at debian.org>
-Date: Tue, 1 Jun 2010 21:40:22 +0200
-Subject: [PATCH] Fix spelling errors
-
----
- c/ctyping.ml          |    2 +-
- jc/jc_typing.ml       |    2 +-
- ml/typing/parmatch.ml |    2 +-
- 3 files changed, 3 insertions(+), 3 deletions(-)
-
-diff --git a/c/ctyping.ml b/c/ctyping.ml
-index b921295..94ba6bb 100644
---- a/c/ctyping.ml
-+++ b/c/ctyping.ml
-@@ -353,7 +353,7 @@ let warn_for_read_only loc e =
-   | TEvar (Fun_info _f) ->
-       warning loc ("function assignment (ignored)")
-   | _ when e.texpr_type.ctype_const ->
--      warning loc "assigment of read-only location"
-+      warning loc "assignment of read-only location"
-   | _ -> 
-       ()
- 
-diff --git a/jc/jc_typing.ml b/jc/jc_typing.ml
-index 80d9e3a..7567fa6 100644
---- a/jc/jc_typing.ml
-+++ b/jc/jc_typing.ml
-@@ -3295,7 +3295,7 @@ of an invariant policy";
-                     "A Gen_separation inc or cni pragma should \
-                      have 2 arguments (%i given)" (List.length li)
-               | _ -> typing_error loc 
--                  "I dont know that kind of Gen_separation pragma : %s" kind in
-+                  "I don't know that kind of Gen_separation pragma : %s" kind in
-             create_pragma_gen_sep_logic loc kind id li
-           end;
- 	acc
-diff --git a/ml/typing/parmatch.ml b/ml/typing/parmatch.ml
-index 476d33e..6d5e60d 100644
---- a/ml/typing/parmatch.ml
-+++ b/ml/typing/parmatch.ml
-@@ -135,7 +135,7 @@ let find_label lbl lbls =
-   try
-     let name,_,_ = List.nth lbls lbl.lbl_pos in
-     name
--  with Failure "nth" -> "*Unkown label*"
-+  with Failure "nth" -> "*Unknown label*"
- 
- let rec get_record_labels ty tenv =
-   match get_type_descr ty tenv with
--- 
diff --git a/debian/patches/0004-Generate-Jessie.cma-for-bytecode-only-architectures.patch b/debian/patches/0004-Generate-Jessie.cma-for-bytecode-only-architectures.patch
deleted file mode 100644
index 4d2a654..0000000
--- a/debian/patches/0004-Generate-Jessie.cma-for-bytecode-only-architectures.patch
+++ /dev/null
@@ -1,22 +0,0 @@
-From: Mehdi Dogguy <mehdi at debian.org>
-Date: Sun, 24 Jan 2010 22:52:15 +0100
-Subject: [PATCH] Generate Jessie.cma for bytecode only architectures
-
----
- Makefile.in |    2 +-
- 1 files changed, 1 insertions(+), 1 deletions(-)
-
-diff --git a/Makefile.in b/Makefile.in
-index 587e8cd..0c119dc 100644
---- a/Makefile.in
-+++ b/Makefile.in
-@@ -369,7 +369,7 @@ ifeq ($(FRAMAC),yes)
- JESSIE_PLUGIN_PATH=frama-c-plugin
- $(JESSIE_PLUGIN_BYTE): jc/jc.cmo $(JCCMO) $(CMO)
- 	$(MAKE) -C $(JESSIE_PLUGIN_PATH) depend
--	$(MAKE) -C $(JESSIE_PLUGIN_PATH) Jessie.cmo
-+	$(MAKE) -C $(JESSIE_PLUGIN_PATH) Jessie.cma
- 
- $(JESSIE_PLUGIN_OPT): $(JCLIB) $(JCCMX) $(CMX)
- 	$(MAKE) -C $(JESSIE_PLUGIN_PATH) depend
--- 
diff --git a/debian/patches/0005-Coq-float-can-be-in-coqlib-user-contrib-Float.patch b/debian/patches/0005-Coq-float-can-be-in-coqlib-user-contrib-Float.patch
deleted file mode 100644
index ec5a873..0000000
--- a/debian/patches/0005-Coq-float-can-be-in-coqlib-user-contrib-Float.patch
+++ /dev/null
@@ -1,22 +0,0 @@
-From: Mehdi Dogguy <mehdi at debian.org>
-Date: Wed, 17 Feb 2010 15:37:49 +0100
-Subject: [PATCH] Coq-float can be in coqlib/user-contrib/Float
-
----
- configure.in |    2 +-
- 1 files changed, 1 insertions(+), 1 deletions(-)
-
-diff --git a/configure.in b/configure.in
-index 2d3872a..e8a8f59 100644
---- a/configure.in
-+++ b/configure.in
-@@ -372,7 +372,7 @@ else
- 	AC_MSG_CHECKING(Coq floating-point library)
-  	case $COQVERSION in
- 	   8.2*|trunk)
-- 	      if test -f "$COQLIB/user-contrib/AllFloat.vo"; then
-+ 	      if test -f "$COQLIB/user-contrib/AllFloat.vo" || test -f "$COQLIB/user-contrib/Float/AllFloat.vo"; then
- 	        AC_MSG_RESULT(yes)
- 	  	WHYFLOATS="lib/coq/WhyFloats.vo lib/coq/JessieFloats.vo lib/coq/floats_strict.vo"
- 		COQFLOATSMSG=yes
--- 
diff --git a/debian/patches/0006-Cope-with-OCaml-3.12-s-Map.patch b/debian/patches/0006-Cope-with-OCaml-3.12-s-Map.patch
deleted file mode 100644
index 798293d..0000000
--- a/debian/patches/0006-Cope-with-OCaml-3.12-s-Map.patch
+++ /dev/null
@@ -1,110 +0,0 @@
-From: Stephane Glondu <steph at glondu.net>
-Date: Wed, 16 Jun 2010 07:47:09 +0200
-Subject: [PATCH] Cope with OCaml 3.12's Map
-
-Bug-Debian: http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=585459
-Signed-off-by: Stephane Glondu <steph at glondu.net>
----
- c/cutil.ml      |   19 ++++++++++++++++++-
- c/cutil.mli     |   23 ++++++++++++++++++++---
- jc/jc_stdlib.ml |   15 ++++++++++++++-
- 3 files changed, 52 insertions(+), 5 deletions(-)
-
-diff --git a/c/cutil.ml b/c/cutil.ml
-index c0969d9..3e7b01f 100644
---- a/c/cutil.ml
-+++ b/c/cutil.ml
-@@ -72,12 +72,29 @@ end
- 
- (* commonly used maps/sets based on std lib *)
- 
-+module type MAP = sig
-+  type key
-+  type +'a t
-+  val empty : 'a t
-+  val is_empty : 'a t -> bool
-+  val mem : key -> 'a t -> bool
-+  val add : key -> 'a -> 'a t -> 'a t
-+  val remove : key -> 'a t -> 'a t
-+  val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
-+  val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
-+  val iter : (key -> 'a -> unit) -> 'a t -> unit
-+  val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
-+  val find : key -> 'a t -> 'a
-+  val map : ('a -> 'b) -> 'a t -> 'b t
-+  val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
-+end
-+
- module StringSet = Set.Make (String)
- module StringMap = Map.Make (String)
- module Int32Map = Map.Make (Int32)
- module Int32Set = Set.Make (Int32)
- 
--module Int31Map : Map.S with type key = int = 
-+module Int31Map : MAP with type key = int =
- struct
-   module M = Int32Map
-   let to32 f = fun i32 -> f (Int32.to_int i32)
-diff --git a/c/cutil.mli b/c/cutil.mli
-index 7c27a07..47d3866 100644
---- a/c/cutil.mli
-+++ b/c/cutil.mli
-@@ -47,11 +47,28 @@ module Pair : sig
-       : Set.OrderedType with type t = L1.t * L2.t
- end
- 
-+module type MAP = sig
-+  type key
-+  type +'a t
-+  val empty : 'a t
-+  val is_empty : 'a t -> bool
-+  val mem : key -> 'a t -> bool
-+  val add : key -> 'a -> 'a t -> 'a t
-+  val remove : key -> 'a t -> 'a t
-+  val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
-+  val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
-+  val iter : (key -> 'a -> unit) -> 'a t -> unit
-+  val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
-+  val find : key -> 'a t -> 'a
-+  val map : ('a -> 'b) -> 'a t -> 'b t
-+  val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
-+end
-+
- module StringSet : Set.S with type elt = string
--module StringMap : Map.S with type key = string
--module Int32Map : Map.S with type key = int32
-+module StringMap : MAP with type key = string
-+module Int32Map : MAP with type key = int32
- module Int32Set : Set.S with type elt = int32
--module Int31Map : Map.S with type key = int
-+module Int31Map : MAP with type key = int
- module Int31Set : Set.S with type elt = int
- 
- val list1 : 'a list -> 'a
-diff --git a/jc/jc_stdlib.ml b/jc/jc_stdlib.ml
-index 4efb55f..c9f58d8 100644
---- a/jc/jc_stdlib.ml
-+++ b/jc/jc_stdlib.ml
-@@ -93,7 +93,20 @@ module Map = struct
-   module type OrderedType = Map.OrderedType
- 
-   module type S = sig
--    include Map.S
-+    type key
-+    type +'a t
-+    val empty : 'a t
-+    val is_empty : 'a t -> bool
-+    val mem : key -> 'a t -> bool
-+    val add : key -> 'a -> 'a t -> 'a t
-+    val remove : key -> 'a t -> 'a t
-+    val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
-+    val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
-+    val iter : (key -> 'a -> unit) -> 'a t -> unit
-+    val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
-+    val find : key -> 'a t -> 'a
-+    val map : ('a -> 'b) -> 'a t -> 'b t
-+    val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
-     val elements: 'a t -> (key * 'a) list
-     val keys: 'a t -> key list
-     val values: 'a t -> 'a list
--- 
diff --git a/debian/patches/0007-Squeeze-s-Coq-is-also-compatible.patch b/debian/patches/0007-Squeeze-s-Coq-is-also-compatible.patch
deleted file mode 100644
index 01bdbe3..0000000
--- a/debian/patches/0007-Squeeze-s-Coq-is-also-compatible.patch
+++ /dev/null
@@ -1,22 +0,0 @@
-From: Mehdi Dogguy <mehdi at dogguy.org>
-Date: Thu, 20 Jan 2011 20:56:15 +0100
-Subject: [PATCH] Squeeze's Coq is also compatible
-
----
- tools/dpConfig.ml |    2 +-
- 1 files changed, 1 insertions(+), 1 deletions(-)
-
-diff --git a/tools/dpConfig.ml b/tools/dpConfig.ml
-index b55e8bd..3785a8b 100644
---- a/tools/dpConfig.ml
-+++ b/tools/dpConfig.ml
-@@ -181,7 +181,7 @@ let coq =
-     version = "";
-     version_switch = "-v";
-     version_regexp = "The Coq Proof Assistant, version \\([^ ]+\\)";
--    versions_ok = ["8.0"; "8.1";"8.2";"8.2pl1"];
-+    versions_ok = ["8.0"; "8.1";"8.2";"8.2pl1";"8.2pl2"];
-     versions_old = ["7.4"];
-     command = "coqc";
-     command_switches = "";
--- 
diff --git a/debian/patches/series b/debian/patches/series
index 64b2a84..e69de29 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -1,7 +0,0 @@
-0001-Do-not-run-tests-on-non-existant-files.patch
-0002-Enable-Apron-support.patch
-0003-Fix-spelling-errors.patch
-0004-Generate-Jessie.cma-for-bytecode-only-architectures.patch
-0005-Coq-float-can-be-in-coqlib-user-contrib-Float.patch
-0006-Cope-with-OCaml-3.12-s-Map.patch
-0007-Squeeze-s-Coq-is-also-compatible.patch

-- 
why packaging



More information about the Pkg-ocaml-maint-commits mailing list