diff --git a/gwhy-2.33.patch b/gwhy-2.33.patch index d106a7e..d55b90f 100644 --- a/gwhy-2.33.patch +++ b/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 diff --git a/why-flocq23.patch b/why-flocq23.patch deleted file mode 100644 index b54d85a..0000000 --- a/why-flocq23.patch +++ /dev/null @@ -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)). diff --git a/why-flocq24.patch b/why-flocq24.patch new file mode 100644 index 0000000..e4f10a4 --- /dev/null +++ b/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)). diff --git a/why.spec b/why.spec index 8ca5b82..1d540ed 100644 --- a/why.spec +++ b/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 -Patch2: %{name}-flocq23.patch +# Adapt to flocq 2.4.0 +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 - 2.34-13 +- Fix gwhy-2.33.patch (bz 1164470) + +* Thu Nov 13 2014 Richard W.M. Jones - 2.34-12 +- Bump and rebuild for broken dependencies. + +* Thu Oct 30 2014 Jerry James - 2.34-11 +- Rebuild for coq 8.4pl5 + +* Thu Sep 18 2014 Jerry James - 2.34-10 +- Rebuild for why3 0.85 + +* Mon Sep 8 2014 Jerry James - 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 - 2.34-8 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild + * Tue Jun 24 2014 Jerry James - 2.34-7 - Omit "-z now" when building with relro (bz 1105265) - Resolve a conflict between Frama-C and why modules both named "Project"