[Pkg-ocaml-maint-commits] [SCM] why packaging branch, master, updated. debian/2.23+dfsg-2-7-g1583277

Mehdi Dogguy mehdi at debian.org
Tue Apr 27 14:41:33 UTC 2010 

The following commit has been merged in the master branch:
commit 104157ee8874b1b0b52f9c98dfb6a6bc660749f9
Author: Mehdi Dogguy <mehdi at debian.org>
Date:   Tue Apr 27 12:05:15 2010 +0200

    Update patches

diff --git a/debian/changelog b/debian/changelog
index 1dd767f..68bd4aa 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,8 +1,10 @@
 why (2.25+dfsg-1) UNRELEASED; urgency=low
 
   * New upstream release
+    - Refresh patches
+    - Remove 0004-Use-tools-make_float_model.ocamlbest-instead-of-opt-.patch
 
- -- Mehdi Dogguy <mehdi at debian.org>  Mon, 26 Apr 2010 22:25:26 +0200
+ -- Mehdi Dogguy <mehdi at debian.org>  Tue, 27 Apr 2010 12:34:21 +0200
 
 why (2.23+dfsg-2) unstable; urgency=low
 
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
index 03b4128..c83b6f9 100644
--- 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
@@ -10,7 +10,7 @@ diff --git a/Makefile.in b/Makefile.in
 index 15b604b..1ff1a91 100644
 --- a/Makefile.in
 +++ b/Makefile.in
-@@ -747,7 +747,7 @@ bench-tc:: $(BINARY) $(WHYVO)
+@@ -731,7 +731,7 @@ bench-tc:: $(BINARY) $(WHYVO)
  	cd bench; sh ./bench "../$(BINARY) -tc"
  
  test:: $(BINARY) $(WHYVO)
diff --git a/debian/patches/0002-Enable-Apron-support.patch b/debian/patches/0002-Enable-Apron-support.patch
index b3aeaa8..898272d 100644
--- a/debian/patches/0002-Enable-Apron-support.patch
+++ b/debian/patches/0002-Enable-Apron-support.patch
@@ -1,28 +1,41 @@
-From: Samuel Mimram <samuel.mimram at ens-lyon.org>
-Date: Sun, 17 Jan 2010 18:51:03 +0100
+From fa76edb5e371fd81d8a28ecbcec4d12e86b8261f Mon Sep 17 00:00:00 2001
+From: Mehdi Dogguy <mehdi at debian.org>
+Date: Tue, 27 Apr 2010 12:22:38 +0200
 Subject: [PATCH] Enable Apron support
 
 ---
- configure.in |    4 ++--
- 1 files changed, 2 insertions(+), 2 deletions(-)
+ configure.in |    6 +++---
+ 1 files changed, 3 insertions(+), 3 deletions(-)
 
 diff --git a/configure.in b/configure.in
-index d08df14..7d0b77b 100644
+index d5162f7..27b3e89 100644
 --- a/configure.in
 +++ b/configure.in
