[why] - Since 2.26 FTBFS, try latest upstream (2.28). - Rebase Makefile.in patch. - Fix(?) test result. -

[Richard W.M. Jones]

commit 8df1e20e7d17b74c322a91f1a81691da2a61bad9
Author: Richard W.M. Jones <rjones at redhat.com>
Date:   Fri Jan 21 18:39:12 2011 +0000

    - Since 2.26 FTBFS, try latest upstream (2.28).
    - Rebase Makefile.in patch.
    - Fix(?) test result.
    - No libdir/frama-c directory is created any more.

 .gitignore                 |    1 +
 min_why.why.result         |    4 ----
 sources                    |    2 +-
 why-2.26-Makefile.in.patch |   22 ----------------------
 why-2.28-Makefile.in.patch |   20 ++++++++++++++++++++
 why.spec                   |   16 +++++++++++-----
 6 files changed, 33 insertions(+), 32 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index 23521f0..2381cf1 100644
--- a/.gitignore
+++ b/.gitignore
@@ -2,3 +2,4 @@ krakatoa.pdf
 why-2.23.tar.gz
 /krakatoa.pdf
 /why-2.26.tar.gz
+/why-2.28.tar.gz
diff --git a/min_why.why.result b/min_why.why.result
index f10fc4a..04848f9 100644
--- a/min_why.why.result
+++ b/min_why.why.result
@@ -24,10 +24,6 @@ logic sub_int : int, int -> int
 
 logic mul_int : int, int -> int
 
-logic div_int : int, int -> int
-
-logic mod_int : int, int -> int
-
 logic neg_int : int -> int
 
 predicate zwf_zero(a: int, b: int) = ((0 <= b) and (a < b))
diff --git a/sources b/sources
index d818982..77a847d 100644
--- a/sources
+++ b/sources
@@ -1,2 +1,2 @@
 14563361a9427e58115825b4e782d23e  krakatoa.pdf
-ae10d920c6919aa30934e7383b260d6b  why-2.26.tar.gz
+c1fec836b51a5a10d30da82cfe3bbbb9  why-2.28.tar.gz
diff --git a/why-2.28-Makefile.in.patch b/why-2.28-Makefile.in.patch
new file mode 100644
index 0000000..f94625b
--- /dev/null
+++ b/why-2.28-Makefile.in.patch
@@ -0,0 +1,20 @@
+--- why-2.28.old/Makefile.in	2010-12-17 20:06:44.000000000 +0000
++++ why-2.28/Makefile.in	2011-01-21 18:32:55.262077657 +0000
+@@ -843,14 +843,9 @@
+ 	cp -f $(V7FILES) $(LIBDIR)/why/coq7
+ 	cp -f $(VO7) $(LIBDIR)/why/coq7
+ install-coq-v8 install-coq-v8.1:
+-	if test -w $(COQLIB) ; then \
+-	  mkdir -p $(COQLIB)/user-contrib/Why ; \
+-	  cp -f $(VO8) $(COQLIB)/user-contrib/Why ; \
+-	else \
+-	  echo "Cannot copy to Coq standard library. Add \"-R $(LIBDIR)/why/coq Why\" to Coq options." ;\
+-	mkdir -p $(LIBDIR)/why/coq ;\
+-	cp -f $(VO8) $(V8FILES) $(LIBDIR)/why/coq ;\
+-	fi
++	mkdir -p $(COQLIB)/user-contrib/Why
++	cp -f $(V8FILES) $(COQLIB)/user-contrib/Why
++	cp -f $(VO8) $(COQLIB)/user-contrib/Why
+ 
+ install-pvs-no:
+ install-pvs-yes: $(PVSFILES)
diff --git a/why.spec b/why.spec
index bdf6d50..bf6c876 100644
--- a/why.spec
+++ b/why.spec
@@ -1,6 +1,6 @@
 Name:           why
-Version:        2.26
-Release:        2%{?dist}
+Version:        2.28
+Release:        1%{?dist}
 Summary:        Software verification platform
 
 Group:          Applications/Engineering
@@ -25,7 +25,7 @@ Source13:       patch_jessie_pvs
 # about when bad parameters are passed to it - this patch fixes that.
 # Upstream has been informed about this issue and a better fix is on
 # their todo list
-Patch0:         gwhy-%{version}.patch
+Patch0:         gwhy-2.26.patch
 
 # This patch makes a Fedora-specific fix to eliminate checking for the
 # location of Coq - since we're using the coq package, we know where
@@ -33,7 +33,7 @@ Patch0:         gwhy-%{version}.patch
 # It also makes a fix necessary to correctly build the bytecode only
 # version of why by building the make_float_model tool correctly in
 # this case.
-Patch1:         why-%{version}-Makefile.in.patch
+Patch1:         why-2.28-Makefile.in.patch
 
 BuildRoot:      %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
 BuildRequires:  ocaml >= 3.09, ocaml-camlp4-devel, gtk2-devel
@@ -276,7 +276,7 @@ sed -e "/ENABLE_JESSIE=yes/d" -i /usr/share/frama-c/known_plugins.ac
 %files
 %defattr(-,root,root,-)
 %{_bindir}/*
-%{_libdir}/frama-c/*
+#%{_libdir}/frama-c/*
 %{_libdir}/caduceus/*
 %{_libdir}/coq/*
 %{_libdir}/jessie/*
@@ -328,6 +328,12 @@ sed -e "/ENABLE_JESSIE=yes/d" -i /usr/share/frama-c/known_plugins.ac
 
 
 %changelog
+* Fri Jan 21 2011 Richard W.M. Jones <rjones at gmail.com> - 2.28-1
+- Since 2.26 FTBFS, try latest upstream (2.28).
+- Rebase Makefile.in patch.
+- Fix(?) test result.
+- No libdir/frama-c directory is created any more.
+
 * Fri Jan 21 2011 Richard W.M. Jones <rjones at gmail.com> - 2.26-2
 - Bump and rebuild for OCaml 3.12.