From d9e6e7f8c318e9a08d5b7d5abb6db4a64a4e60b4 Mon Sep 17 00:00:00 2001 From: Peter Robinson Date: Mon, 18 Aug 2014 08:34:56 +0000 Subject: [PATCH 1/7] - Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild --- why.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/why.spec b/why.spec index 8ca5b82..17c8393 100644 --- a/why.spec +++ b/why.spec @@ -10,7 +10,7 @@ Name: why Version: 2.34 -Release: 7%{?dist} +Release: 8%{?dist} Summary: Software verification platform License: LGPLv2 with exceptions @@ -432,6 +432,9 @@ gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || : %changelog +* 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" From dcfb5e236969d54c55ef3fd28f176353d12cb3a5 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 8 Sep 2014 14:11:02 -0600 Subject: [PATCH 2/7] Rebuild for flocq 2.4.0 and why3 0.84. Fix license handling. BR emacs instead of emacs-nox. --- why-flocq23.patch | 11 ----------- why-flocq24.patch | 14 ++++++++++++++ why.spec | 19 ++++++++++++++----- 3 files changed, 28 insertions(+), 16 deletions(-) delete mode 100644 why-flocq23.patch create mode 100644 why-flocq24.patch 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 17c8393..8c9f6b4 100644 --- a/why.spec +++ b/why.spec @@ -10,7 +10,7 @@ Name: why Version: 2.34 -Release: 8%{?dist} +Release: 9%{?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.84 +sed -i 's/0\.83/0.84/' 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,11 @@ gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || : %changelog +* 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 From f4fe84ba98a9a000d8a069faa69a2d37ce1713b8 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 18 Sep 2014 15:29:20 -0600 Subject: [PATCH 3/7] Rebuild for why3 0.85. --- why.spec | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/why.spec b/why.spec index 8c9f6b4..acbd6c9 100644 --- a/why.spec +++ b/why.spec @@ -10,7 +10,7 @@ Name: why Version: 2.34 -Release: 9%{?dist} +Release: 10%{?dist} Summary: Software verification platform License: LGPLv2 with exceptions @@ -260,8 +260,8 @@ sed -e 's/command = "pvs"/command = "pvs-sbcl"/' \ -i tools/dpConfig.ml sed -i 's/pvs/pvs-sbcl/' configure -# Build with why3 0.84 -sed -i 's/0\.83/0.84/' configure +# Build with why3 0.85 +sed -i 's/0\.83/0.85/' configure %build %if ! %{opt} @@ -436,6 +436,9 @@ gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || : %changelog +-* 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 From 47b0b9b08248f1a81d411dad18350cf454047362 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 18 Sep 2014 15:30:16 -0600 Subject: [PATCH 4/7] Fix fat-fingered changelog entry. --- why.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/why.spec b/why.spec index acbd6c9..d361a45 100644 --- a/why.spec +++ b/why.spec @@ -436,7 +436,7 @@ gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || : %changelog --* Thu Sep 18 2014 Jerry James - 2.34-10 +* Thu Sep 18 2014 Jerry James - 2.34-10 - Rebuild for why3 0.85 * Mon Sep 8 2014 Jerry James - 2.34-9 From e831eedffd90bd86d1403b376bd115e590702337 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 7 Nov 2014 09:06:25 -0700 Subject: [PATCH 5/7] Rebuild for coq 8.4pl5. --- why.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/why.spec b/why.spec index d361a45..23e1f45 100644 --- a/why.spec +++ b/why.spec @@ -10,7 +10,7 @@ Name: why Version: 2.34 -Release: 10%{?dist} +Release: 11%{?dist} Summary: Software verification platform License: LGPLv2 with exceptions @@ -436,6 +436,9 @@ gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || : %changelog +* 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 From 912790a954d5b7a495360e3b0a9e1876b62fdb1c Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Thu, 13 Nov 2014 13:34:46 +0000 Subject: [PATCH 6/7] Bump and rebuild for broken dependencies. (cherry picked from commit 8329d966f92a9bbfbcafbe4cbb177a5cddfc44cd) --- why.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/why.spec b/why.spec index 23e1f45..fa5ff70 100644 --- a/why.spec +++ b/why.spec @@ -10,7 +10,7 @@ Name: why Version: 2.34 -Release: 11%{?dist} +Release: 12%{?dist} Summary: Software verification platform License: LGPLv2 with exceptions @@ -436,6 +436,9 @@ gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || : %changelog +* 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 From aac0cc5d5cbc4718ff0adb9cd434477953478d9a Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sat, 15 Nov 2014 15:31:25 -0700 Subject: [PATCH 7/7] Fix gwhy-2.33.patch (bz 1164470). --- gwhy-2.33.patch | 6 ++++-- why.spec | 5 ++++- 2 files changed, 8 insertions(+), 3 deletions(-) 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.spec b/why.spec index fa5ff70..1d540ed 100644 --- a/why.spec +++ b/why.spec @@ -10,7 +10,7 @@ Name: why Version: 2.34 -Release: 12%{?dist} +Release: 13%{?dist} Summary: Software verification platform License: LGPLv2 with exceptions @@ -436,6 +436,9 @@ 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.