-@@ -252,12 +252,12 @@ AC_ARG_ENABLE(apron,[  --enable-apron=[no/yes]  use APRON library for abstract i
+@@ -264,7 +264,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(/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)
-+      AC_CHECK_FILE(/usr/lib/ocaml/apron/apron.cma,APRONLIB="-I +apron",APRONLIB=no)
+       AC_CHECK_FILE(/usr/lib/apron.cmxa,APRONLIB="-I /usr/lib -I /usr/local/lib",APRONLIB=no)
        if test "$APRONLIB" = no ; then	
- 	 AC_MSG_ERROR(Cannot find APRON library.)
-       fi		     
-    fi
+@@ -275,7 +275,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 oct.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=""
+@@ -544,4 +544,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)"
 -- 
+1.7.0
+
diff --git a/debian/patches/0003-Fix-spelling-errors.patch b/debian/patches/0003-Fix-spelling-errors.patch
index 27f30ba..fc0dd46 100644
--- a/debian/patches/0003-Fix-spelling-errors.patch
+++ b/debian/patches/0003-Fix-spelling-errors.patch
@@ -26,7 +26,7 @@ diff --git a/jc/jc_typing.ml b/jc/jc_typing.ml
 index c217377..4fae30d 100644
 --- a/jc/jc_typing.ml
 +++ b/jc/jc_typing.ml
-@@ -3313,7 +3313,7 @@ of an invariant policy";
+@@ -3278,7 +3278,7 @@ of an invariant policy";
                | "cni", [_;_] -> `Cni
  
                | ("inc"|"cni"), _ -> typing_error loc "A Gen_separation inc or cni pragma should have 2 arguments (%i given)" (List.length li)
@@ -48,17 +48,4 @@ index 476d33e..6d5e60d 100644
  
  let rec get_record_labels ty tenv =
    match get_type_descr ty tenv with
-diff --git a/tools/dp.ml b/tools/dp.ml
-index d5fb25f..ad9f498 100644
---- a/tools/dp.ml
-+++ b/tools/dp.ml
-@@ -65,7 +65,7 @@ let spec =
-     "-select", Arg.Set select_hypotheses, 
-     "applies some selection of hypotheses (only Alt-Ergo)";
-     "-simple", Arg.Set simple, "Print only Valid, I don't know, Invalid, Fail, Timeout";
--    "-split", Arg.Set split, "Create a directory wich contains all the goal splitted in different file"
-+    "-split", Arg.Set split, "Create a directory wich contains all the goal split in different file"
-   ]
- 
- let () = 
 -- 
diff --git a/debian/patches/0004-Use-tools-make_float_model.ocamlbest-instead-of-opt-.patch b/debian/patches/0004-Use-tools-make_float_model.ocamlbest-instead-of-opt-.patch
deleted file mode 100644
index 02a908e..0000000
--- a/debian/patches/0004-Use-tools-make_float_model.ocamlbest-instead-of-opt-.patch
+++ /dev/null
@@ -1,32 +0,0 @@
-From: Mehdi Dogguy <mehdi at debian.org>
-Date: Sun, 24 Jan 2010 21:05:55 +0100
-Subject: [PATCH] Use tools/make_float_model.ocamlbest instead of opt version
-
----
- Makefile.in |   11 +++++++----
- 1 files changed, 7 insertions(+), 4 deletions(-)
-
-diff --git a/Makefile.in b/Makefile.in
-index 1ff1a91..5b749ac 100644
---- a/Makefile.in
-+++ b/Makefile.in
-@@ -653,11 +653,14 @@ bin/cadlog.opt: src/version.cmx c/cversion.cmx tools/cadlog.cmx
- tools/make_float_model.opt: tools/make_float_model.cmx
- 	$(OCAMLOPT) -o $@ $^
- 
--lib/why/double_model.why lib/why/double_strict.why: tools/make_float_model.opt
--	tools/make_float_model.opt double 53 -1074
-+tools/make_float_model.byte: tools/make_float_model.cmo
-+	$(OCAMLC) -o $@ $^
- 
--lib/why/single_model.why lib/why/single_strict.why: tools/make_float_model.opt
--	tools/make_float_model.opt single 24 -149
-+lib/why/double_model.why lib/why/double_strict.why: tools/make_float_model.$(OCAMLBEST)
-+	tools/make_float_model.$(OCAMLBEST) double 53 -1074
-+
-+lib/why/single_model.why lib/why/single_strict.why: tools/make_float_model.$(OCAMLBEST)
-+	tools/make_float_model.$(OCAMLBEST) single 24 -149
- 
- 
- static:: $(STATICBINARY)
--- 
diff --git a/debian/patches/0005-Generate-Jessie.cma-for-bytecode-only-architectures.patch b/debian/patches/0005-Generate-Jessie.cma-for-bytecode-only-architectures.patch
index c923670..6f47cc2 100644
--- a/debian/patches/0005-Generate-Jessie.cma-for-bytecode-only-architectures.patch
+++ b/debian/patches/0005-Generate-Jessie.cma-for-bytecode-only-architectures.patch
@@ -10,7 +10,7 @@ diff --git a/Makefile.in b/Makefile.in
 index 5b749ac..1270548 100644
 --- a/Makefile.in
 +++ b/Makefile.in
-@@ -371,7 +371,7 @@ ifeq ($(FRAMAC),yes)
+@@ -365,7 +365,7 @@ ifeq ($(FRAMAC),yes)
  JESSIE_PLUGIN_PATH=frama-c-plugin
  $(JESSIE_PLUGIN_BYTE): jc/jc.cmo $(JCCMO) $(CMO)
  	$(MAKE) -C $(JESSIE_PLUGIN_PATH) depend
diff --git a/debian/patches/0006-Coq-float-can-be-in-coqlib-user-contrib-Float.patch b/debian/patches/0006-Coq-float-can-be-in-coqlib-user-contrib-Float.patch
index 1e9eb6a..3ae6d70 100644
--- a/debian/patches/0006-Coq-float-can-be-in-coqlib-user-contrib-Float.patch
+++ b/debian/patches/0006-Coq-float-can-be-in-coqlib-user-contrib-Float.patch
@@ -10,7 +10,7 @@ diff --git a/configure.in b/configure.in
 index 7d0b77b..e7f0cd8 100644
 --- a/configure.in
 +++ b/configure.in
-@@ -334,7 +334,7 @@ else
+@@ -375,5 +375,5 @@ else
  	AC_MSG_CHECKING(Coq floating-point library)
   	case $COQVERSION in
  	   8.2*|trunk)
diff --git a/debian/patches/series b/debian/patches/series
index 2f183b2..9f8208b 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -1,6 +1,5 @@
 0001-Do-not-run-tests-on-non-existant-files.patch
 0002-Enable-Apron-support.patch
 0003-Fix-spelling-errors.patch
-0004-Use-tools-make_float_model.ocamlbest-instead-of-opt-.patch
 0005-Generate-Jessie.cma-for-bytecode-only-architectures.patch
 0006-Coq-float-can-be-in-coqlib-user-contrib-Float.patch

-- 
why packaging

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