diff --git a/.gitignore b/.gitignore
deleted file mode 100644
index ed00d3a..0000000
--- a/.gitignore
+++ /dev/null
@@ -1,3 +0,0 @@
-/krakatoa.pdf
-/why-2.35.tar.gz
-/why-icons.tar.xz
diff --git a/README.why b/README.why
deleted file mode 100644
index ba95dfa..0000000
--- a/README.why
+++ /dev/null
@@ -1,8 +0,0 @@
-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
deleted file mode 100644
index 406a7a9..0000000
--- a/README.why-coq.Fedora
+++ /dev/null
@@ -1,6 +0,0 @@
-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
new file mode 100644
index 0000000..497866a
--- /dev/null
+++ b/dead.package
@@ -0,0 +1 @@
+Abandoned by upstream and fails to build from source
diff --git a/div.pvs b/div.pvs
deleted file mode 100644
index 4005fe3..0000000
--- a/div.pvs
+++ /dev/null
@@ -1,35 +0,0 @@
-% 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
deleted file mode 100644
index fc64aad..0000000
--- a/jessie.appdata.xml
+++ /dev/null
@@ -1,26 +0,0 @@
-
-
- jessie.desktop
- CC0
-
-
- 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.
-
-
-
- http://krakatoa.lri.fr/jessie/max_why3ide.png
- http://krakatoa.lri.fr/jessie/max_ptr_why3ide.png
- http://krakatoa.lri.fr/jessie/binary_search_raw.png
- http://krakatoa.lri.fr/jessie/binary_search_ovfl.png
- http://krakatoa.lri.fr/jessie/binary_search_behav.png
-
- http://krakatoa.lri.fr/
-
-
diff --git a/jessie.desktop b/jessie.desktop
deleted file mode 100644
index 099b3ad..0000000
--- a/jessie.desktop
+++ /dev/null
@@ -1,7 +0,0 @@
-[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
deleted file mode 100755
index 3e4abca..0000000
--- a/patch_jessie_pvs
+++ /dev/null
@@ -1,59 +0,0 @@
-#!/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
deleted file mode 100644
index 4f126a6..0000000
--- a/rem.pvs
+++ /dev/null
@@ -1,35 +0,0 @@
-% 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
deleted file mode 100644
index e3fda8e..0000000
--- a/sources
+++ /dev/null
@@ -1,3 +0,0 @@
-cc7a2e360acf8569a2eb878f51bfc8ff krakatoa.pdf
-10bde72f95de8bc34135a8207cfcc9ec why-2.35.tar.gz
-ed5648bbfb5e74fdfb814cdd725b191e why-icons.tar.xz
diff --git a/why-2.35-Makefile.in.patch b/why-2.35-Makefile.in.patch
deleted file mode 100644
index 5b490d5..0000000
--- a/why-2.35-Makefile.in.patch
+++ /dev/null
@@ -1,23 +0,0 @@
---- Makefile.in.orig 2015-03-25 08:32:17.000000000 -0600
-+++ Makefile.in 2015-03-30 20:00:00.000000000 -0600
-@@ -815,17 +815,9 @@
- mkdir -p $(LIBDIR)/why/coq7
- cp -f $(VO7) $(LIBDIR)/why/coq7
- install-coq-v8 install-coq-v8.1:
-- if test -w $(COQLIB) ; then \
-- rm -f $(COQLIB)/user-contrib/Why*.v* ; \
-- rm -f $(COQLIB)/user-contrib/caduceus*.v* $(COQLIB)/user-contrib/Caduceus*.v* ; \
-- rm -f $(COQLIB)/user-contrib/jessie*.v* $(COQLIB)/user-contrib/Jessie*.v* ; \
-- 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." ;\
-- fi
-- mkdir -p $(LIBDIR)/why/coq
-- cp -f $(VO8) $(LIBDIR)/why/coq
-+ mkdir -p $(COQLIB)/user-contrib/Why
-+ cp -pf $(V8FILES) $(COQLIB)/user-contrib/Why
-+ cp -pf $(VO8) $(COQLIB)/user-contrib/Why
-
- install-pvs-no:
- install-pvs-yes: $(PVSFILES)
diff --git a/why-ocamlgraph186.patch b/why-ocamlgraph186.patch
deleted file mode 100644
index fd15ef4..0000000
--- a/why-ocamlgraph186.patch
+++ /dev/null
@@ -1,14 +0,0 @@
---- src/hypotheses_filtering.ml.orig 2015-03-25 08:32:17.000000000 -0600
-+++ src/hypotheses_filtering.ml 2015-03-30 20:00:00.000000000 -0600
-@@ -1680,9 +1680,9 @@
- *******************)
-
- module W = struct
-- type label = PdlGraph.E.label
-+ type edge = PdlGraph.E.t
- type t = int
-- let weight x = x
-+ let weight e = PdlGraph.E.label e
- let zero = 0
- let add = (+)
- let compare = compare
diff --git a/why.spec b/why.spec
deleted file mode 100644
index bec3df1..0000000
--- a/why.spec
+++ /dev/null
@@ -1,598 +0,0 @@
-# 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.35
-Release: 9%{?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
-
-# 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
-# it is and their checking causes the rpm building to fail.
-# 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.
-Patch0: %{name}-2.35-Makefile.in.patch
-
-# Adapt to ocamlgraph 1.8.6
-Patch1: %{name}-ocamlgraph186.patch
-
-BuildRequires: auto-destdir
-BuildRequires: cvc3
-BuildRequires: desktop-file-utils
-BuildRequires: emacs 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: why3
-BuildRequires: coq
-%if %{has_pvs}
-BuildRequires: pvs
-%endif
-
-Requires: hicolor-icon-theme
-Requires: emacs-filesystem
-Requires: xemacs-filesystem
-
-# This can be removed once Fedora 22 reaches EOL
-Obsoletes: %{name}-gwhy < 2.35-1%{?dist}
-Provides: %{name}-gwhy = %{version}-%{release}
-Obsoletes: %{name}-emacs < 2.35-1%{?dist}
-Provides: %{name}-emacs = %{version}-%{release}
-Obsoletes: %{name}-emacs-el < 2.35-1%{?dist}
-Provides: %{name}-emacs-el = %{version}-%{release}
-Obsoletes: %{name}-xemacs < 2.35-1%{?dist}
-Provides: %{name}-xemacs = %{version}-%{release}
-Obsoletes: %{name}-xemacs-el < 2.35-1%{?dist}
-Provides: %{name}-xemacs-el = %{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, CVC3, 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
-Group: Applications/Engineering
-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
-
-%package coq
-Group: Applications/Engineering
-Summary: Libraries for interfacing Coq with Why
-Requires: %{name}%{?_isa} = %{version}-%{release}
-Requires: gappalib-coq
-
-%description coq
-This package contains a set of routines that assist in the manipulation
-of why Coq-formatted output within Coq.
-
-%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
-Group: Applications/Engineering
-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
-Group: Applications/Engineering
-Summary: Complete Why software verification platform suite
-Requires: why%{?_isa} = %{version}-%{release}
-Requires: why-jessie%{?_isa} = %{version}-%{release}
-Requires: why-coq%{?_isa} = %{version}-%{release}
-%if %{has_pvs}
-Requires: why-pvs-support%{?_isa} = %{version}-%{release}
-%endif
-Requires: alt-ergo cvc3 gappalib-coq 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
-%patch0
-%patch1
-
-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 examples/bresenham/bresenham.mlw \
- examples/bresenham/bresenham_coq.mlw examples/bresenham/bresenham_inv.mlw \
- examples/edit-distance/distance.mlw examples/heapsort/downheap.mlw \
- examples/heapsort/heapsort.mlw examples/heapsort/Inftree.v \
- examples/kmp/kmp.mlw examples/kmp/Lex.v examples/kmp/Match.v \
- examples/kmp/Next.v examples/misc/matrix.why examples/misc/matrix_why.v \
- examples/quicksort/partition.mlw examples/quicksort/Partition.v \
- examples/quicksort/quicksort.mlw examples/quicksort/Quicksort.v \
- examples/sqrt/sqrt.mlw examples/string-matching/Match.v; do
- %fix_encoding $f ISO-8859-1 UTF-8
-done
-
-# Fix line endings
-for f in examples-c/tutorial/average.c examples-c/tutorial/purse.c \
- examples-c/ukkonen/main.c examples-c/ukkonen/ukkonen.c; do
- sed "s/\r//" $f > $f.new
- touch -r $f $f.new
- mv -f $f.new $f
-done
-
-# APRON support: add a missing rpath
-sed -i "s|-lpolkaMPQ_caml|-Wl,-rpath,%{_libdir}/ocaml/apron|" 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 -e 's/command = "pvs"/command = "pvs-sbcl"/' \
- -e 's/PVS, (pvs, \["pvs"\]);/PVS, (pvs, ["pvs-sbcl" ; "pvs"]);/' \
- -i tools/dpConfig.ml
-sed -i 's/pvs/pvs-sbcl/' configure
-
-# Allow building with why3 0.86.2
-sed -i 's/0\.85|0\.86/&|0.86.2/' configure
-
-%build
-%if ! %{opt}
-%global opt_option OCAMLBEST=byte OCAMLC=ocamlc OCAMLDEP=ocamldep OCAMLYACC=ocamlyacc OCAMLLEX=ocamllex
-%else
-%global opt_option OCAMLBEST=opt OCAMLOPT=ocamlopt.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
-
-# 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}}
-%global why_examples_dir %{why_doc_dir}/examples/
-
-# Fix up documentation and examples
-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 %{SOURCE1} %{SOURCE3} CHANGES README Version %{buildroot}%{why_doc_dir}
-
-# Copy in the example files, leaving behind all generated files
-cd examples
-for d in `find -mindepth 1 -maxdepth 1 -type d`; do
- mkdir -p %{buildroot}%{why_examples_dir}mlw/$d
-done
-for f in `find -regex '.*\(\.mlw\|\.why\)' | grep -E -v '_inv|_coq|_why'`; do
- cp -p $f %{buildroot}%{why_examples_dir}mlw/$f
-done
-
-cd ../examples-c
-for d in `find -mindepth 1 -maxdepth 1 -type d`; do
- mkdir -p %{buildroot}%{why_examples_dir}c/$d
-done
-for f in `find -regex '.*\.c'`; do
- cp -p $f %{buildroot}%{why_examples_dir}c/$f
-done
-
-# Remove a stray coq file (already installed in the right place)
-rm -f %{buildroot}%{_libdir}/coq/jessie_why.v
-
-# Move the Emacs support file to the right places and byte compile it
-cd ..
-mkdir -p %{buildroot}%{_emacs_sitelispdir}
-cp -p lib/emacs/why.el %{buildroot}%{_emacs_sitelispdir}
-mkdir -p %{buildroot}%{_xemacs_sitelispdir}
-cp -p lib/emacs/why.el %{buildroot}%{_xemacs_sitelispdir}
-cd %{buildroot}%{_emacs_sitelispdir}
-%{_emacs_bytecompile} why.el
-cd %{buildroot}%{_xemacs_sitelispdir}
-%{_xemacs_bytecompile} why.el
-rm -fr %{buildroot}%{_libdir}/why/emacs
-
-%check
-make check
-
-%post jessie
-update-desktop-database &> /dev/null || :
-touch --no-create %{_datadir}/icons/hicolor &>/dev/null
-gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || :
-
-%postun jessie
-update-desktop-database &> /dev/null || :
-touch --no-create %{_datadir}/icons/hicolor &>/dev/null
-gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || :
-
-%files
-%license COPYING LICENSE
-%{_bindir}/*
-%{_libdir}/why/
-%{_datadir}/icons/hicolor/*/apps/%{name}.png
-%{_emacs_sitelispdir}/why.el*
-%{_xemacs_sitelispdir}/why.el*
-%{why_doc_dir}/
-# This last example is really an example only for Coq - only .v files
-%exclude %{why_examples_dir}mlw/string-matching/
-# why-jessie
-%exclude %{_bindir}/jessie
-# why-pvs-support:
-%exclude %{_bindir}/patch_jessie_pvs
-
-%files jessie
-%{_bindir}/jessie
-%{_libdir}/frama-c/plugins/Jessie.*
-%{_datadir}/appdata/jessie.appdata.xml
-%{_datadir}/applications/jessie.desktop
-
-%files coq
-%doc README.why-coq.Fedora
-%{_libdir}/coq/user-contrib/Why/
-
-%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
-* 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.