[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