diff --git a/.gitignore b/.gitignore
deleted file mode 100644
index 3c891f7..0000000
--- a/.gitignore
+++ /dev/null
@@ -1,2 +0,0 @@
-/krakatoa.pdf
-/why-2.30.tar.gz
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/README.why-gwhy.Fedora b/README.why-gwhy.Fedora
deleted file mode 100644
index 3cc41b4..0000000
--- a/README.why-gwhy.Fedora
+++ /dev/null
@@ -1,6 +0,0 @@
-Fedora why-gwhy package:
-
-Contains the gwhy GUI for Why.
-
-Run gwhy with "gwhy <filename>". (If you forget and run without a
-filename you'll be prompted for it.)
\ 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/gwhy-2.26.patch b/gwhy-2.26.patch
deleted file mode 100644
index 15a2576..0000000
--- a/gwhy-2.26.patch
+++ /dev/null
@@ -1,53 +0,0 @@
---- bin/gwhy.sh.orig	2011-03-02 01:27:41.000000000 -0700
-+++ bin/gwhy.sh	2011-07-07 15:41:07.232455718 -0600
-@@ -1,11 +1,17 @@
- #!/bin/sh
- 
--case $1 in
-+if ! test $1; then
-+file=`zenity --file-selection --title="Select the file you want to open with gwhy"`;
-+else
-+file=$1
-+fi
-+
-+case $file in
-   *.java)
--	b=`basename $1 .java`
--	krakatoa $1 || exit 1
-+	b=`basename $file .java`
-+	krakatoa $file || exit 1
- 	echo "krakatoa on $b.java done"
--        d=`dirname $1`
-+        d=`dirname $file`
-         echo "cd $d"
-         cd $d
- 	jessie -locs $b.jloc -why-opt -split-user-conj $b.jc || exit 2
-@@ -13,20 +19,23 @@
- 	make -f $b.makefile gui
- 	;;
-   *.c)
--	b=`basename $1 .c`
--	caduceus -why-opt -split-user-conj $1 || exit 1
-+	b=`basename $file .c`
-+	caduceus -why-opt -split-user-conj $b.c || exit 1
- 	make -f $b.makefile gui
- 	;;
-   *.jc)
--	b=`basename $1 .jc`
-+	b=`basename $file .jc`
- 	jessie -why-opt -split-user-conj $b.jc || exit 1
- 	make -f $b.makefile gui
- 	;;
-   *.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/gwhy-icon.png b/gwhy-icon.png
deleted file mode 100644
index 9a1b76c..0000000
Binary files a/gwhy-icon.png and /dev/null differ
diff --git a/gwhy.desktop b/gwhy.desktop
deleted file mode 100644
index 27f853a..0000000
--- a/gwhy.desktop
+++ /dev/null
@@ -1,8 +0,0 @@
-[Desktop Entry]
-Encoding=UTF-8
-Name=gwhy
-Comment=Examine and develop Why .why files
-Exec=gwhy
-Icon=ICON-LOCATION-BASE/gwhy-icon.png
-Type=Application
-Categories=Development;
\ No newline at end of file
diff --git a/jessie.desktop b/jessie.desktop
deleted file mode 100644
index 239f37a..0000000
--- a/jessie.desktop
+++ /dev/null
@@ -1,8 +0,0 @@
-[Desktop Entry]
-Encoding=UTF-8
-Name=jessie
-Comment=Verify C program using Jessie plug-in
-Exec=frama-c -jessie %f
-Icon=ICON-LOCATION-BASE/gwhy-icon.png
-Type=Application
-Categories=Development;
diff --git a/min.mlw b/min.mlw
deleted file mode 100644
index ae72dea..0000000
--- a/min.mlw
+++ /dev/null
@@ -1,4 +0,0 @@
-logic min: int, int -> int
-axiom min_ax: forall x,y:int. min(x,y) <= x
-parameter r: int ref
-let f (n:int) = {} r := min !r n { r <= r@ }
\ No newline at end of file
diff --git a/min_why.why.result b/min_why.why.result
deleted file mode 100644
index 04848f9..0000000
--- a/min_why.why.result
+++ /dev/null
@@ -1,41 +0,0 @@
-logic eq_unit : unit, unit -> prop
-
-logic neq_unit : unit, unit -> prop
-
-logic eq_bool : bool, bool -> prop
-
-logic neq_bool : bool, bool -> prop
-
-logic lt_int : int, int -> prop
-
-logic le_int : int, int -> prop
-
-logic gt_int : int, int -> prop
-
-logic ge_int : int, int -> prop
-
-logic eq_int : int, int -> prop
-
-logic neq_int : int, int -> prop
-
-logic add_int : int, int -> int
-
-logic sub_int : int, int -> int
-
-logic mul_int : int, int -> int
-
-logic neg_int : int -> int
-
-predicate zwf_zero(a: int, b: int) = ((0 <= b) and (a < b))
-
-logic min : int, int -> int
-
-axiom min_ax: (forall x:int. (forall y:int. (min(x, y) <= x)))
-
-goal f_po_1:
-  forall n:int.
-  forall r0:int.
-  forall r:int.
-  (r = min(r0, n)) ->
-  (r <= r0)
-
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 ae20770..0000000
--- a/sources
+++ /dev/null
@@ -1,2 +0,0 @@
-1e8d6c76e5c3cee018172e981309c68b  krakatoa.pdf
-c3f6c5616e32743e883ffb7609f96336  why-2.30.tar.gz
diff --git a/why-2.30-Makefile.in.patch b/why-2.30-Makefile.in.patch
deleted file mode 100644
index eb43de5..0000000
--- a/why-2.30-Makefile.in.patch
+++ /dev/null
@@ -1,20 +0,0 @@
---- Makefile.in.orig	2011-10-24 09:21:06.000000000 -0600
-+++ Makefile.in	2011-10-25 15:37:54.600278865 -0600
-@@ -782,14 +782,9 @@
- 	cp -f $(V7FILES) $(LIBDIR)/why/coq7
- 	cp -f $(VO7) $(LIBDIR)/why/coq7
- install-coq-v8 install-coq-v8.1:
--	if test -w $(COQLIB) ; then \
--	  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." ;\
--	mkdir -p $(LIBDIR)/why/coq ;\
--	cp -f $(VO8) $(V8FILES) $(LIBDIR)/why/coq ;\
--	fi
-+	mkdir -p $(COQLIB)/user-contrib/Why
-+	cp -f $(V8FILES) $(COQLIB)/user-contrib/Why
-+	cp -f $(VO8) $(COQLIB)/user-contrib/Why
- 
- install-pvs-no:
- install-pvs-yes: $(PVSFILES)
diff --git a/why-apron.patch b/why-apron.patch
deleted file mode 100644
index 4e23767..0000000
--- a/why-apron.patch
+++ /dev/null
@@ -1,40 +0,0 @@
---- jc/jc_annot_inference.ml.orig	2011-10-24 09:21:06.000000000 -0600
-+++ jc/jc_annot_inference.ml	2011-11-23 13:47:40.438177237 -0700
-@@ -148,7 +148,7 @@
- 	      Some(tptr,offt)
- 	end
-     | JCTvar _ | JCTderef _ | JCTapp _ | JCTold _ | JCTat _ | JCTif _ 
--    | JCTrange _ | JCTmatch _ | JCTaddress _ | JCTbase_block _
-+    | JCTlet _ | JCTrange _ | JCTmatch _ | JCTaddress _ | JCTbase_block _
-     | JCTconst _ | JCTbinary _ | JCTunary _ | JCToffset _ | JCTinstanceof _ 
-     | JCTreal_cast _ | JCTrange_cast _ | JCTbitwise_cast _ | JCTcast _ ->
- 	None
-@@ -491,7 +491,7 @@
-   in
-   Format.fprintf Format.str_formatter "%a" Jc_output.assertion a;
-   let formula = Format.flush_str_formatter () in
--  let lab = Output.reg_pos "G" ?id ?kind ?name ~formula loc in
-+  let lab = Output.old_reg_pos "G" ?id ?kind ?name ~formula (Loc.extract loc) in
-   new assertion_with ~mark:lab a
- 
- 
-@@ -608,8 +608,8 @@
- 	Atp.Fn(atp_of_unop uop, [atp_of_term t1])
-     | JCTvar _ | JCTderef _ | JCTapp _ | JCToffset _ ->
- 	Atp.Var (Vwp.variable_for_term t)
--    | JCTshift _ | JCTold _ | JCTat _ | JCTmatch _ | JCTinstanceof _ 
--    | JCTcast _ | JCTrange_cast _ | JCTbitwise_cast _ | JCTreal_cast _ 
-+    | JCTshift _ | JCTold _ | JCTat _ | JCTmatch _ | JCTinstanceof _ | JCTlet _
-+    | JCTcast _ | JCTrange_cast _ | JCTbitwise_cast _ | JCTreal_cast _
-     | JCTaddress _ | JCTif _ | JCTrange _ | JCTunary _ | JCTbase_block _ ->
- 	err ()
- 
-@@ -1198,7 +1198,7 @@
-       | JCTunary _ | JCTshift _ | JCTinstanceof _ | JCTmatch _ 
-       | JCTold _ | JCTat _ | JCTcast _ | JCTbitwise_cast _ 
-       | JCTrange_cast _ | JCTreal_cast _ | JCTaddress _ | JCTbase_block _
--      | JCTrange _ | JCTif _ -> 
-+      | JCTlet _ | JCTrange _ | JCTif _ -> 
- 	  err ()
-     with Failure "linearize" -> 
-       (TermMap.add t (Int 1) TermMap.empty, Int 0)
diff --git a/why-flocq2.patch b/why-flocq2.patch
deleted file mode 100644
index 27dda9f..0000000
--- a/why-flocq2.patch
+++ /dev/null
@@ -1,510 +0,0 @@
---- ./lib/coq/WhyFloats.v.orig	2011-10-24 09:21:06.000000000 -0600
-+++ ./lib/coq/WhyFloats.v	2012-01-11 15:41:08.873131034 -0700
-@@ -19,17 +19,13 @@ Let emin := (3 - emax - prec)%Z.
- Let fexp := FLT_exp emin prec.
- Lemma Hprec': (0 < prec)%Z. revert Hprec. now case Zlt_bool_spec. Qed.
- Lemma Hemax': (prec < emax)%Z. revert Hemax. now case Zlt_bool_spec. Qed.
--Let binary_round_correct := binary_round_sign_shl_correct prec emax Hprec' Hemax'.
-+Lemma fexp': Valid_exp fexp. apply FLT_exp_valid. apply Hprec'. Qed.
- 
- Definition r_to_sd rnd x : binary_float prec emax :=
-   let r := round radix2 fexp (round_mode rnd) x in
-   let m := Ztrunc (scaled_mantissa radix2 fexp r) in
--  let e := canonic_exponent radix2 fexp r in
--  match m with
--  | Z0 => B754_zero prec emax false
--  | Zpos m => FF2B _ _ _ (proj1 (binary_round_correct rnd false m e))
--  | Zneg m => FF2B _ _ _ (proj1 (binary_round_correct rnd true m e))
--  end.
-+  let e := canonic_exp radix2 fexp r in
-+  binary_normalize prec emax Hprec' Hemax' rnd m e false.
- 
- Lemma is_finite_FF2B :
-   forall f H,
-@@ -49,59 +45,19 @@ Theorem r_to_sd_correct :
-   (Rabs r < bpow radix2 emax)%R ->
-   is_finite prec emax (r_to_sd rnd x) = true /\
-   r_to_sd rnd x = r :>R.
--Proof.
-+Proof with auto with typeclass_instances.
- intros rnd x r Bx.
- unfold r_to_sd. fold r.
--assert (Gx: generic_format radix2 fexp r).
--apply generic_format_round.
--apply FLT_exp_correct.
--exact Hprec'.
--assert (Hr: Z2R (Ztrunc (scaled_mantissa radix2 fexp r)) = scaled_mantissa radix2 fexp r).
--apply sym_eq.
--now apply scaled_mantissa_generic.
--revert Hr.
--case_eq (Ztrunc (scaled_mantissa radix2 fexp r)).
--(* *)
--intros _ Hx.
--repeat split.
--apply Rmult_eq_reg_r with (bpow radix2 (- canonic_exponent radix2 fexp r)).
--now rewrite Rmult_0_l.
--apply Rgt_not_eq.
--apply bpow_gt_0.
--(* *)
--intros p Hp Hx.
--case binary_round_correct ; intros Hv.
--unfold F2R, Fnum, Fexp, cond_Zopp.
--rewrite Hx, scaled_mantissa_bpow.
--rewrite round_generic with (1 := Gx).
--rewrite Rlt_bool_true with (1 := Bx).
--intros H.
--split.
--rewrite is_finite_FF2B.
--revert H.
--assert (0 <> r)%R.
--intros H.
--rewrite <- H, scaled_mantissa_0 in Hx.
--now apply (Z2R_neq 0 (Zpos p)).
--now case binary_round_sign_shl.
--now rewrite B2R_FF2B.
--(* *)
--intros p Hp Hx.
--case binary_round_correct ; intros Hv.
--unfold F2R, Fnum, Fexp, cond_Zopp, Zopp.
--rewrite Hx, scaled_mantissa_bpow.
--rewrite round_generic with (1 := Gx).
-+generalize (binary_normalize_correct prec emax Hprec' Hemax' rnd (Ztrunc (scaled_mantissa radix2 fexp r)) (canonic_exp radix2 fexp r) false).
-+unfold r.
-+elim generic_format_round...
-+fold emin r.
-+rewrite round_generic...
- rewrite Rlt_bool_true with (1 := Bx).
--intros H.
--split.
--rewrite is_finite_FF2B.
--revert H.
--assert (0 <> r)%R.
--intros H.
--rewrite <- H, scaled_mantissa_0 in Hx.
--now apply (Z2R_neq 0 (Zneg p)).
--now case binary_round_sign_shl.
--now rewrite B2R_FF2B.
-+now split.
-+apply generic_format_round...
-+apply fexp'.
-+apply fexp'.
- Qed.
- 
- Theorem r_to_sd_format :
-@@ -109,15 +65,14 @@ Theorem r_to_sd_format :
-   FLT_format radix2 emin prec x ->
-   (Rabs x < bpow radix2 emax)%R ->
-   r_to_sd rnd x = x :>R.
--Proof.
-+Proof with auto with typeclass_instances.
- intros rnd x Fx Bx.
- assert (Gx: generic_format radix2 fexp x).
--apply -> FLT_format_generic.
-+apply generic_format_FLT.
- apply Fx.
--exact Hprec'.
--pattern x at 2 ; rewrite <- round_generic with (rnd := round_mode rnd) (1 := Gx).
-+pattern x at 2 ; rewrite <- round_generic with (rnd := round_mode rnd) (2 := Gx)...
- refine (proj2 (r_to_sd_correct _ _ _)).
--now rewrite round_generic with (1 := Gx).
-+rewrite round_generic...
- Qed.
- 
- End r_to_sd.
-@@ -152,10 +107,10 @@ rewrite <- Zsucc_pred.
- generalize (Zeq_bool_eq _ _ H1). clear.
- rewrite Fcalc_digits.Z_of_nat_S_digits2_Pnat.
- intros H.
--apply (Fcalc_digits.Zpower_gt_digits Fcalc_digits.radix2 (Zpos prec) (Zpos m)).
-+apply (Fcalc_digits.Zpower_gt_Zdigits Fcalc_digits.radix2 (Zpos prec) (Zpos m)).
- revert H.
- unfold FLT_exp.
--generalize (Fcalc_digits.digits Fcalc_digits.radix2 (Zpos m)).
-+generalize (Fcore_digits.Zdigits Fcalc_digits.radix2 (Zpos m)).
- intros ; zify ; omega.
- apply bpow_le.
- now apply Zle_bool_imp_le.
-@@ -172,6 +127,23 @@ Definition rnd_of_mode (m:mode) :=
- 
- (** Single precision *)
- 
-+Definition binary32 := binary_float 24 128.
-+
-+Let Hprec32 : (0 < 24)%Z.
-+apply refl_equal.
-+Qed.
-+
-+Let Hprec32_emax : (24 < 128)%Z.
-+apply refl_equal.
-+Qed.
-+
-+Definition b32_opp := Bopp 24 128.
-+Definition b32_plus := Bplus _ _ Hprec32 Hprec32_emax.
-+Definition b32_minus := Bminus _ _ Hprec32 Hprec32_emax.
-+Definition b32_mult := Bmult _ _ Hprec32 Hprec32_emax.
-+Definition b32_div := Bdiv _ _ Hprec32 Hprec32_emax.
-+Definition b32_sqrt := Bsqrt _ _ Hprec32 Hprec32_emax.
-+
- Record single : Set := mk_single {
-   single_float : binary32;
-   single_value := (single_float : R);
-@@ -229,12 +201,12 @@ Theorem bounded_real_no_overflow_single
-   forall m x,
-   (Rabs x <= max_single)%R ->
-   no_overflow_single m x.
--Proof.
-+Proof with auto with typeclass_instances.
- intros m x Hx.
- apply Rabs_le.
- assert (generic_format radix2 (FLT_exp (-149) 24) max_single).
--apply generic_format_canonic_exponent.
--unfold canonic_exponent.
-+apply generic_format_F2R.
-+unfold canonic_exp.
- rewrite ln_beta_F2R. 2: easy.
- rewrite (ln_beta_unique _ _ 24).
- easy.
-@@ -245,31 +217,40 @@ now apply Z2R_lt.
- generalize (Rabs_le_inv _ _ Hx).
- split.
- erewrite <- round_generic with (x := Ropp max_single).
--apply round_monotone with (2 := proj1 H0).
--now apply FLT_exp_correct.
-+unfold round_single.
-+apply round_le...
-+apply FLT_exp_valid. easy.
-+easy.
-+apply valid_rnd_round_mode.
- now apply generic_format_opp.
--rewrite <- round_generic with (rnd := round_mode (rnd_of_mode m)) (1 := H).
--apply round_monotone with (2 := proj2 H0).
--now apply FLT_exp_correct.
-+unfold round_single.
-+apply round_le_generic...
-+apply FLT_exp_valid.
-+apply Hprec'...
-+easy.
- Qed.
- 
- Theorem round_single_monotonic :
-   forall m x y, (x <= y)%R ->
-   (round_single m x <= round_single m y)%R.
--Proof.
-+Proof with auto with typeclass_instances.
- intros m x y Hxy.
--apply round_monotone with (2 := Hxy).
--now apply FLT_exp_correct.
-+unfold round_single.
-+apply round_le...
-+apply FLT_exp_valid.
-+apply Hprec'...
- Qed.
- 
- Theorem round_single_idempotent :
-   forall m1 m2 x,
-   round_single m1 (round_single m2 x) = round_single m2 x.
--Proof.
-+Proof with auto with typeclass_instances.
- intros m1 m2 x.
- apply round_generic.
--apply generic_format_round.
--now apply FLT_exp_correct.
-+apply valid_rnd_round_mode.
-+apply generic_format_round...
-+apply FLT_exp_valid.
-+apply Hprec'...
- Qed.
- 
- Theorem round_down_single_neg :
-@@ -295,8 +276,9 @@ Theorem round_single_down_le :
-   (round_single down x <= x)%R.
- Proof.
- intros x.
--eapply round_DN_pt.
--now apply FLT_exp_correct.
-+eapply round_DN_pt...
-+apply FLT_exp_valid.
-+apply Hprec'. easy.
- Qed.
- 
- Theorem round_up_single_ge :
-@@ -305,12 +287,30 @@ Theorem round_up_single_ge :
- Proof.
- intros x.
- apply Rle_ge.
--eapply round_UP_pt.
--now apply FLT_exp_correct.
-+eapply round_UP_pt...
-+apply FLT_exp_valid.
-+apply Hprec'. easy.
- Qed.
- 
- (** Double precision *)
- 
-+Definition binary64 := binary_float 53 1024.
-+
-+Let Hprec64 : (0 < 53)%Z.
-+apply refl_equal.
-+Qed.
-+
-+Let Hprec64_emax : (53 < 1024)%Z.
-+apply refl_equal.
-+Qed.
-+
-+Definition b64_opp := Bopp 53 1024.
-+Definition b64_plus := Bplus _ _ Hprec64 Hprec64_emax.
-+Definition b64_minus := Bminus _ _ Hprec64 Hprec64_emax.
-+Definition b64_mult := Bmult _ _ Hprec64 Hprec64_emax.
-+Definition b64_div := Bdiv _ _ Hprec64 Hprec64_emax.
-+Definition b64_sqrt := Bsqrt _ _ Hprec64 Hprec64_emax.
-+
- Record double : Set := mk_double {
-   double_float : binary64;
-   double_value := (double_float : R);
-@@ -368,12 +368,12 @@ Theorem bounded_real_no_overflow_double
-   forall m x,
-   (Rabs x <= max_double)%R ->
-   no_overflow_double m x.
--Proof.
-+Proof with auto with typeclass_instances.
- intros m x Hx.
- apply Rabs_le.
- assert (generic_format radix2 (FLT_exp (-1074) 53) max_double).
--apply generic_format_canonic_exponent.
--unfold canonic_exponent.
-+apply generic_format_F2R.
-+unfold canonic_exp.
- rewrite ln_beta_F2R. 2: easy.
- rewrite (ln_beta_unique _ _ 53).
- easy.
-@@ -384,31 +384,40 @@ now apply Z2R_lt.
- generalize (Rabs_le_inv _ _ Hx).
- split.
- erewrite <- round_generic with (x := Ropp max_double).
--apply round_monotone with (2 := proj1 H0).
--now apply FLT_exp_correct.
-+unfold round_double.
-+apply round_le...
-+apply FLT_exp_valid. easy.
-+easy.
-+apply valid_rnd_round_mode.
- now apply generic_format_opp.
--rewrite <- round_generic with (rnd := round_mode (rnd_of_mode m)) (1 := H).
--apply round_monotone with (2 := proj2 H0).
--now apply FLT_exp_correct.
-+unfold round_double.
-+apply round_le_generic...
-+apply FLT_exp_valid.
-+apply Hprec'...
-+easy.
- Qed.
- 
- Theorem round_double_monotonic :
-   forall m x y, (x <= y)%R ->
-   (round_double m x <= round_double m y)%R.
--Proof.
-+Proof with auto with typeclass_instances.
- intros m x y Hxy.
--apply round_monotone with (2 := Hxy).
--now apply FLT_exp_correct.
-+unfold round_double.
-+apply round_le...
-+apply FLT_exp_valid.
-+apply Hprec'...
- Qed.
- 
- Theorem round_double_idempotent :
-   forall m1 m2 x,
-   round_double m1 (round_double m2 x) = round_double m2 x.
--Proof.
-+Proof with auto with typeclass_instances.
- intros m1 m2 x.
- apply round_generic.
--apply generic_format_round.
--now apply FLT_exp_correct.
-+apply valid_rnd_round_mode.
-+apply generic_format_round...
-+apply FLT_exp_valid.
-+apply Hprec'...
- Qed.
- 
- Theorem round_down_double_neg :
-@@ -434,8 +443,9 @@ Theorem round_double_down_le :
-   (round_double down x <= x)%R.
- Proof.
- intros x.
--eapply round_DN_pt.
--now apply FLT_exp_correct.
-+eapply round_DN_pt...
-+apply FLT_exp_valid.
-+apply Hprec'. easy.
- Qed.
- 
- Theorem round_up_double_ge :
-@@ -444,8 +454,9 @@ Theorem round_up_double_ge :
- Proof.
- intros x.
- apply Rle_ge.
--eapply round_UP_pt.
--now apply FLT_exp_correct.
-+eapply round_UP_pt...
-+apply FLT_exp_valid.
-+apply Hprec'. easy.
- Qed.
- 
- (** Quad precision *)
-@@ -566,8 +577,8 @@ unfold F2R. simpl.
- split.
- now rewrite Rmult_1_r.
- now split.
--apply <- FLT_format_generic.
--2: easy.
-+apply FLT_format_generic.
-+apply Hprec'. easy.
- change 2%Z with (radix_val radix2) in Bz.
- destruct z as [|z|z] ; unfold Zabs in Bz.
- apply generic_format_0.
---- ./lib/coq/WhyFloatsStrict.v.orig	2011-10-24 09:21:06.000000000 -0600
-+++ ./lib/coq/WhyFloatsStrict.v	2012-01-11 15:42:11.453663887 -0700
-@@ -155,30 +155,13 @@ repeat split.
- exact H2.
- Qed.
- 
--Axiom Bplus_correct : (* the statement from Flocq 1.4 is not strong enough;
--                         the axiom can be removed once the library is converted to Flocq 2.0 *)
--  forall (prec emax : Z) (Hprec : (0 < prec)%Z) (Hmax : (prec < emax)%Z)
--         (m : Fappli_IEEE.mode) (x y : binary_float prec emax),
--  is_finite prec emax x = true ->
--  is_finite prec emax y = true ->
--  if Rlt_bool (Rabs (round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m)
--       (B2R prec emax x + B2R prec emax y))) (bpow radix2 emax)
--  then
--    B2R prec emax (Bplus prec emax Hprec Hmax m x y) =
--      round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m) (B2R prec emax x + B2R prec emax y) /\
--    is_finite prec emax (Bplus prec emax Hprec Hmax m x y) = true
--  else
--    B2FF prec emax (Bplus prec emax Hprec Hmax m x y) =
--      binary_overflow prec emax m (Bsign prec emax x) /\
--    Bsign prec emax x = Bsign prec emax y.
--
- Lemma add_single_specification :
-   forall m (x y : single),
-   no_overflow_single m (single_value x + single_value y) ->
-   exists z, add_single_post m x y z.
- Proof.
- intros m x y Br.
--refine (_ (Bplus_correct 24 128 (refl_equal Lt) (refl_equal Lt) (rnd_of_mode m) (single_float x) (single_float y)
-+refine (_ (Bplus_correct 24 128 Hprec32 Hprec32_emax (rnd_of_mode m) (single_float x) (single_float y)
-   (single_finite x) (single_finite y))).
- rewrite Rlt_bool_true.
- 2: now apply no_overflow_single_bounded.
-@@ -189,27 +172,13 @@ repeat split.
- exact H1.
- Qed.
- 
--Axiom Bmult_correct : (* the statement from Flocq 1.4 is not strong enough;
--                         the axiom can be removed once the library is converted to Flocq 2.0 *)
--  forall (prec emax : Z) (Hprec : (0 < prec)%Z) (Hmax : (prec < emax)%Z)
--         (m : Fappli_IEEE.mode) (x y : binary_float prec emax),
--  if Rlt_bool (Rabs (round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m)
--       (B2R prec emax x * B2R prec emax y))) (bpow radix2 emax)
--  then
--    B2R prec emax (Bmult prec emax Hprec Hmax m x y) =
--      round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m) (B2R prec emax x * B2R prec emax y) /\
--    is_finite prec emax (Bmult prec emax Hprec Hmax m x y) = andb (is_finite prec emax x) (is_finite prec emax y)
--  else
--    B2FF prec emax (Bmult prec emax Hprec Hmax m x y) =
--      binary_overflow prec emax m (xorb (Bsign prec emax x) (Bsign prec emax y)).
--
- Lemma mul_single_specification :
-   forall m (x y : single),
-   no_overflow_single m (single_value x * single_value y) ->
-   exists z, mul_single_post m x y z.
- Proof.
- intros m x y Br.
--refine (_ (Bmult_correct 24 128 (refl_equal Lt) (refl_equal Lt) (rnd_of_mode m) (single_float x) (single_float y))).
-+refine (_ (Bmult_correct 24 128 Hprec32 Hprec32_emax (rnd_of_mode m) (single_float x) (single_float y))).
- rewrite Rlt_bool_true.
- 2: now apply no_overflow_single_bounded.
- fold b32_mult.
-@@ -220,28 +189,13 @@ repeat split.
- exact H1.
- Qed.
- 
--Axiom Bdiv_correct : (* the statement from Flocq 1.4 is not strong enough;
--                        the axiom can be removed once the library is converted to Flocq 2.0 *)
--  forall (prec emax : Z) (Hprec : (0 < prec)%Z) (Hmax : (prec < emax)%Z)
--    (m : Fappli_IEEE.mode) (x y : binary_float prec emax),
--  B2R prec emax y <> 0%R ->
--  if Rlt_bool (Rabs (round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m)
--       (B2R prec emax x / B2R prec emax y))) (bpow radix2 emax)
--  then
--    B2R prec emax (Bdiv prec emax Hprec Hmax m x y) =
--      round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m) (B2R prec emax x / B2R prec emax y) /\
--    is_finite prec emax (Bdiv prec emax Hprec Hmax m x y) = is_finite prec emax x
--  else
--    B2FF prec emax (Bdiv prec emax Hprec Hmax m x y) =
--      binary_overflow prec emax m (xorb (Bsign prec emax x) (Bsign prec emax y)).
--
- Lemma div_single_specification :
-   forall m (x y : single), single_value y <> R0 ->
-   no_overflow_single m (single_value x / single_value y) ->
-   exists z, div_single_post m x y z.
- Proof.
- intros m x y Zy Br.
--refine (_ (Bdiv_correct 24 128 (refl_equal Lt) (refl_equal Lt) (rnd_of_mode m) (single_float x) (single_float y) Zy)).
-+refine (_ (Bdiv_correct 24 128 Hprec32 Hprec32_emax (rnd_of_mode m) (single_float x) (single_float y) Zy)).
- rewrite Rlt_bool_true.
- 2: now apply no_overflow_single_bounded.
- fold b32_div.
-@@ -252,20 +206,12 @@ repeat split.
- exact H1.
- Qed.
- 
--Axiom Bsqrt_correct : (* the statement from Flocq 1.4 is not strong enough;
--                         the axiom can be removed once the library is converted to Flocq 2.0 *)
--  forall (prec emax : Z) (Hprec : (0 < prec)%Z) (Hmax : (prec < emax)%Z)
--         (m : Fappli_IEEE.mode) (x : binary_float prec emax),
--  B2R prec emax (Bsqrt prec emax Hprec Hmax m x) =
--    round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m) (sqrt (B2R prec emax x)) /\
--  is_finite prec emax (Bsqrt prec emax Hprec Hmax m x) = match x with B754_zero _ => true | B754_finite false _ _ _ => true | _ => false end.
--
- Lemma sqrt_single_specification :
-   forall m (x : single), Rle 0 (single_value x) ->
-   exists z, sqrt_single_post m x z.
- Proof.
- intros m x Zx.
--refine (_ (Bsqrt_correct 24 128 (refl_equal Lt) (refl_equal Lt) (rnd_of_mode m) (single_float x))).
-+refine (_ (Bsqrt_correct 24 128 Hprec32 Hprec32_emax (rnd_of_mode m) (single_float x))).
- fold b32_sqrt.
- intros (H1, H2).
- assert (is_finite 24 128 (b32_sqrt (rnd_of_mode m) (single_float x)) = true).
---- ./lib/coq/JessieGappa.v.orig	2011-10-24 09:21:06.000000000 -0600
-+++ ./lib/coq/JessieGappa.v	2012-01-11 15:41:08.874131235 -0700
-@@ -571,7 +571,7 @@ unfold min_gen_float, min_float2.
- case F ; apply bpow_gt_0.
- rewrite <- round_of_min_gen with F m.
- revert Bx1.
--case F ; apply round_monotone ; now apply FLT_exp_correct.
-+case F ; apply round_le...
- Save.
- 
- Lemma negative_constant : forall f m x, 
-@@ -592,7 +592,7 @@ case F ; apply bpow_ge_0.
- apply Rle_lt_trans with (- min_gen_float F)%R.
- rewrite <- round_of_opp_min_gen with F m.
- revert Bx2.
--case F ; apply round_monotone ; now apply FLT_exp_correct.
-+case F ; apply round_le...
- apply Ropp_lt_gt_0_contravar.
- unfold min_gen_float, min_float2.
- case F ; apply bpow_gt_0.
-@@ -602,7 +602,7 @@ Lemma round_increasing: forall f m x y,
-       (x <= y)%R -> (round_float f m x <= round_float f m y)%R.
- Proof.
- intros F m x y.
--case F ; apply round_monotone ; now apply FLT_exp_correct.
-+case F ; apply round_le...
- Save.
- 
- Lemma round_greater_min: forall f m x, 
diff --git a/why.spec b/why.spec
deleted file mode 100644
index 1ff7d47..0000000
--- a/why.spec
+++ /dev/null
@@ -1,556 +0,0 @@
-# Whether coq is available
-%ifarch %{ocaml_arches}
-%global has_coq 1
-%else
-%global has_coq 0
-%endif
-
-# 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)
-
-# Don't create debuginfo; it's not particularly useful for OCaml programs.
-%global debug_package %{nil}
-
-Name:           why
-Version:        2.30
-Release:        5%{?dist}
-Summary:        Software verification platform
-
-Group:          Applications/Engineering
-License:        LPGLv2 with exceptions
-URL:            http://why.lri.fr/
-Source0:        http://why.lri.fr/download/why-%{version}.tar.gz
-Source1:        README.why-gwhy.Fedora
-Source2:        README.why-coq.Fedora
-Source3:        README.why
-Source4:        gwhy.desktop
-Source5:        gwhy-icon.png
-Source6:        min.mlw
-Source7:        min_why.why.result
-Source8:        http://krakatoa.lri.fr/manual/krakatoa.pdf
-Source9:        jessie.desktop
-Source10:       div.pvs
-Source11:       rem.pvs
-Source12:       patch_jessie_pvs
-
-# The gwhy execution shell script is not particularly informative
-# about when bad parameters are passed to it - this patch fixes that.
-# Upstream has been informed about this issue and a better fix is on
-# their todo list
-Patch0:         gwhy-2.26.patch
-
-# 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.
-Patch1:         why-2.30-Makefile.in.patch
-
-# This patch fixes some mildly bitrotted APRON support code.
-# Applied upstream.
-Patch2:         why-apron.patch
-
-# This patch updates the flocq usage for flocq 2.0.0.  It will be sent upstream.
-Patch3:         why-flocq2.patch
-
-BuildRequires:  auto-destdir
-BuildRequires:  cvc3
-BuildRequires:  desktop-file-utils
-BuildRequires:  emacs-nox xemacs xemacs-packages-extra
-BuildRequires:  frama-c-devel
-BuildRequires:  gappalib-coq
-BuildRequires:  gtk2-devel
-BuildRequires:  ocaml
-BuildRequires:  ocaml-apron-devel
-BuildRequires:  ocaml-camlp4-devel
-BuildRequires:  ocaml-lablgtk-devel
-BuildRequires:  ocaml-ocamldoc
-BuildRequires:  ocaml-ocamlgraph-devel
-%if %{has_coq}
-BuildRequires:  coq
-%endif
-%if %{has_pvs}
-BuildRequires:  pvs
-%endif
-
-# Only build on arches that support ocaml
-ExclusiveArch: %{ocaml_arches}
-
-# Filter out names that should not be exposed externally
-%global __requires_exclude ocaml\\\(((Ast)|(Cc)|(Env)|(Error)|(Loc)|(Logic)|(Logic_decl)|(Misc)|(Parser)|(Project)|(Ptree)|(Types))\\\)
-%global __provides_exclude ocaml\\\(((Lexer)|(Lib)|(Loc)|(Output)|(Parser)|(Project)|(Report)|(Xml))\\\)
-
-%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 gwhy
-Group:          Applications/Engineering
-Summary:        IDE for Why software verification platform
-Requires:       %{name}%{?_isa} = %{version}-%{release}, zenity
-
-%description gwhy
-Gwhy is an optional graphical user interface for the Why software
-coordination platform.  It assists in the coordination of dispatching
-assertions that need to be proven to different theorem provers by
-providing an interface to do this and also supports inspection of why
-input files.
-
-%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
-
-%if %{has_coq}
-%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.
-%endif
-
-%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 emacs
-Summary:        Emacs support file for why files
-Group:          Development/Languages
-Requires:       %{name} = %{version}-%{release}
-Requires:       emacs(bin)
-BuildArch:      noarch
-
-%description emacs
-This package contains an Emacs support file for working with why files.
-
-%package emacs-el
-Summary:        Emacs source file for why support
-Group:          Development/Languages
-Requires:       %{name}-emacs = %{version}-%{release}
-BuildArch:      noarch
-
-%description emacs-el
-This package contains the Emacs source file for the Emacs why support.
-This package is not needed to use the Emacs support.
-
-%package xemacs
-Summary:        XEmacs support file for why files
-Group:          Development/Languages
-Requires:       %{name} = %{version}-%{release}
-Requires:       xemacs(bin)
-BuildArch:      noarch
-
-%description xemacs
-This package contains an XEmacs support file for working with why files.
-
-%package xemacs-el
-Summary:        XEmacs source file for why support
-Group:          Development/Languages
-Requires:       %{name}-xemacs = %{version}-%{release}
-BuildArch:      noarch
-
-%description xemacs-el
-This package contains the XEmacs source file for the XEmacs why support.
-This package is not needed to use the Emacs support.
-
-%package all
-Group:          Applications/Engineering
-Summary:        Complete Why software verification platform suite
-Requires:       why%{?_isa} = %{version}-%{release}
-Requires:       why-gwhy%{?_isa} = %{version}-%{release}
-Requires:       why-jessie%{?_isa} = %{version}-%{release}
-%if %{has_coq}
-Requires:       why-coq%{?_isa} = %{version}-%{release}
-%endif
-%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
-%patch0
-%patch1
-%patch2
-%patch3
-
-cp -p %SOURCE1 %SOURCE2 %SOURCE6 %SOURCE7 ./
-
-# Fix missing DESTDIRs in the makefile
-sed -e 's|$(COQLIB)/user-contrib/Why|$(DESTDIR)$(COQLIB)/user-contrib/Why|' \
-    -e 's|$(PVSLIB)/why|$(DESTDIR)$(PVSLIB)/why|' \
-    -i Makefile.in
-
-%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 a doubly utf8-encoded file
-%fix_encoding examples/sqrt/sqrt_why.v UTF-8 ISO-8859-1
-
-# 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 include and a missing rpath
-sed -e "s|-I +apron|-I +apron -I +mlgmpidl|" \
-    -e "s|-lpolkaMPQ_caml|-Wl,-rpath,%{_libdir}/ocaml/apron|" \
-    -i 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
-
-# Update the version numbers of external programs
-# Also, command "pvs" is LVM2's /sbin/pvs, so rename "pvs" to pvs-sbcl:
-sed -e 's/versions_ok = \["0\.93"\]/versions_ok = ["0.93";"0.94"]/' \
-    -e 's/versions_ok = \["1\.0\.25";.*\]/versions_ok = ["1.0.31"]/' \
-    -e 's/versions_ok = \["2.2"\]/versions_ok = ["2.4.1"]/' \
-    -e 's/versions_ok = \["8\.0";.*\]/versions_ok = ["8.3pl2"]/' \
-    -e 's/versions_ok = \["4\.1"\]/versions_ok = ["5.0"]/' \
-    -e 's/command = "pvs"/command = "pvs-sbcl"/' \
-    -e 's/PVS, (pvs, \["pvs"\]);/PVS, (pvs, ["pvs-sbcl" ; "pvs"]);/' \
-    -i tools/dpConfig.ml
-sed -e 's/pvs/pvs-sbcl/' -i configure
-
-%if %{has_coq}
-%configure --enable-apron --enable-verbosemake
-%else
-%configure --enable-apron --enable-verbosemake COQC=no
-%endif
-make %{opt_option}
-
-# Strip binaries (the Makefile misses some of them)
-strip bin/why-cpulimit
-strip frama-c-plugin/Jessie.cmxs
-%if %opt
-strip bin/rv_merge.opt bin/simplify2why.opt bin/tool-stat.opt \
-      bin/why2html.opt bin/why-dp.opt bin/why-obfuscator.opt bin/why-stat.opt
-%endif
-
-%install
-# Avoid a bug in PVS batch mode when using emacs
-make install DESTDIR=%{buildroot} %{opt_option} PVSLIB=%{_libdir}/pvs/lib \
-     PVSEMACS=xemacs
-
-# Fix a small bug in their Makefile: if no Coq, NO .v files should be installed
-%if ! %{has_coq}
-rm -f `find %{buildroot}%{_datadir}/coq -name '*.v'`
-%endif
-
-# If no PVS, no .pvs files should be installed
-%if ! %{has_pvs}
-rm -fr %{buildroot}%{_libdir}/pvs
-%endif
-
-# Install desktop icon and menu entry
-%global why_data_dir %{_datadir}/why
-mkdir -p %{buildroot}%{why_data_dir}
-cp -p %{SOURCE5} %{buildroot}%{why_data_dir}
-sed -e 's|ICON-LOCATION-BASE|%{why_data_dir}|' %{SOURCE4} > gwhy.desktop
-desktop-file-install --vendor="fedora" \
- --dir=%{buildroot}%{_datadir}/applications gwhy.desktop
-sed -e 's|ICON-LOCATION-BASE|%{why_data_dir}|' %{SOURCE9} > jessie.desktop
-desktop-file-install --vendor="fedora" \
- --dir=%{buildroot}%{_datadir}/applications jessie.desktop
-
-%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 %{SOURCE10} %{SOURCE11} %{buildroot}%{_libdir}/pvs/lib/ints/
-cp -p %{SOURCE12}             %{buildroot}%{_bindir}/
-%endif
-
-%global why_doc_dir %{_defaultdocdir}/%{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 %{SOURCE8} %{SOURCE3} CHANGES COPYING LICENSE 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
-%if %opt
-%global why bin/why.opt
-%else
-%global why bin/why.byte
-%endif
-WHYLIB=lib %why --why --output min.why min.mlw
-diff -u min.why min_why.why.result  # Show differences from correct result.
-
-%files
-%{_bindir}/*
-%{_libdir}/why/
-%{_mandir}/man1/why.1*
-%{why_doc_dir}/
-# This last example is really an example only for Coq - only .v files
-%exclude %{why_examples_dir}mlw/string-matching/
-# why-gwhy:
-%exclude %{_bindir}/gwhy*
-# why-jessie
-%exclude %{_bindir}/jessie
-# why-pvs-support:
-%exclude %{_bindir}/patch_jessie_pvs
-
-%files gwhy
-%doc README.why-gwhy.Fedora
-%{_bindir}/gwhy
-%{_bindir}/gwhy-bin
-%{why_data_dir}/
-%{_datadir}/applications/fedora-gwhy.desktop
-
-%files jessie
-%{_bindir}/jessie
-%{_libdir}/jessie/
-%{_libdir}/frama-c/plugins/Jessie.*
-%{_datadir}/applications/fedora-jessie.desktop
-
-%if %{has_coq}
-%files coq
-%doc README.why-coq.Fedora
-%{_libdir}/coq/user-contrib/Why/
-%endif
-
-%if %{has_pvs}
-%files pvs-support
-%{_libdir}/pvs/lib/*
-%{_bindir}/patch_jessie_pvs
-%endif
-
-%files emacs
-%{_emacs_sitelispdir}/why.elc
-
-%files emacs-el
-%{_emacs_sitelispdir}/why.el
-
-%files xemacs
-%{_xemacs_sitelispdir}/why.elc
-
-%files xemacs-el
-%{_xemacs_sitelispdir}/why.el
-
-# "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 Jan 11 2012 Jerry James <loganjerry@gmail.com> - 2.30-5
-- Patch to work with flocq 2.0.0
-
-* Tue Dec 27 2011 Jerry James <loganjerry@gmail.com> - 2.30-4
-- Rebuild for coq 8.3pl3
-
-* Tue Dec  6 2011 Jerry James <loganjerry@gmail.com> - 2.30-3
-- Update alt_ergo and yices "okay" version numbers
-
-* Wed Nov 23 2011 Jerry James <loganjerry@gmail.com> - 2.30-2
-- Rebuild with APRON and gappalib-coq support
-
-* Fri Oct 28 2011 Jerry James <loganjerry@gmail.com> - 2.30-1
-- New upstream release
-
-* Thu Jul 14 2011 Jerry James <loganjerry@gmail.com> - 2.29-2
-- Fix broken conditionals
-
-* Mon Jul 11 2011 Jerry James <loganjerry@gmail.com> - 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 <karsten@redhat.com> 2.28-2.2
-- add ppc to excludearch, too. No pvs-sbcl available there
-
-* Wed Apr 13 2011 Karsten Hopp <karsten@redhat.com> 2.28-2.1
-- add ppc64 to excludearch, no sbcl available there
-
-* Mon Feb 07 2011 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.28-2
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild
-
-* Fri Jan 21 2011 Richard W.M. Jones <rjones@gmail.com> - 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 <rjones@gmail.com> - 2.26-2
-- Bump and rebuild for OCaml 3.12.
-
-* Sat Oct 09 2010 David A. Wheeler + Mark Rader <dwheeler@dwheeler.com> - 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 <rjones@gmail.com> - 2.23-2
-- Rebuild to fix dependencies.
-
-* Fri Jan 08 2010 Alan Dunn <amdunn@gmail.com> - 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 <dennis@ausil.us> - 2.17-5
-- Exclude sparc64 s390 s390x  there is no ocaml there
-
-* Fri Aug 07 2009 Alan Dunn <amdunn@gmail.com> - 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 <rel-eng@lists.fedoraproject.org> - 2.17-3
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_12_Mass_Rebuild
-
-* Wed Feb 25 2009 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.17-2
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_11_Mass_Rebuild
-
-* Wed Dec 24 2008 Alan Dunn <amdunn@gmail.com> 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 <amdunn@gmail.com> 2.14-2.1
-- ExcludeArch ppc64 on Fedora 8 due to no ocaml.
-* Fri Aug 1 2008 Alan Dunn <amdunn@gmail.com> 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 <amdunn@gmail.com> 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 <amdunn@gmail.com> 2.13-2
-- Added several patches: fixed Zenon output, completed fix of rename
-  of cpulimit -> why-cpulimit.
-* Wed Jul 23 2008 Alan Dunn <amdunn@gmail.com> 2.13-1
-- Initial Fedora RPM version.
-
-# TODO:
-# If file $HOME/.gwhyrc does not exist, autorun "why-config".
-# Finish packaging/integrating "APRON" (for Inference of annotations)
-