diff -Nru why-2.30+dfsg/debian/changelog why-2.30+dfsg/debian/changelog --- why-2.30+dfsg/debian/changelog 2012-01-02 14:57:17.000000000 +0000 +++ why-2.30+dfsg/debian/changelog 2012-01-16 18:04:11.000000000 +0000 @@ -1,3 +1,22 @@ +why (2.30+dfsg-3) unstable; urgency=high + + * Fix 0002-Mark-alt-ergo-0.93-as-compatible.patch + - Adapt version_regexp because "alt-ergo -version" changed. + * Fix 0004-Default-to-why2-for-jessie-atp.patch + - default to "gui" instead of "why2". + * Add 0007-Replace-caduceus-invocation-by-Frama-C.patch + - Caduceus is gone. We use Frama-C instead. + - Adding Frama-C to Why's dependencies. + * Setting urgency to "high" to fix those issues. + + -- Mehdi Dogguy Mon, 16 Jan 2012 18:19:38 +0100 + +why (2.30+dfsg-2) unstable; urgency=low + + * Rebuilt with latest coq-float 1:8.3pl1-1 (no source changes). + + -- Mehdi Dogguy Thu, 12 Jan 2012 17:50:39 +0100 + why (2.30+dfsg-1) unstable; urgency=low * New upstream release. diff -Nru why-2.30+dfsg/debian/control why-2.30+dfsg/debian/control --- why-2.30+dfsg/debian/control 2012-01-02 14:57:17.000000000 +0000 +++ why-2.30+dfsg/debian/control 2012-01-16 18:04:11.000000000 +0000 @@ -30,6 +30,7 @@ ${shlibs:Depends}, ${ocaml:Depends}, ${misc:Depends}, + frama-c-base (= ${F:FramaCVersion}), make Suggests: libwhy-coq (= ${binary:Version}) Recommends: alt-ergo diff -Nru why-2.30+dfsg/debian/patches/0002-Mark-alt-ergo-0.93-as-compatible.patch why-2.30+dfsg/debian/patches/0002-Mark-alt-ergo-0.93-as-compatible.patch --- why-2.30+dfsg/debian/patches/0002-Mark-alt-ergo-0.93-as-compatible.patch 2012-01-02 14:57:17.000000000 +0000 +++ why-2.30+dfsg/debian/patches/0002-Mark-alt-ergo-0.93-as-compatible.patch 2012-01-16 18:00:11.000000000 +0000 @@ -3,18 +3,20 @@ Subject: Mark alt-ergo > 0.93 as compatible --- - tools/dpConfig.ml | 2 +- - 1 files changed, 1 insertions(+), 1 deletions(-) + tools/dpConfig.ml | 4 ++-- + 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tools/dpConfig.ml b/tools/dpConfig.ml -index 66be764..da10db6 100644 +index 66be764..ca83a38 100644 --- a/tools/dpConfig.ml +++ b/tools/dpConfig.ml -@@ -84,7 +84,7 @@ let alt_ergo = +@@ -83,8 +83,8 @@ let alt_ergo = + is_interactive = false; version = ""; version_switch = "-version"; - version_regexp = ".*Ergo \\([^ ]*\\)"; +- version_regexp = ".*Ergo \\([^ ]*\\)"; - versions_ok = ["0.93"]; ++ version_regexp = "\\([^ ]*\\)"; + versions_ok = ["0.93"; "0.93.1"; "0.94"]; versions_old = ["0.8"; "0.9" ; "0.91"; "0.92.1"; "0.92.2" ]; command = "alt-ergo"; diff -Nru why-2.30+dfsg/debian/patches/0004-Default-to-why2-for-jessie-atp.patch why-2.30+dfsg/debian/patches/0004-Default-to-why2-for-jessie-atp.patch --- why-2.30+dfsg/debian/patches/0004-Default-to-why2-for-jessie-atp.patch 2012-01-02 14:57:17.000000000 +0000 +++ why-2.30+dfsg/debian/patches/0004-Default-to-why2-for-jessie-atp.patch 2012-01-16 18:00:11.000000000 +0000 @@ -7,7 +7,7 @@ 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/frama-c-plugin/jessie_options.ml b/frama-c-plugin/jessie_options.ml -index 8e57656..8da0b66 100644 +index 8e57656..ce0e99c 100644 --- a/frama-c-plugin/jessie_options.ml +++ b/frama-c-plugin/jessie_options.ml @@ -175,7 +175,7 @@ module Atp = @@ -15,7 +15,7 @@ let option_name = "-jessie-atp" let module_name = "-jessie-atp" - let default = "why3ml" -+ let default = "why2" ++ let default = "gui" let arg_name = "" let help = "use given automated theorem prover, among `alt-ergo', `cvc3', `simplify', `vampire', `yices' and `z3'. Use `goals' to simply generate goals in Why syntax." let kind = `Tuning diff -Nru why-2.30+dfsg/debian/patches/0007-Replace-caduceus-invocation-by-Frama-C.patch why-2.30+dfsg/debian/patches/0007-Replace-caduceus-invocation-by-Frama-C.patch --- why-2.30+dfsg/debian/patches/0007-Replace-caduceus-invocation-by-Frama-C.patch 1970-01-01 00:00:00.000000000 +0000 +++ why-2.30+dfsg/debian/patches/0007-Replace-caduceus-invocation-by-Frama-C.patch 2012-01-16 18:00:27.000000000 +0000 @@ -0,0 +1,24 @@ +From: Mehdi Dogguy +Date: Mon, 16 Jan 2012 18:19:16 +0100 +Subject: Replace caduceus invocation by Frama-C + +--- + bin/gwhy.sh | 4 +--- + 1 files changed, 1 insertions(+), 3 deletions(-) + +diff --git a/bin/gwhy.sh b/bin/gwhy.sh +index 35c487e..f7d7a6b 100755 +--- a/bin/gwhy.sh ++++ b/bin/gwhy.sh +@@ -13,9 +13,7 @@ case $1 in + make -f $b.makefile gui + ;; + *.c) +- b=`basename $1 .c` +- caduceus -why-opt -split-user-conj $1 || exit 1 +- make -f $b.makefile gui ++ frama-c -jessie -jessie-why-opt="-split-user-conj" $1 || exit 1 + ;; + *.jc) + b=`basename $1 .jc` +-- diff -Nru why-2.30+dfsg/debian/patches/series why-2.30+dfsg/debian/patches/series --- why-2.30+dfsg/debian/patches/series 2012-01-02 14:57:17.000000000 +0000 +++ why-2.30+dfsg/debian/patches/series 2012-01-16 18:00:11.000000000 +0000 @@ -4,3 +4,4 @@ 0004-Default-to-why2-for-jessie-atp.patch 0005-Fix-Jc_annot_inference-use-old_reg_pos.patch 0006-Fix-spelling-error-in-binary.patch +0007-Replace-caduceus-invocation-by-Frama-C.patch diff -Nru why-2.30+dfsg/debian/rules why-2.30+dfsg/debian/rules --- why-2.30+dfsg/debian/rules 2012-01-02 14:57:17.000000000 +0000 +++ why-2.30+dfsg/debian/rules 2012-01-16 18:00:11.000000000 +0000 @@ -8,6 +8,7 @@ WHYDIR = $(CURDIR)/debian/why FRAMADIR = $(WHYDIR)/$(shell frama-c -print-plugin-path) +FRAMAVER = $(shell dpkg-query -W -f='$${Version}' frama-c-base) VERSION = $(shell cat Version | grep ^VERSION | cut -d= -f 2) export OCAMLINIT_SED += -e 's/@VERSION@/$(VERSION)/g' @@ -41,6 +42,7 @@ #Jessie.cma is installed, no need for this extra file -$(RM) -f $(FRAMADIR)/Jessie.cmo echo 'F:CoqABI=$(COQ_ABI)' >> debian/libwhy-coq.substvars + echo 'F:FramaCVersion=$(FRAMAVER)' >> debian/why.substvars override_dh_compress: dh_compress -X.v -X.sx -X.why