Fix gwhy-2.33.patch (bz 1164470).

(cherry picked from commit 8329d966f9)

gwhy-2.33.patch

@@ -22,7 +22,7 @@
          echo "cd $d"
          cd $d
  	jessie -locs $b.jloc -why-opt -split-user-conj $b.jc || exit 2
-@@ -13,18 +19,20 @@
+@@ -13,18 +19,22 @@
  	make -f $b.makefile gui
  	;;
    *.c)
@@ -38,12 +38,14 @@
    *.mlw|*.why)
 -	gwhy-bin -split-user-conj $1
 +	gwhy-bin -split-user-conj $file
- 	;;
++	;;
 +  ?*)
 +	echo "$file does not have file type extension recognized by gwhy"
+	;;
    *)
 -	echo "don't know what to do with $1"
 +	echo "gwhy needs the name of a file to inspect in order to run"
++	;;
  esac
  
  

why-flocq23.patch

@@ -1,11 +0,0 @@
---- lib/coq/WhyFloats.v.orig	2014-03-17 16:01:46.000000000 -0600
-+++ lib/coq/WhyFloats.v	2014-04-21 15:39:55.680771647 -0600
-@@ -108,7 +108,7 @@
- generalize (Zeq_bool_eq _ _ H1). clear.
- rewrite Fcalc_digits.Z_of_nat_S_digits2_Pnat.
- intros H.
--apply (Fcalc_digits.Zpower_gt_Zdigits Fcalc_digits.radix2 (Zpos prec) (Zpos m)).
-+apply (Fcore_digits.Zpower_gt_Zdigits Fcalc_digits.radix2 (Zpos prec) (Zpos m)).
- revert H.
- unfold FLT_exp.
- generalize (Fcore_digits.Zdigits radix2 (Zpos m)).

why-flocq24.patch

@@ -0,0 +1,14 @@
+--- ./lib/coq/WhyFloats.v.orig	2014-03-17 16:01:46.000000000 -0600
++++ ./lib/coq/WhyFloats.v	2014-09-02 17:40:03.356028320 -0600
+@@ -106,9 +106,9 @@ apply Zlt_succ_le.
+ change (Zpos m < Zsucc (Zpred (Zpower_pos 2 prec)))%Z.
+ rewrite <- Zsucc_pred.
+ generalize (Zeq_bool_eq _ _ H1). clear.
+-rewrite Fcalc_digits.Z_of_nat_S_digits2_Pnat.
++rewrite Fcore_digits.Zpos_digits2_pos.
+ intros H.
+-apply (Fcalc_digits.Zpower_gt_Zdigits Fcalc_digits.radix2 (Zpos prec) (Zpos m)).
++apply (Fcore_digits.Zpower_gt_Zdigits Fcore_Zaux.radix2 (Zpos prec) (Zpos m)).
+ revert H.
+ unfold FLT_exp.
+ generalize (Fcore_digits.Zdigits radix2 (Zpos m)).

why.spec

@@ -10,7 +10,7 @@
 
 Name:           why
 Version:        2.34
-Release:        7%{?dist}
+Release:        13%{?dist}
 Summary:        Software verification platform
 
 License:        LGPLv2 with exceptions
@@ -47,8 +47,8 @@ Patch0:         gwhy-2.33.patch
 # this case.
 Patch1:         %{name}-2.34-Makefile.in.patch
 
-# Adapt to flocq 2.3.0
+# Adapt to flocq 2.4.0
-Patch2:         %{name}-flocq23.patch
+Patch2:         %{name}-flocq24.patch
 
 # Avoid a clash between Frama-C and why modules both named "Project".
 # Sent upstream 26 Jun 2014.
@@ -57,7 +57,7 @@ Patch3:         %{name}-project.patch
 BuildRequires:  auto-destdir
 BuildRequires:  cvc3
 BuildRequires:  desktop-file-utils
-BuildRequires:  emacs-nox xemacs xemacs-packages-extra
+BuildRequires:  emacs xemacs xemacs-packages-extra
 BuildRequires:  frama-c-devel
 BuildRequires:  gappalib-coq
 BuildRequires:  gtk2-devel
@@ -260,6 +260,9 @@ sed -e 's/command = "pvs"/command = "pvs-sbcl"/' \
     -i tools/dpConfig.ml
 sed -i 's/pvs/pvs-sbcl/' configure
 
+# Build with why3 0.85
+sed -i 's/0\.83/0.85/' configure
+
 %build
 %if ! %{opt}
 %global opt_option OCAMLBEST=byte OCAMLC=ocamlc OCAMLDEP=ocamldep OCAMLYACC=ocamlyacc OCAMLLEX=ocamllex
@@ -311,7 +314,7 @@ cp -p %{SOURCE12}             %{buildroot}%{_bindir}/
 mkdir -p %{buildroot}%{why_examples_dir}mlw/
 mkdir -p %{buildroot}%{why_examples_dir}c/
 cp -p doc/manual.ps %{buildroot}%{why_doc_dir}/why-manual.ps
-cp -p %{SOURCE8} %{SOURCE3} CHANGES COPYING LICENSE README Version %{buildroot}%{why_doc_dir}
+cp -p %{SOURCE8} %{SOURCE3} CHANGES README Version %{buildroot}%{why_doc_dir}
 
 # Copy in the example files, leaving behind all generated files
 cd examples
@@ -375,6 +378,7 @@ touch --no-create %{_datadir}/icons/hicolor &>/dev/null
 gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || :
 
 %files
+%license COPYING LICENSE
 %{_bindir}/*
 %{_libdir}/why/
 %{_mandir}/man1/why.1*
@@ -432,6 +436,26 @@ gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || :
 
 
 %changelog
+* Sat Nov 15 2014 Jerry James <loganjerry@gmail.com> - 2.34-13
+- Fix gwhy-2.33.patch (bz 1164470)
+
+* Thu Nov 13 2014 Richard W.M. Jones <rjones@redhat.com> - 2.34-12
+- Bump and rebuild for broken dependencies.
+
+* Thu Oct 30 2014 Jerry James <loganjerry@gmail.com> - 2.34-11
+- Rebuild for coq 8.4pl5
+
+* Thu Sep 18 2014 Jerry James <loganjerry@gmail.com> - 2.34-10
+- Rebuild for why3 0.85
+
+* Mon Sep  8 2014 Jerry James <loganjerry@gmail.com> - 2.34-9
+- Rebuild for flocq 2.4.0 and why3 0.84
+- Fix license handling
+- BR emacs instead of emacs-nox
+
+* Mon Aug 18 2014 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.34-8
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild
+
 * Tue Jun 24 2014 Jerry James <loganjerry@gmail.com> - 2.34-7
 - Omit "-z now" when building with relro (bz 1105265)
 - Resolve a conflict between Frama-C and why modules both named "Project"