diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..71c4898
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,4 @@
+/krakatoa.pdf
+/why-icons.tar.xz
+/why-2.36.tar.gz
+/why-2.38.tar.gz
diff --git a/README.why b/README.why
new file mode 100644
index 0000000..ba95dfa
--- /dev/null
+++ b/README.why
@@ -0,0 +1,8 @@
+Fedora why package:
+
+Contains the main why executable and supporting tools.
+
+Consider visiting the main Why site - http://why.lri.fr - for more
+documentation. Also, there is more information about the tools
+Caduceus and Krakatoa at http://caduceus.lri.fr and
+http://krakatoa.lri.fr respectively.
\ No newline at end of file
diff --git a/README.why-coq.Fedora b/README.why-coq.Fedora
new file mode 100644
index 0000000..406a7a9
--- /dev/null
+++ b/README.why-coq.Fedora
@@ -0,0 +1,6 @@
+Fedora why-coq package:
+
+Contains libraries for interfacing why with Coq.
+
+You shouldn't have to do anything extra - you should now just be able
+to use the Coq-related capabilities of Why.
\ No newline at end of file
diff --git a/dead.package b/dead.package
deleted file mode 100644
index 497866a..0000000
--- a/dead.package
+++ /dev/null
@@ -1 +0,0 @@
-Abandoned by upstream and fails to build from source
diff --git a/div.pvs b/div.pvs
new file mode 100644
index 0000000..4005fe3
--- /dev/null
+++ b/div.pvs
@@ -0,0 +1,35 @@
+% Copyright (c) 2010 Jerry James.
+%
+% Permission is hereby granted, free of charge, to any person obtaining a copy
+% of this software and associated documentation files (the "Software"), to deal
+% in the Software without restriction, including without limitation the rights
+% to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+% copies of the Software, and to permit persons to whom the Software is
+% furnished to do so, subject to the following conditions:
+%
+% The above copyright notice and this permission notice shall be included in
+% all copies or substantial portions of the Software.
+%
+% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+% IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+% FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+% AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+% LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+% OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+% THE SOFTWARE.
+
+div: THEORY
+BEGIN
+
+ x : VAR int
+ nzy : VAR nzint
+
+ div(x, nzy): int =
+ IF (x >= 0 AND nzy > 0) THEN ndiv(x, nzy)
+ ELSIF (x >= 0 AND nzy < 0) THEN -ndiv(x, -nzy)
+ ELSIF (x < 0 AND nzy > 0) THEN -ndiv(-x, nzy)
+ ELSE ndiv(-x, -nzy)
+ ENDIF
+
+END div
+
diff --git a/jessie.appdata.xml b/jessie.appdata.xml
new file mode 100644
index 0000000..3cbd299
--- /dev/null
+++ b/jessie.appdata.xml
@@ -0,0 +1,43 @@
+
+
+ jessie.desktop
+ CC0-1.0
+ LGPL-2.1
+ jessie
+ Interface between why and Frama-C
+
+
+ Jessie is an interface between why and Frama-C.
+
+
+ Why is a software verification platform that applies formal proving tools to
+ annotated programs. The Jessie plugin provide the ability to analyze C
+ programs by invoking Frama-C.
+
+
+
+ loganjerry@gmail.com
+ http://krakatoa.lri.fr/
+ https://gforge.inria.fr/tracker/?atid=4012&group_id=999&func=browse
+
diff --git a/jessie.desktop b/jessie.desktop
new file mode 100644
index 0000000..099b3ad
--- /dev/null
+++ b/jessie.desktop
@@ -0,0 +1,7 @@
+[Desktop Entry]
+Name=jessie
+Comment=Verify C program using Jessie plug-in
+Exec=frama-c -jessie %F
+Icon=why
+Type=Application
+Categories=Development;
diff --git a/patch_jessie_pvs b/patch_jessie_pvs
new file mode 100755
index 0000000..3e4abca
--- /dev/null
+++ b/patch_jessie_pvs
@@ -0,0 +1,59 @@
+#!/bin/sh
+
+# To use PVS with frama-c without the NASA Langley PVS library:
+# frama-c -jessie -jessie-atp pvs FILE.c # Generates PVS files
+# cd FILE.jessie/pvs
+# patch_jessie_pvs # Patch jessie_why.pvs to not need NASA Langley library.
+# You can then run PVS to prove the generated theorems with:
+# pvs-sbcl FILE_why.pvs
+#
+# Copyright (c) 2010 David A. Wheeler
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in
+# all copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+# THE SOFTWARE.
+
+
+if [ ! -f jessie_why.pvs ] ; then
+ echo "Did not find file jessie_why.pvs in current directory"
+ exit 1
+fi
+
+patch -p0 -N << END_OF_PATCH
+--- jessie_why.pvs.ORIGINAL 2010-10-05 14:41:58.965970651 -0400
++++ jessie_why.pvs 2010-10-06 14:28:39.250971269 -0400
+@@ -169,14 +169,14 @@
+ (FORALL (x: real): (FORALL (y: real): min(x, y) = x OR min(x, y) = y))
+
+ %% Why axiom sqrt_pos
+- sqrt_pos: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES sqrt(x) >= 0.0))
++ % sqrt_pos: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES sqrt(x) >= 0.0))
+
+ %% Why axiom sqrt_sqr
+- sqrt_sqr: AXIOM
+- (FORALL (x: real): (x >= 0.0 IMPLIES sqr_real(sqrt(x)) = x))
++ % sqrt_sqr: AXIOM
++ % (FORALL (x: real): (x >= 0.0 IMPLIES sqr_real(sqrt(x)) = x))
+
+ %% Why axiom sqr_sqrt
+- sqr_sqrt: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES sqrt(x * x) = x))
++ % sqr_sqrt: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES sqrt(x * x) = x))
+
+ %% Why axiom abs_real_pos
+ abs_real_pos: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES abs(x) = x))
+END_OF_PATCH
+
diff --git a/rem.pvs b/rem.pvs
new file mode 100644
index 0000000..4f126a6
--- /dev/null
+++ b/rem.pvs
@@ -0,0 +1,35 @@
+% Copyright (c) 2010 Jerry James.
+%
+% Permission is hereby granted, free of charge, to any person obtaining a copy
+% of this software and associated documentation files (the "Software"), to deal
+% in the Software without restriction, including without limitation the rights
+% to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+% copies of the Software, and to permit persons to whom the Software is
+% furnished to do so, subject to the following conditions:
+%
+% The above copyright notice and this permission notice shall be included in
+% all copies or substantial portions of the Software.
+%
+% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+% IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+% FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+% AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+% LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+% OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+% THE SOFTWARE.
+
+rem: THEORY
+BEGIN
+
+ x : VAR int
+ nzy : VAR nzint
+
+ rem(x, nzy): int =
+ IF (x >= 0 AND nzy > 0) THEN rem(nzy)(x)
+ ELSIF (x >= 0 AND nzy < 0) THEN rem(-nzy)(x)
+ ELSIF (x < 0 AND nzy > 0) THEN -rem(nzy)(-x)
+ ELSE -rem(-nzy)(-x)
+ ENDIF
+
+END rem
+
diff --git a/sources b/sources
new file mode 100644
index 0000000..d04e7bd
--- /dev/null
+++ b/sources
@@ -0,0 +1,3 @@
+SHA512 (krakatoa.pdf) = 5d0f4e6b938ddc1eafa48264c02cf99e68f776a7e190b997e35fb2cd154627b5d27369886f570cbcfdfe5f3a1929a97a1fec9457a6f6662f83cbb2e51f65ca04
+SHA512 (why-2.38.tar.gz) = 304cda3aa2f0ca2e114cf3bc6f2bb89327ec97b0f2217d605dbcda3b7601550992bb757724af43ba4ee7ca8eb7ca8bcacb218265acbe7b7b275de9cca86f88a9
+SHA512 (why-icons.tar.xz) = d6ca78cf09540f5742564912470fb8c49f7d11ca16cd8bb60c8790af10c1591198f6020bd792cff8e3464f762b7ef0a690d3e4ba1a2cf670c286c8056d266bc3
diff --git a/why.spec b/why.spec
new file mode 100644
index 0000000..a180553
--- /dev/null
+++ b/why.spec
@@ -0,0 +1,567 @@
+# Whether PVS is available
+%ifarch %{ix86} x86_64 ppc sparcv9
+%global has_pvs 1
+%else
+%global has_pvs 0
+%endif
+
+# What kind of ocaml build to do
+%global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
+
+Name: why
+Version: 2.38
+Release: 1%{?dist}
+Summary: Software verification platform
+
+License: LGPLv2 with exceptions
+URL: http://why.lri.fr/
+Source0: http://why.lri.fr/download/%{name}-%{version}.tar.gz
+Source1: http://krakatoa.lri.fr/manual/krakatoa.pdf
+Source2: README.why-coq.Fedora
+Source3: README.why
+Source4: jessie.desktop
+Source5: jessie.appdata.xml
+Source6: div.pvs
+Source7: rem.pvs
+Source8: patch_jessie_pvs
+# Created with gimp from official upstream icon
+Source9: %{name}-icons.tar.xz
+
+BuildRequires: auto-destdir
+BuildRequires: desktop-file-utils
+BuildRequires: xemacs xemacs-packages-extra
+BuildRequires: frama-c
+BuildRequires: gappalib-coq
+BuildRequires: ocaml
+BuildRequires: ocaml-apron-devel
+BuildRequires: ocaml-camlp4-devel
+BuildRequires: ocaml-findlib
+BuildRequires: ocaml-mlgmpidl-devel
+BuildRequires: ocaml-ocamldoc
+BuildRequires: ocaml-ocamlgraph-devel
+BuildRequires: ocaml-zarith-devel
+BuildRequires: why3
+BuildRequires: coq
+%if %{has_pvs}
+BuildRequires: pvs
+%endif
+
+Requires: gappalib-coq
+Requires: hicolor-icon-theme
+Requires: emacs-filesystem
+
+# This can be removed once Fedora 25 reaches EOL
+Obsoletes: %{name}-coq < 2.36-1
+Provides: %{name}-coq = %{version}-%{release}
+
+# Filter out bogus requires
+%global __requires_exclude ocaml\\\((Ast|Cc|Env|Error|Jc_ast|Jc_env|Loc|Logic|Logic_decl|Misc|Ptree|Types)\\\)
+
+%description
+Why is a software verification platform that applies formal proving
+tools to annotated programs. It is currently capable of analysis of C
+(through "Frama-C"), Java (through the included tool "Krakatoa"), and
+potentially ML programs with some modification into Why's own ML-like
+language. Furthermore, Why is capable of analysis of any program that
+is mapped onto its own internal language. It uses a weakest
+precondition involving calculus to generate potential theorems necessary
+for the proof of a program's correctness. It translates these theorems
+into formats that can be used by external proof assistants (without any
+extra work Coq, PVS, HOL Light, and Mizar are supported - having one is
+recommended and both Coq and PVS are packaged for Fedora) and automated
+theorem provers (without any extra work Simplify, Alt-Ergo, Yices, Z3,
+CVC3, and Zenon are supported and Alt-Ergo, Z3, and Zenon are packaged
+for Fedora) so that these results can be externally proven, resulting in
+a proof of program correctness.
+
+Note: Each user account must be set up by running "why-config" at the
+command line (to set up a configuration file).
+
+%package jessie
+Summary: Interface between why and frama-c
+Requires: %{name}%{?_isa} = %{version}-%{release}
+Requires: frama-c
+
+%description jessie
+The Jessie plugin, an interface between why and frama-c. Invoke it with:
+ frama-c -jessie FILE.c
+
+%if %{has_pvs}
+# Why's integration with PVS depends on the NASA Langley PVS Libraries,
+# which have no license information. This provides an alternative:
+%package pvs-support
+Summary: Complete Why software verification platform suite
+Requires: %{name}%{?_isa} = %{version}-%{release}
+Requires: pvs
+
+%description pvs-support
+This package provides support definitions so that the Why software
+verification platform suite can invoke PVS without licensing issues.
+%endif
+
+%package all
+Summary: Complete Why software verification platform suite
+Requires: why%{?_isa} = %{version}-%{release}
+Requires: why-jessie%{?_isa} = %{version}-%{release}
+%if %{has_pvs}
+Requires: why-pvs-support%{?_isa} = %{version}-%{release}
+%endif
+Requires: alt-ergo z3 zenon
+
+%description all
+This package provides a complete software verification platform suite
+based on Why, including various automated and interactive provers.
+
+%prep
+%setup -q
+%setup -q -T -D -a 9
+
+cp -p %SOURCE2 ./
+
+# Link with Fedora LDFLAGS
+for flag in $RPM_LD_FLAGS; do
+ sed -e "\%^bin/jessie\.opt%,\%^bin/jessie\.byte%s|-o|-ccopt $flag &|" \
+ -e "/gtkThread\.cmx/s|-o|-ccopt $flag &|" \
+ -i Makefile.in
+done
+
+%define fix_encoding() \
+ iconv -f %2 -t %3 %1 > %1.utf8; \
+ touch -r %1 %1.utf8; \
+ mv -f %1.utf8 %1;
+
+# Fix encodings
+for f in CHANGES COPYING; do
+ %fix_encoding $f ISO-8859-1 UTF-8
+done
+
+# APRON support: add a missing rpath and adapt to newer versions of apron
+sed -e "s|-lpolkaMPQ_caml|-Wl,-rpath,%{_libdir}/ocaml/apron|" \
+ -e "s|box\.cmxa polka.cmxa|boxMPQ.cmxa polkaMPQ.cmxa octMPQ.cmxa|" \
+ -i configure
+
+# Enable debuginfo
+sed -i 's,@STRIP@,/usr/bin/true,;s,-dtypes [^-],-g &,' Makefile.in
+sed -ri 's,ocaml(c|opt),& -g,' atp/Makefile
+
+# Command "pvs" is LVM2's /sbin/pvs, so rename "pvs" to pvs-sbcl:
+sed -i 's/pvs/pvs-sbcl/' configure
+
+# Allow building with OCaml 4.04
+sed -i 's/4\.03\.\*/4.03.*|4.04.*/' configure
+
+# Fix detection of why3
+sed -i '/WHY3/s/\\+\\) \.\*/*\\).*/' configure
+
+%build
+%if ! %{opt}
+%global opt_option OCAMLBEST=byte OCAMLDEP=ocamldep OCAMLYACC=ocamlyacc OCAMLLEX=ocamllex
+%else
+%global opt_option OCAMLBEST=opt
+%endif
+
+%configure --enable-apron --enable-verbosemake
+make %{opt_option}
+
+%install
+# Avoid a bug in PVS batch mode when using emacs
+make install DESTDIR=%{buildroot} %{opt_option} \
+ PVSLIB=%{buildroot}%{_libdir}/pvs/lib PVSEMACS=xemacs
+
+# Fix permissions
+chmod a-x %{buildroot}%{_libdir}/frama-c/plugins/META.frama-c-jessie
+chmod a-x %{buildroot}%{_libdir}/frama-c/plugins/Jessie.cmi
+chmod a-x %{buildroot}%{_libdir}/frama-c/plugins/top/Jessie.cm{a,o,x}
+
+# If no PVS, no .pvs files should be installed
+%if ! %{has_pvs}
+rm -fr %{buildroot}%{_libdir}/pvs
+%endif
+
+# Install desktop file
+desktop-file-install --dir=%{buildroot}%{_datadir}/applications %{SOURCE4}
+
+# Install AppData files
+mkdir -p %{buildroot}%{_datadir}/appdata
+install -pm 644 %{SOURCE5} %{buildroot}%{_datadir}/appdata
+
+# Install the icons
+mkdir -p %{buildroot}%{_datadir}/icons
+cp -a icons %{buildroot}%{_datadir}/icons/hicolor
+
+%if %{has_pvs}
+# Get rid of a BUILDROOT reference in a log file (fails QA_CHECK_RPATHS)
+sed -i "s|%{buildroot}||" %{buildroot}%{_libdir}/pvs/lib/why/top.out
+
+mkdir -p %{buildroot}%{_libdir}/pvs/lib/ints/
+cp -p %{SOURCE6} %{SOURCE7} %{buildroot}%{_libdir}/pvs/lib/ints/
+cp -p %{SOURCE8} %{buildroot}%{_bindir}/
+%endif
+
+%global why_doc_dir %{?_pkgdocdir}%{!?_pkgdocdir:%{_docdir}/%{name}-%{version}}
+
+# Fix up documentation and examples
+mkdir -p %{buildroot}%{why_doc_dir}
+cp -p %{SOURCE1} %{SOURCE3} CHANGES README Version %{buildroot}%{why_doc_dir}
+
+%check
+make check
+
+%post jessie
+touch --no-create %{_datadir}/icons/hicolor &>/dev/null
+gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || :
+
+%postun jessie
+touch --no-create %{_datadir}/icons/hicolor &>/dev/null
+gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || :
+
+%files
+%doc README.why-coq.Fedora
+%license COPYING LICENSE
+%{_bindir}/*
+%{_libdir}/why/
+%{_datadir}/icons/hicolor/*/apps/%{name}.png
+%{why_doc_dir}/
+# why-jessie
+%exclude %{_bindir}/jessie
+# why-pvs-support:
+%exclude %{_bindir}/patch_jessie_pvs
+
+%files jessie
+%{_bindir}/jessie
+%{_libdir}/frama-c/plugins/Jessie.cmi
+%{_libdir}/frama-c/plugins/META.frama-c-jessie
+%{_libdir}/frama-c/plugins/top/Jessie.*
+%{_datadir}/appdata/jessie.appdata.xml
+%{_datadir}/applications/jessie.desktop
+
+%if %{has_pvs}
+%files pvs-support
+%{_libdir}/pvs/lib/*
+%{_bindir}/patch_jessie_pvs
+%endif
+
+# "why-all" is a meta-package; it just depends on other packages, so that
+# it's easier to install a useful suite of tools. Thus, it has no files:
+%files all
+
+
+%changelog
+* Fri Mar 24 2017 Jerry James - 2.38-1
+- New upstream release
+
+* Sat Feb 11 2017 Fedora Release Engineering - 2.36-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild
+
+* Thu Jan 12 2017 Jerry James - 2.36-1
+- New upstream release
+
+* Wed Nov 30 2016 Jerry James - 2.35-23
+- Rebuild for gappalib-coq 1.3.2
+
+* Sun Nov 06 2016 Richard W.M. Jones - 2.35-21
+- Rebuild for OCaml 4.04.0.
+- Modify configure script to allow building with OCaml 4.04.
+- Modify configure script to use octMPQ library (part of Apron).
+
+* Fri Oct 28 2016 Jerry James - 2.35-20
+- Rebuild for coq 8.5pl3
+- Remove obsolete scriptlets
+
+* Thu Sep 29 2016 Jerry James - 2.35-19
+- Rebuild for flocq 2.5.2 and gappalib-coq 1.3.1
+
+* Fri Sep 2 2016 Jerry James - 2.35-18
+- Rebuild for why3 0.87.2
+
+* Fri Jul 22 2016 Jerry James - 2.35-17
+- Rebuild for apron 0.9.11 and gappalib-coq 1.3.0
+
+* Wed Jul 13 2016 Jerry James - 2.35-16
+- Rebuild for coq 8.5pl2
+
+* Wed Jun 1 2016 Jerry James - 2.35-15
+- Rebuild for why3 0.87.1 and Frama-C Aluminium
+
+* Fri Apr 22 2016 Jerry James - 2.35-14
+- Rebuild for coq 8.5pl1
+
+* Sat Apr 16 2016 Jerry James - 2.35-13
+- Rebuild for ocaml-ocamlgraph 1.8.7
+
+* Fri Mar 18 2016 Jerry James - 2.35-12
+- Rebuild for why3 0.87.0
+
+* Fri Feb 12 2016 Jerry James - 2.35-11
+- Rebuild for coq 8.5, flocq 2.5.1, gappalib-coq 1.2.1, why3 0.86.3, and
+ Frama-C Magnesium
+- Use camlp4 in preference to camlp5
+- Drop cvc3 support
+- Update appdata for latest specification
+
+* Fri Feb 05 2016 Fedora Release Engineering - 2.35-10
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild
+
+* Wed Oct 14 2015 Jerry James - 2.35-9
+- Rebuild for flocq 2.5.0, gappalib-coq 1.2.0, and why3 0.86.2
+
+* Thu Jul 30 2015 Richard W.M. Jones - 2.35-8
+- OCaml 4.02.3 rebuild.
+
+* Mon Jun 22 2015 Jerry James - 2.35-7
+- Rebuild for why3 0.86.1
+
+* Fri Jun 19 2015 Richard W.M. Jones - 2.35-6
+- Rebuild for ocaml-4.02.2.
+
+* Fri Jun 19 2015 Fedora Release Engineering - 2.35-5
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_23_Mass_Rebuild
+
+* Sat May 16 2015 Jerry James - 2.35-4
+- Rebuild for why3 0.86
+
+* Mon Apr 13 2015 Jerry James - 2.35-3
+- Rebuild for coq 8.4pl6
+
+* Wed Apr 1 2015 Jerry James - 2.35-2
+- Adjust requires filter
+
+* Tue Mar 31 2015 Jerry James - 2.35-1
+- New upstream release
+- Drop upstreamed -flocq24 and -frama-c-sodium patches
+- Drop all gwhy-related sources, as gwhy has been retired
+- Merge (X)Emacs files into the main package due to change in policy
+
+* Thu Mar 19 2015 Jerry James - 2.34-18
+- Rebuild for Frama-C Sodium
+- Add -ocamlgraph186 patch to adapt to ocamlgraph 1.8.6
+- Add -frama-c-sodium patch to adapt to Frama-C Sodium
+
+* Thu Feb 19 2015 Richard W.M. Jones - 2.34-17
+- ocaml-4.02.1 rebuild.
+
+* Sat Nov 15 2014 Jerry James - 2.34-16
+- Fix gwhy-2.33.patch (bz 1164470)
+
+* Thu Nov 13 2014 Richard W.M. Jones - 2.34-15
+- Bump and rebuild for broken dependencies.
+
+* Thu Oct 30 2014 Jerry James - 2.34-14
+- Rebuild for coq 8.4pl5
+
+* Thu Sep 18 2014 Jerry James - 2.34-13
+- Rebuild for why3 0.85
+
+* Mon Sep 8 2014 Jerry James - 2.34-12
+- Rebuild for fixed frama-c
+- Fix license handling
+
+* Tue Sep 2 2014 Jerry James - 2.34-11
+- Rebuild for the final ocaml 4.02.0 release
+
+* Mon Aug 25 2014 Jerry James - 2.34-10
+- ocaml-4.02.0+rc1 rebuild.
+
+* Mon Aug 18 2014 Fedora Release Engineering - 2.34-9
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild
+
+* Mon Aug 4 2014 Jerry James - 2.34-8
+- OCaml 4.02.0 beta rebuild
+- BR emacs instead of emacs-nox, which no longer exists
+
+* 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"
+
+* Sun Jun 08 2014 Fedora Release Engineering - 2.34-6
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild
+
+* Tue May 13 2014 Jerry James - 2.34-5
+- Rebuild for coq 8.4pl4
+
+* Mon Apr 21 2014 Jerry James - 2.34-4
+- Rebuild for ocamlgraph 1.8.5 and flocq 2.3.0
+- Drop has_coq macro, since coq is now universally available
+- Add -flocq23 patch to adapt to flocq 2.3.0
+
+* Tue Apr 15 2014 Richard W.M. Jones - 2.34-3
+- Remove ocaml_arches macro (RHBZ#1087794).
+
+* Mon Mar 24 2014 Jerry James - 2.34-2
+- Remove dropped patches
+- Add icons
+- Fix the desktop icon entries
+
+* Tue Mar 18 2014 Jerry James - 2.34-1
+- New upstream release
+- Drop upstreamed -hashtbl, -flocq, and -or patches
+- Add ocaml-findlib BR
+
+* Wed Feb 26 2014 Jerry James - 2.33-6
+- Rebuild for ocamlgraph 1.8.4
+- Update desktop files
+- Add AppData files for gwhy and jessie
+
+* Tue Sep 17 2013 Jerry James - 2.33-5
+- Rebuild for OCaml 4.01.0
+- Enable debuginfo
+- Add -or patch to fix warnings, since warnings are errors
+
+* Sat Jul 27 2013 Ville Skyttä - 2.33-4
+- Install docs to %%{_pkgdocdir} where available.
+
+* Fri Jun 21 2013 Jerry James - 2.33-3
+- Rebuild for frama-c Fluorine 20130601
+
+* Thu May 23 2013 Jerry James - 2.33-2
+- Rebuild for new frama-c and why3 builds
+
+* Tue May 14 2013 Jerry James - 2.33-1
+- New upstream release
+- Drop upstreamed -warning, -coq84, and -ocaml4 patches
+- Add -hashtbl patch
+- Enable Jessie plugin again
+
+* Sat Feb 09 2013 Parag Nemade - 2.31-7
+- Remove vendor tag from desktop file as per https://fedorahosted.org/fesco/ticket/1077
+
+* Mon Jan 14 2013 Jerry James - 2.31-6
+- Rebuild for alt-ergo 0.95
+
+* Mon Jan 7 2013 Jerry James - 2.31-5
+- Rebuild for coq 8.4pl1
+
+* Fri Oct 19 2012 Jerry James - 2.31-4
+- Rebuild for OCaml 4.00.1 and frama-c Oxygen
+- Recripple the Jessie plugin until it works with frama-c Oxygen
+
+* Tue Sep 11 2012 Jerry James - 2.31-3
+- Rebuild for new frama-c build with altered API.
+
+* Mon Aug 27 2012 Jerry James - 2.31-2
+- Frama-c is fixed; rebuild with the Jessie plugin enabled and functioning
+
+* Thu Aug 23 2012 Jerry James - 2.31-1
+- New upstream version
+- Drop upstreamed patches
+- Add ocaml-mlgmpidl-devel and why3 BRs
+- Add -warning, -ocaml4, and -coq84 patches to fix the build
+- Cripple the Jessie plugin until problems with frama-c and hashtables are fixed
+
+* Mon Jul 30 2012 Richard W.M. Jones - 2.30-7
+- Rebuild for OCaml 4.00.0 official.
+
+* Sun Jul 22 2012 Fedora Release Engineering - 2.30-6
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild
+
+* Wed Jan 11 2012 Jerry James - 2.30-5
+- Patch to work with flocq 2.0.0
+
+* Tue Dec 27 2011 Jerry James - 2.30-4
+- Rebuild for coq 8.3pl3
+
+* Tue Dec 6 2011 Jerry James - 2.30-3
+- Update alt_ergo and yices "okay" version numbers
+
+* Wed Nov 23 2011 Jerry James - 2.30-2
+- Rebuild with APRON and gappalib-coq support
+
+* Fri Oct 28 2011 Jerry James - 2.30-1
+- New upstream release
+
+* Thu Jul 14 2011 Jerry James - 2.29-2
+- Fix broken conditionals
+
+* Mon Jul 11 2011 Jerry James - 2.29-1
+- New upstream release (fixes FTBFS: bz 715902)
+- Remove unnecessary spec file elements (BuildRoot, etc.)
+- Update approach to filtering provides and requires
+- Add has_pvs analogously to has_coq, and simplify macro usage
+- Add (X)Emacs support packages
+- New subpackage for the jessie plugin to avoid unowned directories and
+ permit a direct dependency on frama-c
+- Prepare for the eventual availability of APRON
+
+* Thu Apr 14 2011 Karsten Hopp 2.28-2.2
+- add ppc to excludearch, too. No pvs-sbcl available there
+
+* Wed Apr 13 2011 Karsten Hopp 2.28-2.1
+- add ppc64 to excludearch, no sbcl available there
+
+* Mon Feb 07 2011 Fedora Release Engineering - 2.28-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild
+
+* Fri Jan 21 2011 Richard W.M. Jones - 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 - 2.26-2
+- Bump and rebuild for OCaml 3.12.
+
+* Sat Oct 09 2010 David A. Wheeler + Mark Rader - 2.26-1
+- Upgrade to upstream version 2.26 (inc. update of krakatoa.pdf)
+- Integrated with Frama-C and PVS (as pvs-sbcl)
+
+* Mon Jan 11 2010 Richard W.M. Jones - 2.23-2
+- Rebuild to fix dependencies.
+
+* Fri Jan 08 2010 Alan Dunn - 2.23-1
+- Upgrade to upstream version 2.23
+- Move execstack fixing to spec file from patch
+- Moved patch descriptions to initial patch declaration as in examples
+ in Fedora documentation
+- New Caduceus, Krakatoa documentation
+- Update test result from small test min.mlw
+- Added CVC3 interfacing capabilities
+- Removed patch for gwhy configuration, as there is a new mechanism for this
+
+* Tue Sep 22 2009 Dennis Gilmore - 2.17-5
+- Exclude sparc64 s390 s390x there is no ocaml there
+
+* Fri Aug 07 2009 Alan Dunn - 2.17-4
+- Removed now irrelevant check for no OCaml in Fedora < 9 (those
+ distributions are EOL)
+- Changed ExcludeArch to proper Fedora versions
+- Builds coq subpackage exactly when Coq can be built, thus making
+ build independent of whether Coq can be built
+- define -> global
+- Fixed accidental use of in tar ocamlgraph instead of one that is
+ separately packaged
+
+* Mon Jul 27 2009 Fedora Release Engineering - 2.17-3
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_12_Mass_Rebuild
+
+* Wed Feb 25 2009 Fedora Release Engineering - 2.17-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_11_Mass_Rebuild
+
+* Wed Dec 24 2008 Alan Dunn 2.17-1
+- Upgrade to version 2.17 (bz: 477790)
+- Add ownership of two directories common with Coq, but neither program requires the other (bz: 474016)
+- Minor filename change in 2.17 (GPL -> LICENSE)
+- Added back Coq .v files to match policy for Coq
+- Changed directory structure re: jessie and krakatoa to match new structure in 2.17
+- Minor changes to patches to ensure they still work in 2.17
+- Corrected package location gwhy-icon.png (should only be in gwhy)
+* Tue Aug 5 2008 Alan Dunn 2.14-2.1
+- ExcludeArch ppc64 on Fedora 8 due to no ocaml.
+* Fri Aug 1 2008 Alan Dunn 2.14-2
+- Fixed minor issues in response to package review:
+- Inclusion of COPYING, GPL license-related files
+- Added config.mll patch to make default config file created nicer
+- Changes subpackage dependencies to be fully versioned.
+- Makes during build allowed to be noisy (allowed to print).
+* Wed Jul 30 2008 Alan Dunn 2.14-1
+- Changed to new version of why, removed previous why-cpulimit name
+ change, zenon output format patches as the issues were fixed in
+ why 2.14.
+- Moved doc subpackage back into main package.
+- Added example files to documentation subpackage.
+- Added check section with test on small why file.
+- Reformatted some macro names for greater readability.
+* Thu Jul 24 2008 Alan Dunn 2.13-2
+- Added several patches: fixed Zenon output, completed fix of rename
+ of cpulimit -> why-cpulimit.
+* Wed Jul 23 2008 Alan Dunn 2.13-1
+- Initial Fedora RPM version.