15 changed files with 1548 additions and 1 deletions
--- a/.gitignore
+++ b/.gitignore
@ -0,0 +1,6 @@
+/krakatoa.pdf
+/why-icons.tar.xz
+/why-2.36.tar.gz
+/why-2.38.tar.gz
+/why-2.39.tar.gz
+/why-2.40.tar.gz
--- a/README.why
+++ 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.
--- a/README.why-coq.Fedora
+++ 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.
--- a/dead.package
+++ b/dead.package
@ -1 +0,0 @@
-Abandoned by upstream and fails to build from source
--- a/div.pvs
+++ 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
+
--- a/jessie.appdata.xml
+++ b/jessie.appdata.xml
@ -0,0 +1,43 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<component type="desktop">
+ <id>jessie.desktop</id>
+ <metadata_license>CC0-1.0</metadata_license>
+ <project_license>LGPL-2.1</project_license>
+ <name>jessie</name>
+ <summary>Interface between why and Frama-C</summary>
+ <description>
+  <p>
+   Jessie is an interface between why and Frama-C.
+  </p>
+  <p>
+   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.
+  </p>
+ </description>
+ <screenshots>
+  <screenshot type="default">
+   <image>http://krakatoa.lri.fr/jessie/max_why3ide.png</image>
+   <caption>Interactive proof session</caption>
+  </screenshot>
+  <screenshot>
+   <image>http://krakatoa.lri.fr/jessie/max_ptr_why3ide.png</image>
+   <caption>Max function proof</caption>
+  </screenshot>
+  <screenshot>
+   <image>http://krakatoa.lri.fr/jessie/binary_search_raw.png</image>
+   <caption>Binary search function proof</caption>
+  </screenshot>
+  <screenshot>
+   <image>http://krakatoa.lri.fr/jessie/binary_search_ovfl.png</image>
+   <caption>Binary search arithmetic overflow</caption>
+  </screenshot>
+  <screenshot>
+   <image>http://krakatoa.lri.fr/jessie/binary_search_behav.png</image>
+   <caption>Binar search function behavior</caption>
+  </screenshot>
+ </screenshots>
+ <update_contact>loganjerry@gmail.com</update_contact>
+ <url type="homepage">http://krakatoa.lri.fr/</url>
+ <url type="bugtracker">https://gforge.inria.fr/tracker/?atid=4012&amp;group_id=999&amp;func=browse</url>
+</component>
--- a/jessie.desktop
+++ 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;
--- a/59
+++ b/59
@ -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
+
--- a/rem.pvs
+++ 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
+
--- a/3
+++ b/3
@ -0,0 +1,3 @@
+SHA512 (krakatoa.pdf) = 5d0f4e6b938ddc1eafa48264c02cf99e68f776a7e190b997e35fb2cd154627b5d27369886f570cbcfdfe5f3a1929a97a1fec9457a6f6662f83cbb2e51f65ca04
+SHA512 (why-2.40.tar.gz) = e99f528ab2a3030c5ed8509ec45e75dc2f3dc2ed92fe1213c2b92a2dc700e2d9c32bc765751b2660cc1f3a6e110b4687a4262779fdae52faaaf144c411712972
+SHA512 (why-icons.tar.xz) = d6ca78cf09540f5742564912470fb8c49f7d11ca16cd8bb60c8790af10c1591198f6020bd792cff8e3464f762b7ef0a690d3e4ba1a2cf670c286c8056d266bc3
--- a/why-num.patch
+++ b/why-num.patch
@ -0,0 +1,596 @@
+--- atp/cooper.ml.orig	2018-01-23 03:07:35.000000000 -0700
+++ atp/cooper.ml	2018-02-11 20:48:48.754907226 -0700
+@@ -38,10 +38,10 @@
+ (* Lift operations up to numerals.                                           *)
+ (* ------------------------------------------------------------------------- *)
+ 
+-let mk_numeral n = Fn(string_of_num n,[]);;
+let mk_numeral n = Fn(Z.to_string n,[]);;
+ 
+ let dest_numeral =
+-  function (Fn(ns,[])) -> num_of_string ns
+  function (Fn(ns,[])) -> Z.of_string ns
+          | _ -> failwith "dest_numeral";;
+ 
+ let is_numeral = can dest_numeral;;
+@@ -59,12 +59,12 @@ let numeral2 fn m n = mk_numeral(fn (des
+ (* ------------------------------------------------------------------------- *)
+ 
+ let rec linear_cmul n tm =
+-  if n =/ Int 0 then Fn("0",[]) else
+  if Z.equal n Z.zero then Fn("0",[]) else
+   match tm with
+     Fn("+",[Fn("*",[c1; x1]); rest]) ->
+-        Fn("+",[Fn("*",[numeral1 (( */ ) n) c1; x1]);
+        Fn("+",[Fn("*",[numeral1 (Z.mul n) c1; x1]);
+                         linear_cmul n rest])
+-  | k -> numeral1 (( */ ) n) k;;
+  | k -> numeral1 (Z.mul n) k;;
+ 
+ let earlierv vars (Var x) (Var y) = earlier vars x y;;
+ 
+@@ -73,7 +73,7 @@ let rec linear_add vars tm1 tm2 =
+    (Fn("+",[Fn("*",[c1; x1]); rest1]),
+     Fn("+",[Fn("*",[c2; x2]); rest2])) ->
+         if x1 = x2 then
+-          let c = numeral2 (+/) c1 c2 in
+          let c = numeral2 Z.add c1 c2 in
+           if c = Fn("0",[]) then linear_add vars rest1 rest2
+           else Fn("+",[Fn("*",[c; x1]); linear_add vars rest1 rest2])
+         else if earlierv vars x1 x2 then
+@@ -84,9 +84,9 @@ let rec linear_add vars tm1 tm2 =
+         Fn("+",[Fn("*",[c1; x1]); linear_add vars rest1 tm2])
+   | (_,Fn("+",[Fn("*",[c2; x2]); rest2])) ->
+         Fn("+",[Fn("*",[c2; x2]); linear_add vars tm1 rest2])
+-  | _ -> numeral2 (+/) tm1 tm2;;
+  | _ -> numeral2 Z.add tm1 tm2;;
+ 
+-let linear_neg tm = linear_cmul (Int(-1)) tm;;
+let linear_neg tm = linear_cmul Z.minus_one tm;;
+ 
+ let linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2);;
+ 
+@@ -116,7 +116,7 @@ let mkatom vars p t = Atom(R(p,[Fn("0",[
+ let linform vars fm =
+   match fm with
+     Atom(R("divides",[c;t])) ->
+-        let c' = mk_numeral(abs_num(dest_numeral c)) in
+        let c' = mk_numeral(Z.abs(dest_numeral c)) in
+         Atom(R("divides",[c';lint vars t]))
+   | Atom(R("=",[s;t])) -> mkatom vars "=" (Fn("-",[t;s]))
+   | Atom(R("<",[s;t])) -> mkatom vars "<" (Fn("-",[t;s]))
+@@ -144,11 +144,11 @@ let rec posineq fm =
+ let rec formlcm x fm =
+   match fm with
+     Atom(R(p,[_;Fn("+",[Fn("*",[c;y]);z])])) when y = x ->
+-        abs_num(dest_numeral c)
+        Z.abs(dest_numeral c)
+   | Not(p) -> formlcm x p
+   | And(p,q) -> lcm_num (formlcm x p) (formlcm x q)
+   | Or(p,q) -> lcm_num (formlcm x p) (formlcm x q)
+-  | _ -> Int 1;;
+  | _ -> Z.one;;
+ 
+ (* ------------------------------------------------------------------------- *)
+ (* Adjust all coefficients of x in formula; fold in reduction to +/- 1.      *)
+@@ -157,10 +157,10 @@ let rec formlcm x fm =
+ let rec adjustcoeff x l fm =
+   match fm with
+     Atom(R(p,[d; Fn("+",[Fn("*",[c;y]);z])])) when y = x ->
+-        let m = l // dest_numeral c in
+-        let n = if p = "<" then abs_num(m) else m in
+-        let xtm = Fn("*",[mk_numeral(m // n); x]) in
+-        Atom(R(p,[linear_cmul (abs_num m) d;
+        let m = Z.div l (dest_numeral c) in
+        let n = if p = "<" then Z.abs(m) else m in
+        let xtm = Fn("*",[mk_numeral(Z.div m n); x]) in
+        Atom(R(p,[linear_cmul (Z.abs m) d;
+                 Fn("+",[xtm; linear_cmul n z])]))
+   | Not(p) -> Not(adjustcoeff x l p)
+   | And(p,q) -> And(adjustcoeff x l p,adjustcoeff x l q)
+@@ -174,7 +174,7 @@ let rec adjustcoeff x l fm =
+ let unitycoeff x fm =
+   let l = formlcm x fm in
+   let fm' = adjustcoeff x l fm in
+-  if l =/ Int 1 then fm' else
+  if Z.equal l Z.one then fm' else
+   let xp = Fn("+",[Fn("*",[Fn("1",[]);x]); Fn("0",[])]) in
+   And(Atom(R("divides",[mk_numeral l; xp])),adjustcoeff x l fm);;
+ 
+@@ -204,7 +204,7 @@ let rec divlcm x fm =
+   | Not(p) -> divlcm x p
+   | And(p,q) -> lcm_num (divlcm x p) (divlcm x q)
+   | Or(p,q) -> lcm_num (divlcm x p) (divlcm x q)
+-  | _ -> Int 1;;
+  | _ -> Z.one;;
+ 
+ (* ------------------------------------------------------------------------- *)
+ (* Construct the B-set.                                                      *)
+@@ -242,8 +242,8 @@ let rec linrep vars x t fm =
+ (* ------------------------------------------------------------------------- *)
+ 
+ let operations =
+-  ["=",(=/); "<",(</); ">",(>/); "<=",(<=/); ">=",(>=/);
+-   "divides",(fun x y -> mod_num y x =/ Int 0)];;
+  ["=",(Z.equal); "<",(Z.lt); ">",(Z.gt); "<=",(Z.leq); ">=",(Z.geq);
+   "divides",(fun x y -> Z.equal (Z.rem y x) Z.zero)];;
+ 
+ let evalc_atom at =
+   match at with
+@@ -265,7 +265,7 @@ let cooper vars fm =
+         let x = Var x0 in
+         let p = unitycoeff x p0 in
+         let p_inf = simplify(minusinf x p) and bs = bset x p
+-        and js = Int 1 --- divlcm x p in
+        and js = Z.one --- divlcm x p in
+         let p_element j b =
+           linrep vars x (linear_add vars b (mk_numeral j)) p in
+         let stage j = list_disj
+--- atp/defcnf.ml.orig	2018-01-23 03:07:35.000000000 -0700
+++ atp/defcnf.ml	2018-02-11 14:00:03.159892859 -0700
+@@ -55,7 +55,7 @@ let rec nenf fm =
+ (* Make a stylized variable and update the index.                            *)
+ (* ------------------------------------------------------------------------- *)
+ 
+-let mkprop n = Atom(P("p_"^(string_of_num n))),n +/ Int 1;;
+let mkprop n = Atom(P("p_"^(Z.to_string n))),Z.succ n;;
+ 
+ (* ------------------------------------------------------------------------- *)
+ (* Make n large enough that "v_m" won't clash with s for any m >= n          *)
+@@ -67,7 +67,7 @@ let max_varindex pfx =
+     let l = String.length s in
+     if l <= m or String.sub s 0 m <> pfx then n else
+     let s' = String.sub s m (l - m) in
+-    if forall numeric (explode s') then max_num n (num_of_string s')
+    if forall numeric (explode s') then Z.max n (Z.of_string s')
+     else n;;
+ 
+ (* ------------------------------------------------------------------------- *)
+@@ -90,7 +90,7 @@ and defstep op (p,q) (fm,defs,n) =
+ 
+ let defcnf fm =
+   let fm' = nenf(psimplify fm) in
+-  let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm' (Int 0) in
+  let n = Z.succ (overatoms (max_varindex "p_" ** pname) fm' Z.zero) in
+   let (fm'',defs,_) = maincnf (fm',undefined,n) in
+   let deflist = map (snd ** snd) (funset defs) in
+   let subcnfs = itlist ((@) ** simpcnf) deflist (simpcnf fm'') in
+@@ -130,7 +130,7 @@ let rec andcnf (fm,defs,n as trip) =
+ 
+ let defcnfs fm =
+   let fm' = nenf(psimplify fm) in
+-  let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm' (Int 0) in
+  let n = Z.succ (overatoms (max_varindex "p_" ** pname) fm' Z.zero) in
+   let (fm'',defs,_) = andcnf (fm',undefined,n) in
+   let deflist = map (snd ** snd) (funset defs) in
+   setify(itlist ((@) ** simpcnf) deflist (simpcnf fm''));;
+@@ -181,7 +181,7 @@ let rec andcnf pos (fm,defs,n as trip) =
+ 
+ let defcnfs imps fm =
+   let fm' = nenf(psimplify fm) in
+-  let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm' (Int 0) in
+  let n = Z.succ (overatoms (max_varindex "p_" ** pname) fm' Z.zero) in
+   let (fm'',defs,_) = andcnf imps (fm',undefined,n) in
+   let deflist = map (snd ** snd) (funset defs) in
+   setify(itlist ((@) ** simpcnf) deflist (simpcnf fm''));;
+@@ -209,7 +209,7 @@ let rec andcnf3 pos (fm,defs,n as trip)
+ 
+ let defcnf3s imps fm =
+   let fm' = nenf(psimplify fm) in
+-  let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm' (Int 0) in
+  let n = Z.succ (overatoms (max_varindex "p_" ** pname) fm' Z.zero) in
+   let (fm'',defs,_) = andcnf3 imps (fm',undefined,n) in
+   let deflist = map (snd ** snd) (funset defs) in
+   setify(itlist ((@) ** simpcnf) deflist (simpcnf fm''));;
+--- atp/fourier_motzkin.ml.orig	2018-01-23 03:07:35.000000000 -0700
+++ atp/fourier_motzkin.ml	2018-02-11 20:34:13.822886848 -0700
+@@ -71,10 +71,10 @@ let rec posineq fm =
+ let rec adjustcoeff x l fm =
+   match fm with
+     Atom(R(p,[d; Fn("+",[Fn("*",[c;y]);z])])) when y = x ->
+-        let m = l // dest_numeral c in
+-        let n = if p = "<=" then abs_num(m) else m in
+-        let xtm = Fn("*",[mk_numeral(m // n); x]) in
+-        Atom(R(p,[linear_cmul (abs_num m) d;
+        let m = Z.div l (dest_numeral c) in
+        let n = if p = "<=" then Z.abs(m) else m in
+        let xtm = Fn("*",[mk_numeral(Z.div m n); x]) in
+        Atom(R(p,[linear_cmul (Z.abs m) d;
+                 Fn("+",[xtm; linear_cmul n z])]))
+   | Not(p) -> Not(adjustcoeff x l p)
+   | And(p,q) -> And(adjustcoeff x l p,adjustcoeff x l q)
+@@ -88,7 +88,7 @@ let rec adjustcoeff x l fm =
+ let unitycoeff x fm =
+   let l = formlcm x fm in
+   let fm' = adjustcoeff x l fm in
+-  if l =/ Int 1 then fm' else
+  if Z.equal l Z.one then fm' else
+   adjustcoeff x l fm;;
+ 
+ (* ------------------------------------------------------------------------- *)
+@@ -98,10 +98,10 @@ let unitycoeff x fm =
+ let isolate x fm =
+   match fm with
+     Atom(R(p,[_;Fn("+",[Fn("*",[c;y]);z])])) when y = x ->
+-      let c = mk_numeral (Int 0 -/ dest_numeral c) in
+      let c = mk_numeral (Z.sub Z.zero (dest_numeral c)) in
+       Atom(R(p,[Fn("*",[c;y]);z]))
+   | Atom(R(p,[zero;Fn("*",[c;y])])) when y = x ->
+-      let c = mk_numeral (Int 0 -/ dest_numeral c) in
+      let c = mk_numeral (Z.sub Z.zero (dest_numeral c)) in
+       Atom(R(p,[Fn("*",[c;y]);zero]))
+   | _ -> 
+       printer fm;
+@@ -110,7 +110,7 @@ let isolate x fm =
+ let replace vars x t fm =
+   match fm with
+     Atom(R(p,[Fn("*",[c;y]);z])) when y = x ->
+-      let t = if dest_numeral c >/ Int 0 then t else linear_neg t in
+      let t = if Z.gt (dest_numeral c) Z.zero then t else linear_neg t in
+       linform vars (Atom(R(p,[t;z])))
+   | _ -> assert false
+ 
+@@ -128,13 +128,13 @@ let fourier vars fm =
+             (function (Atom(R("=",_))) -> true | _ -> false) cjs in
+           let (Atom(R("=",[s;t]))) = eqn in
+ 	  let (Fn("*",[c;_])) = s in
+-	  let y = if dest_numeral c =/ Int 1 then t else linear_neg t in 
+	  let y = if Z.equal (dest_numeral c) Z.one then t else linear_neg t in 
+           list_conj(map (replace vars x y) (subtract cjs [eqn]))
+       with Failure _ ->
+         let l,r =
+           partition 
+ 	    (fun (Atom(R("<=",[Fn("*",[c;_]);t]))) -> 
+-	      dest_numeral c =/ Int (-1)) cjs 
+	      Z.equal (dest_numeral c) Z.minus_one) cjs 
+ 	in
+         let lefts = map (fun (Atom(R("<=",[_;l]))) -> linear_neg l) l
+         and rights = map (fun (Atom(R("<=",[_;r]))) -> r) r in
+--- atp/lib.ml.orig	2018-01-23 03:07:35.000000000 -0700
+++ atp/lib.ml	2018-02-11 13:26:57.020559495 -0700
+@@ -46,11 +46,9 @@ let ( ** ) = fun f g x -> f(g x);;
+ (* GCD and LCM on arbitrary-precision numbers.                               *)
+ (* ------------------------------------------------------------------------- *)
+ 
+-let gcd_num n1 n2 =
+-  abs_num(num_of_big_int
+-      (Big_int.gcd_big_int (big_int_of_num n1) (big_int_of_num n2)));;
+let gcd_num n1 n2 = Z.gcd n1 n2;;
+ 
+-let lcm_num n1 n2 = abs_num(n1 */ n2) // gcd_num n1 n2;;
+let lcm_num n1 n2 = Z.lcm n1 n2;;
+ 
+ (* ------------------------------------------------------------------------- *)
+ (* A useful idiom for "non contradictory" etc.                               *)
+@@ -73,7 +71,7 @@ let can f x = try f x; true with Failure
+ 
+ let rec (--) = fun m n -> if m > n then [] else m::((m + 1) -- n);;
+ 
+-let rec (---) = fun m n -> if m >/ n then [] else m::((m +/ Int 1) --- n);;
+let rec (---) = fun m n -> if Z.gt m n then [] else m::((Z.succ m) --- n);;
+ 
+ let rec map2 f l1 l2 =
+   match (l1,l2) with
+@@ -596,4 +594,4 @@ let equated (Partition f) = dom f;;
+ (* First number starting at n for which p succeeds.                          *)
+ (* ------------------------------------------------------------------------- *)
+ 
+-let rec first n p = if p(n) then n else first (n +/ Int 1) p;;
+let rec first n p = if p(n) then n else first (Z.succ n) p;;
+--- atp/Makefile.orig	2018-01-23 03:07:35.000000000 -0700
+++ atp/Makefile	2018-02-11 13:14:15.311777144 -0700
+@@ -8,6 +8,8 @@
+ # many.ml        (Example relevant to many-sorted logic)
+ # hol.ml         (Simple higher order logic setup)
+ 
+ZARITHLIB=$(shell ocamlfind query zarith)
+
+ #MLFILES = lib.ml intro.ml formulas.ml prop.ml propexamples.ml           \
+           defcnf.ml dp.ml stal.ml bdd.ml fol.ml skolem.ml               \
+           herbrand.ml unif.ml tableaux.ml resolution.ml prolog.ml       \
+@@ -33,9 +35,9 @@ compiled: example.ml atp.cmx; ocamlopt -
+ 
+ # Make the appropriate object for the main body of code
+ 
+-atp.cmx: atp.ml; ocamlopt -w ax -c atp.ml
+atp.cmx: atp.ml; ocamlopt -I $(ZARITHLIB) -w ax -c atp.ml
+ 
+-atp.cmo: atp.ml; ocamlc -w ax -c atp.ml
+atp.cmo: atp.ml; ocamlc -I $(ZARITHLIB) -w ax -c atp.ml
+ 
+ # Make the camlp4 quotation expander
+ 
+--- atp/make.ml.orig	2018-01-23 03:07:35.000000000 -0700
+++ atp/make.ml	2018-02-11 14:37:48.178019612 -0700
+@@ -44,10 +44,9 @@
+ Gc.set { (Gc.get()) with Gc.stack_limit = 16777216 };; (* Up the stack size  *)
+ Format.set_margin 72;;                                 (* Reduce margins     *)
+ open Format;;                                          (* Open formatting    *)
+-open Num;;                                             (* Open bignums       *)
+ let imperative_assign = (:=);;                         (* Preserve this      *)
+ 
+-let print_num n = print_string(string_of_num n);;      (* Avoid range limit  *)
+let print_num n = print_string(Z.to_string n);;        (* Avoid range limit  *)
+ #install_printer print_num;;                           (* when printing nums *)
+ 
+ (* ------------------------------------------------------------------------- *)
+--- atp/Mk_ml_file.orig	2018-01-23 03:07:35.000000000 -0700
+++ atp/Mk_ml_file	2018-02-10 22:01:01.925304810 -0700
+@@ -1,4 +1,3 @@
+-echo "open Num;;"
+ echo "open Format;;"
+ 
+ cat $@ | sed 's/START_INTERACTIVE;;/(\*/' | sed 's/END_INTERACTIVE;;/\*)/'
+--- jc/jc_annot_inference.ml.orig	2018-02-10 16:03:04.338379961 -0700
+++ jc/jc_annot_inference.ml	2018-02-11 13:13:48.313855743 -0700
+@@ -49,7 +49,6 @@ open Apron
+ open Coeff
+ open Interval
+ open Lincons1
+-open Num
+ 
+ 
+ (*****************************************************************************)
+@@ -1120,7 +1119,7 @@ let linearize t =
+     try match t#node with
+       | JCTconst c ->
+ 	  begin match c with
+-	    | JCCinteger s -> (TermMap.empty, num_of_string s)
+	    | JCCinteger s -> (TermMap.empty, Z.of_string s)
+ 	    | JCCboolean _ | JCCvoid | JCCnull | JCCreal _ | JCCstring _ ->
+ 		err ()
+ 	  end
+@@ -1133,7 +1132,7 @@ let linearize t =
+ 		  (fun vt1 c1 acc ->
+ 		     try
+ 		       let c2 = TermMap.find vt1 coeffs2 in
+-		       TermMap.add vt1 (c1 +/ c2) acc
+		       TermMap.add vt1 (Z.add c1 c2) acc
+ 		     with Not_found -> TermMap.add vt1 c1 acc
+ 		  ) coeffs1 TermMap.empty
+ 		in
+@@ -1143,55 +1142,55 @@ let linearize t =
+ 		     else TermMap.add vt2 c2 acc
+ 		  ) coeffs2 coeffs
+ 		in
+-		(coeffs, cst1 +/ cst2)
+		(coeffs, (Z.add cst1 cst2))
+ 	    | `Bsub ->
+ 		let coeffs = TermMap.fold
+ 		  (fun vt1 c1 acc ->
+ 		     try
+ 		       let c2 = TermMap.find vt1 coeffs2 in
+-		       TermMap.add vt1 (c1 -/ c2) acc
+		       TermMap.add vt1 (Z.sub c1 c2) acc
+ 		     with Not_found -> TermMap.add vt1 c1 acc
+ 		  ) coeffs1 TermMap.empty
+ 		in
+ 		let coeffs = TermMap.fold
+ 		  (fun vt2 c2 acc ->
+ 		     if TermMap.mem vt2 coeffs then acc
+-		     else TermMap.add vt2 (minus_num c2) acc
+		     else TermMap.add vt2 (Z.neg c2) acc
+ 		  ) coeffs2 coeffs
+ 		in
+-		(coeffs, cst1 -/ cst2)
+		(coeffs, (Z.sub cst1 cst2))
+ 	    | `Bmul when TermMap.is_empty coeffs1 || TermMap.is_empty coeffs2 ->
+ 		let coeffs =
+ 		  if TermMap.is_empty coeffs1 then
+-		    TermMap.map (fun c -> c */ cst1) coeffs2
+		    TermMap.map (fun c -> Z.mul c cst1) coeffs2
+ 		  else
+-		    TermMap.map (fun c -> c */ cst2) coeffs1
+		    TermMap.map (fun c -> Z.mul c cst2) coeffs1
+ 		in
+-		(coeffs, cst1 */ cst2)
+		(coeffs, (Z.mul cst1 cst2))
+ 	    | `Bmul
+ 	    | `Bdiv
+ 	    | `Bmod -> err ()
+ 	  end
+       | JCTbinary(t1,(#bitwise_op as bop,`Integer),t2) ->
+ 	  let coeffs1, cst1 = aux t1 in
+-	  if coeffs1 = TermMap.empty && cst1 =/ Int 0 then
+	  if coeffs1 = TermMap.empty && Z.equal cst1 Z.zero then
+ 	    match bop with
+ 	      | `Bbw_and
+ 	      | `Bshift_left
+ 	      | `Blogical_shift_right
+-	      | `Barith_shift_right -> TermMap.empty, Int 0
+	      | `Barith_shift_right -> TermMap.empty, Z.zero
+ 	      | `Bbw_or
+ 	      | `Bbw_xor -> aux t2
+ 	      | _ -> err ()
+ 	  else
+ 	    (* Consider non-linear term as abstract variable. *)
+-	    (TermMap.add t (Int 1) TermMap.empty, Int 0)
+	    (TermMap.add t Z.one TermMap.empty, Z.zero)
+       | JCTunary((uop,`Integer),t1) ->
+ 	  let coeffs1,cst1 = aux t1 in
+ 	  begin match uop with
+ 	    | `Uminus ->
+-		let coeffs = TermMap.map (fun c -> minus_num c) coeffs1 in
+-		(coeffs, minus_num cst1)
+		let coeffs = TermMap.map (fun c -> Z.neg c) coeffs1 in
+		(coeffs, Z.neg cst1)
+ 	    | _ -> err ()
+ 	  end
+       | JCTvar _ | JCTderef _ | JCToffset _ | JCTapp _ | JCTbinary _
+@@ -1201,13 +1200,16 @@ let linearize t =
+       | JCTrange _ | JCTif _ | JCTlet _ ->
+ 	  err ()
+     with Failure "linearize" ->
+-      (TermMap.add t (Int 1) TermMap.empty, Int 0)
+      (TermMap.add t Z.one TermMap.empty, Z.zero)
+   in aux t
+ 
+ let linstr_of_term env t =
+(*
+   let mkmulstr = function
+-    | (_va, Int 0) -> ""
+-    | (va, c) -> string_of_num c ^ " * " ^ va
+    | (_va, Z.zero) -> ""
+    | (va, c) -> (Z.to_string c) ^ " * " ^ va
+*)
+  let mkmulstr = (fun (va,c) -> if Z.equal Z.zero c then "" else (Z.to_string c) ^ " * " ^ va)
+   in
+   let rec mkaddstr = function
+     | [] -> ""
+@@ -1286,33 +1288,33 @@ let rec linstr_of_assertion env a =
+ 	in
+ 	let env,str,cst = linstr_of_term env subt in
+ 	if str = "" then
+-	  let ncst = minus_num cst in
+	  let ncst = Z.neg cst in
+ 	  let is_true = match bop with
+-	    | `Blt -> Int 0 </ ncst
+-	    | `Bgt -> Int 0 >/ ncst
+-	    | `Ble -> Int 0 <=/ ncst
+-	    | `Bge -> Int 0 >=/ ncst
+-	    | `Beq -> Int 0 =/ ncst
+-	    | `Bneq -> Int 0 <>/ ncst
+	    | `Blt -> Z.lt Z.zero ncst
+	    | `Bgt -> Z.gt Z.zero ncst
+	    | `Ble -> Z.leq Z.zero ncst
+	    | `Bge -> Z.geq Z.zero ncst
+	    | `Beq -> Z.equal Z.zero ncst
+	    | `Bneq -> not (Z.equal Z.zero ncst)
+ 	  in
+ 	  env, if is_true then Dnf.true_ else Dnf.false_
+ 	else
+-	  let cstr = string_of_num (minus_num cst) in
+	  let cstr = Z.to_string (Z.neg cst) in
+ 	  (* Do not use < and > with APRON, due to bugs in some versions.
+ 	     Convert to equivalent non-strict. *)
+ 	  let str = match bop with
+ 	    | `Blt -> [[str ^ " <= " ^
+-			  (string_of_num (pred_num (minus_num cst)))]]
+			  (Z.to_string (Z.pred (Z.neg cst)))]]
+ 	    | `Bgt -> [[str ^ " >= " ^
+-			  (string_of_num (succ_num (minus_num cst)))]]
+			  (Z.to_string (Z.succ (Z.neg cst)))]]
+ 	    | `Ble -> [[str ^ " <= " ^ cstr]]
+ 	    | `Bge -> [[str ^ " >= " ^ cstr]]
+ 	    | `Beq -> [[str ^ " = " ^ cstr]]
+ 	    | `Bneq ->
+ 		[[str ^ " <= " ^
+-		    (string_of_num (pred_num (minus_num cst)))];
+		    (Z.to_string (Z.pred (Z.neg cst)))];
+ 		 [str ^ " >= " ^
+-		    (string_of_num (succ_num (minus_num cst)))]]
+		    (Z.to_string (Z.succ (Z.neg cst)))]]
+ 	  in
+ 	  env, str
+     | JCAnot a ->
+@@ -1330,8 +1332,8 @@ let rec linstr_of_assertion env a =
+ let linstr_of_expr env e =
+   match Jc_effect.term_of_expr e with None -> None | Some t ->
+     let env,str,cst = linstr_of_term env t in
+-    if str = "" then Some (env, string_of_num cst)
+-    else Some (env, str ^ " + " ^ (string_of_num cst))
+    if str = "" then Some (env, Z.to_string cst)
+    else Some (env, str ^ " + " ^ (Z.to_string cst))
+ 
+ let offset_linstr_of_expr env ok e =
+   match e#node with
+@@ -1340,15 +1342,15 @@ let offset_linstr_of_expr env ok e =
+ 	else
+ 	  begin match Jc_effect.term_of_expr e with None -> None | Some t ->
+ 	    let env,str,cst = linstr_of_term env t in
+-	    if str = "" then Some (env,string_of_num cst)
+-	    else Some (env,str ^ " + " ^ (string_of_num cst))
+	    if str = "" then Some (env,Z.to_string cst)
+	    else Some (env,str ^ " + " ^ (Z.to_string cst))
+ 	  end
+     | _ ->
+ 	if is_nonnull_pointer_type e#typ then
+ 	  match Jc_effect.term_of_expr e with None -> None | Some t ->
+ 	    let env,str,cst = offset_linstr_of_term env ok t in
+-	    if str = "" then Some (env,string_of_num cst)
+-	    else Some (env,str ^ " + " ^ (string_of_num cst))
+	    if str = "" then Some (env,Z.to_string cst)
+	    else Some (env,str ^ " + " ^ (Z.to_string cst))
+ 	else None
+ 
+ 
+@@ -1419,13 +1421,13 @@ let mkassertion lincons =
+ 
+ let rec linterms_of_term t =
+   let mkmulterm (t,c) =
+-    if c =/ Int 0 then None
+-    else if c =/ Int 1 then Some t
+-    else if c =/ Int (-1) then
+    if Z.equal c Z.zero then None
+    else if Z.equal c Z.one then Some t
+    else if Z.equal c Z.minus_one then
+       Some(new term ~typ:integer_type (JCTunary((`Uminus,`Integer),t)))
+     else
+       let c =
+-	new term ~typ:integer_type (JCTconst(JCCinteger(string_of_num c)))
+	new term ~typ:integer_type (JCTconst(JCCinteger(Z.to_string c)))
+       in
+       Some(new term ~typ:integer_type (JCTbinary(c,(`Bmul,`Integer),t)))
+   in
+@@ -1443,30 +1445,30 @@ let rec linterms_of_term t =
+   let coeffs,cst = linearize t in
+   let posl,negl =
+     TermMap.fold (fun t c (pl,nl) ->
+-		    if c >/ Int 0 then (t,c) :: pl, nl
+-		    else if c </ Int 0 then pl, (t,minus_num c) :: nl
+		    if Z.gt c Z.zero then (t,c) :: pl, nl
+		    else if Z.lt c Z.zero then pl, (t,Z.neg c) :: nl
+ 		    else pl, nl
+ 		 ) coeffs ([],[])
+   in
+   let cstt =
+     new term ~typ:integer_type
+-      (JCTconst(JCCinteger(string_of_num(abs_num cst))))
+      (JCTconst(JCCinteger(Z.to_string(Z.abs cst))))
+   in
+   let post = match mkaddterm posl with
+     | None ->
+-	if cst >/ Int 0 then cstt
+	if Z.gt cst Z.zero then cstt
+ 	else new term ~typ:integer_type (JCTconst(JCCinteger "0"))
+     | Some t ->
+-	if cst >/ Int 0 then
+	if Z.gt cst Z.zero then
+ 	  new term ~typ:integer_type (JCTbinary(t,(`Badd,`Integer),cstt))
+ 	else t
+   in
+   let negt = match mkaddterm negl with
+     | None ->
+-	if cst </ Int 0 then cstt
+	if Z.lt cst Z.zero then cstt
+ 	else new term ~typ:integer_type (JCTconst(JCCinteger "0"))
+     | Some t ->
+-	if cst </ Int 0 then
+	if Z.lt cst Z.zero then
+ 	  new term ~typ:integer_type (JCTbinary(t,(`Badd,`Integer),cstt))
+ 	else t
+   in
+@@ -1518,8 +1520,8 @@ let mkconsistent a =
+ 	  let posl,negl =
+ 	    TermMap.fold
+ 	      (fun t c (pl,nl) ->
+-		 if c >/ Int 0 then t :: pl, nl
+-		 else if c </ Int 0 then pl, t :: nl
+		 if Z.gt c Z.zero then t :: pl, nl
+		 else if Z.lt c Z.zero then pl, t :: nl
+ 		 else pl, nl
+ 	      ) coeffs ([],[])
+ 	  in
+@@ -2497,10 +2499,10 @@ let collect_expr_targets e =
+   let collect_integer_overflow ei e1 =
+     match Jc_effect.term_of_expr e1 with None -> [] | Some t1 ->
+       let mint = new term ~typ:integer_type
+-	(JCTconst (JCCinteger (Num.string_of_num ei.jc_enum_info_min)))
+	(JCTconst (JCCinteger (Z.to_string ei.jc_enum_info_min)))
+       in
+       let maxt = new term ~typ:integer_type
+-	(JCTconst(JCCinteger (Num.string_of_num ei.jc_enum_info_max)))
+	(JCTconst(JCCinteger (Z.to_string ei.jc_enum_info_max)))
+       in
+       let mina = new assertion (JCArelation (mint, (`Ble,`Integer), t1)) in
+       let maxa = new assertion (JCArelation (t1, (`Ble,`Integer), maxt)) in
--- a/why-ocaml-4.06.patch
+++ b/why-ocaml-4.06.patch
@ -0,0 +1,11 @@
+--- Makefile.in.orig	2018-02-10 15:44:26.226883183 -0700
+++ Makefile.in	2018-02-12 19:34:20.930490137 -0700
+@@ -214,7 +214,7 @@ jc/jc.cmx jc/jc.o: $(JCCMX_EXPORT)
+ # ppc: jc/jc.cmi jc/jc.cmo jc/jc.cmx
+ 
+ bin/jessie.opt: $(JCCMX)
+-	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLOPT) $(OFLAGS) $(APRONLIB) $(APRONLIBS) $(ATPLIB) -o $@ \
+	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLOPT) -runtime-variant _pic $(OFLAGS) $(APRONLIB) $(APRONLIBS) $(ATPLIB) -o $@ \
+ 		unix.cmxa str.cmxa zarith.cmxa graph.cmxa $^
+ 	$(STRIP)    $@
+ 
--- a/why-project.patch
+++ b/why-project.patch
@ -0,0 +1,115 @@
+--- Makefile.in.orig	2018-01-23 03:07:35.000000000 -0700
+++ Makefile.in	2018-02-10 15:44:26.226883183 -0700
+@@ -155,7 +155,7 @@ CMO_EXPORT =  src/lib.cmo src/rc.cmo src
+ 	   src/effect.cmo src/pp.cmo src/option_misc.cmo \
+ 	   src/report.cmo \
+            src/explain.cmo 	\
+-	   src/xml.cmo src/project.cmo
+	   src/xml.cmo src/whyproject.cmo
+ 
+ # jessie
+ JCCML_EXPORT = src/why3_kw.ml jc/output.ml \
+--- src/options.mli.orig	2018-01-23 03:07:35.000000000 -0700
+++ src/options.mli	2018-02-10 15:44:26.258883112 -0700
+@@ -184,7 +184,7 @@ val files : string list
+ (*s GUI? *)
+ 
+ val gui : bool ref
+-val gui_project : Project.t option ref
+val gui_project : Whyproject.t option ref
+ val lib_files_to_load : string list
+ 
+ (*
+--- src/pretty.ml.orig	2018-01-23 03:07:35.000000000 -0700
+++ src/pretty.ml	2018-02-10 15:44:26.259883110 -0700
+@@ -416,12 +416,12 @@ let output_project f =
+        with Not_found ->
+ 	 functions := SMap.add fn SMap.empty !functions)
+     Util.program_locs ;
+-  let p = Project.create (Filename.basename f) in
+-  Project.set_project_context_file p (f ^ "_ctx.why");
+  let p = Whyproject.create (Filename.basename f) in
+  Whyproject.set_project_context_file p (f ^ "_ctx.why");
+   List.iter
+     (fun (expl,fpo) ->
+        let n = expl.lemma_or_fun_name in
+-       let _ = Project.add_lemma p n expl fpo in ())
+       let _ = Whyproject.add_lemma p n expl fpo in ())
+     !lemmas;
+   SMap.iter
+     (fun fname behs ->
+@@ -431,15 +431,15 @@ let output_project f =
+ 	   floc
+ 	 with Not_found -> Loc.dummy_floc
+        in
+-       let f = Project.add_function p fname floc in
+       let f = Whyproject.add_function p fname floc in
+        SMap.iter
+ 	 (fun beh vcs ->
+-	    let be = Project.add_behavior f beh floc in
+	    let be = Whyproject.add_behavior f beh floc in
+ 	    List.iter
+ 	      (fun (expl,fpo) ->
+-		 let _ = Project.add_goal be expl fpo in ())
+		 let _ = Whyproject.add_goal be expl fpo in ())
+ 	      vcs)
+ 	 behs)
+     !functions;
+-  Project.save p f;
+  Whyproject.save p f;
+   p
+--- src/pretty.mli.orig	2018-01-23 03:07:35.000000000 -0700
+++ src/pretty.mli	2018-02-10 15:44:26.259883110 -0700
+@@ -50,4 +50,4 @@ val output_files : string -> unit
+ (* [output_project f] produces a whole project description, in a file
+ [f.wpr], together with other needed files [f_ctx.why], [f_lemmas.why],
+ and each goal in a separate file [f_po<i>.why] for i=1,2,... *)
+-val output_project : string -> Project.t
+val output_project : string -> Whyproject.t
+--- src/whyweb.ml.orig	2018-01-23 03:07:35.000000000 -0700
+++ src/whyweb.ml	2018-02-10 15:44:26.259883110 -0700
+@@ -29,7 +29,7 @@
+ (**************************************************************************)
+ 
+ open Format
+-open Project
+open Whyproject
+ 
+ (*prover*)
+ let provers = [Ergo ; Simplify ; Z3 ; Yices ; Cvc3]
+@@ -168,7 +168,7 @@ let file = match !file with
+   | None -> ()
+   | Some f -> Arg.usage spec usage; exit 1
+ 
+-let proj = ref (Project.create "")
+let proj = ref (Whyproject.create "")
+ 
+ let proj_file = ref ""
+ 
+@@ -260,7 +260,7 @@ let interp_com c =
+ 	  let _ =  Thread.create (launch_behavior Cvc3)  b in ()
+       | `LaunchCvc3Function f -> 
+ 	  let _ =  Thread.create (launch_function Cvc3) f  in ()
+-      | `Save -> Project.save !proj !proj.project_name
+      | `Save -> Whyproject.save !proj !proj.project_name
+     end;
+     loc
+   with Not_found -> ("",0,0,0)
+@@ -343,7 +343,7 @@ let main_page msg =
+ let load_prj file =
+   eprintf "Reading file %s@." file;
+   try
+-    proj := Project.load file;
+    proj := Whyproject.load file;
+     proj_file := file;
+   with
+       Sys_error _ -> 
+@@ -526,7 +526,7 @@ wprint "<center><a href=\"%s\">Save Proj
+ <table border=\"1\"  cellpadding=\"0\" cellspacing=\"0\">" ns;
+ 	 wprint "<tr><th></th>";
+ 	 List.iter (fun prover -> 
+-		      wprint "<th>%s</th>" (Project.provers_name prover)) 
+		      wprint "<th>%s</th>" (Whyproject.provers_name prover)) 
+ 	   provers;
+ 	 wprint "</tr>
+ ";
--- a/why-safe-string.patch
+++ b/why-safe-string.patch
@ -0,0 +1,19 @@
+--- jc/jc_annot_inference.ml.orig	2018-01-23 03:07:35.000000000 -0700
+++ jc/jc_annot_inference.ml	2018-02-10 16:03:04.338379961 -0700
+@@ -212,14 +212,14 @@ let name_of_term t =
+   Format.fprintf str_formatter "%a" Jc_output.term t;
+   let s = Format.flush_str_formatter () in
+   let s = filter_alphanumeric s in
+-  "T" ^ unique_term_name t s
+  "T" ^ unique_term_name t (Bytes.to_string s)
+ 
+ let name_of_assertion a =
+   ignore (Format.flush_str_formatter ());
+   Format.fprintf str_formatter "%a" Jc_output.assertion a;
+   let s = Format.flush_str_formatter () in
+   let s = filter_alphanumeric s in
+-  "A" ^ unique_assertion_name a s
+  "A" ^ unique_assertion_name a (Bytes.to_string s)
+ 
+ (* support of <new> (Nicolas) *)
+ let rec destruct_alloc t =
--- a/why.spec
+++ b/why.spec
@ -0,0 +1,605 @@
+# Whether PVS is available
+%ifarch %{ix86} x86_64 ppc sparcv9
+%global has_pvs 1
+%else
+%global has_pvs 0
+%endif
+
+Name:           why
+Version:        2.40
+Release:        2%{?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
+# Avoid a clash between Frama-C and why modules both named "Project".
+# Sent upstream 26 Jun 2014.
+Patch0:         %{name}-project.patch
+# Adapt to the safe string feature of ocaml 4.06
+Patch1:         %{name}-safe-string.patch
+# Adapt to ocaml 4.06 in general
+Patch2:         %{name}-ocaml-4.06.patch
+# Finish an incomplete Num to zarith conversion
+Patch3:         %{name}-num.patch
+
+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-camlp5-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
+
+# 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 yices 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
+%patch0
+%patch1
+%patch2
+%patch3
+
+# The other part of avoiding the "Project" module name clash
+mv src/project.ml src/whyproject.ml
+mv src/project.mli src/whyproject.mli
+
+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
+
+%build
+%ifarch %{ocaml_native_compiler}
+%global opt_option OCAMLBEST=opt
+%else
+%global opt_option OCAMLBEST=byte OCAMLDEP=ocamldep OCAMLYACC=ocamlyacc OCAMLLEX=ocamllex
+%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
+
+%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
+* Sat Jul 14 2018 Fedora Release Engineering <releng@fedoraproject.org> - 2.40-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild
+
+* Mon Feb 12 2018 Jerry James <loganjerry@gmail.com> - 2.40-1
+- New upstream release
+- Add -num patch to fix incomplete num to zarith conversion
+
+* Fri Feb 09 2018 Fedora Release Engineering <releng@fedoraproject.org> - 2.39-5
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild
+
+* Thu Jan 18 2018 Igor Gnatenko <ignatenkobrain@fedoraproject.org> - 2.39-4
+- Remove obsolete scriptlets
+
+* Sat Dec  9 2017 Jerry James <loganjerry@gmail.com> - 2.39-3
+- Bring back the -project patch, still needed (bz 1520483)
+- Add the -safe-string patch for building with ocaml 4.06.0
+- Build the Jessie plugin with -runtime-variant _pic
+
+* Sat Dec 02 2017 Richard W.M. Jones <rjones@redhat.com> - 2.39-3
+- OCaml 4.06.0 rebuild.
+
+* Sat Oct  7 2017 Jerry James <loganjerry@gmail.com> - 2.39-2
+- Rebuild for why3 0.88.0
+
+* Thu Sep  7 2017 Jerry James <loganjerry@gmail.com> - 2.39-1
+- New upstream release
+
+* Wed Sep 06 2017 Richard W.M. Jones <rjones@redhat.com> - 2.38-6
+- OCaml 4.05.0 rebuild.
+
+* Thu Aug 03 2017 Fedora Release Engineering <releng@fedoraproject.org> - 2.38-5
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Binutils_Mass_Rebuild
+
+* Thu Jul 27 2017 Fedora Release Engineering <releng@fedoraproject.org> - 2.38-4
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild
+
+* Sat Jul 01 2017 Richard W.M. Jones <rjones@redhat.com> - 2.38-3
+- Rebuild for OCaml 4.04.2.
+
+* Mon May 15 2017 Richard W.M. Jones <rjones@redhat.com> - 2.38-2
+- Rebuild for OCaml 4.04.1.
+
+* Fri Mar 24 2017 Jerry James <loganjerry@gmail.com> - 2.38-1
+- New upstream release
+
+* Sat Feb 11 2017 Fedora Release Engineering <releng@fedoraproject.org> - 2.36-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild
+
+* Thu Jan 12 2017 Jerry James <loganjerry@gmail.com> - 2.36-1
+- New upstream release
+
+* Wed Nov 30 2016 Jerry James <loganjerry@gmail.com> - 2.35-23
+- Rebuild for gappalib-coq 1.3.2
+
+* Sun Nov 06 2016 Richard W.M. Jones <rjones@redhat.com> - 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 <loganjerry@gmail.com> - 2.35-20
+- Rebuild for coq 8.5pl3
+- Remove obsolete scriptlets
+
+* Thu Sep 29 2016 Jerry James <loganjerry@gmail.com> - 2.35-19
+- Rebuild for flocq 2.5.2 and gappalib-coq 1.3.1
+
+* Fri Sep  2 2016 Jerry James <loganjerry@gmail.com> - 2.35-18
+- Rebuild for why3 0.87.2
+
+* Fri Jul 22 2016 Jerry James <loganjerry@gmail.com> - 2.35-17
+- Rebuild for apron 0.9.11 and gappalib-coq 1.3.0
+
+* Wed Jul 13 2016 Jerry James <loganjerry@gmail.com> - 2.35-16
+- Rebuild for coq 8.5pl2
+
+* Wed Jun  1 2016 Jerry James <loganjerry@gmail.com> - 2.35-15
+- Rebuild for why3 0.87.1 and Frama-C Aluminium
+
+* Fri Apr 22 2016 Jerry James <loganjerry@gmail.com> - 2.35-14
+- Rebuild for coq 8.5pl1
+
+* Sat Apr 16 2016 Jerry James <loganjerry@gmail.com> - 2.35-13
+- Rebuild for ocaml-ocamlgraph 1.8.7
+
+* Fri Mar 18 2016 Jerry James <loganjerry@gmail.com> - 2.35-12
+- Rebuild for why3 0.87.0
+
+* Fri Feb 12 2016 Jerry James <loganjerry@gmail.com> - 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 <releng@fedoraproject.org> - 2.35-10
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild
+
+* Wed Oct 14 2015 Jerry James <loganjerry@gmail.com> - 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 <rjones@redhat.com> - 2.35-8
+- OCaml 4.02.3 rebuild.
+
+* Mon Jun 22 2015 Jerry James <loganjerry@gmail.com> - 2.35-7
+- Rebuild for why3 0.86.1
+
+* Fri Jun 19 2015 Richard W.M. Jones <rjones@redhat.com> - 2.35-6
+- Rebuild for ocaml-4.02.2.
+
+* Fri Jun 19 2015 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.35-5
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_23_Mass_Rebuild
+
+* Sat May 16 2015 Jerry James <loganjerry@gmail.com> - 2.35-4
+- Rebuild for why3 0.86
+
+* Mon Apr 13 2015 Jerry James <loganjerry@gmail.com> - 2.35-3
+- Rebuild for coq 8.4pl6
+
+* Wed Apr  1 2015 Jerry James <loganjerry@gmail.com> - 2.35-2
+- Adjust requires filter
+
+* Tue Mar 31 2015 Jerry James <loganjerry@gmail.com> - 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 <loganjerry@gmail.com> - 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 <rjones@redhat.com> - 2.34-17
+- ocaml-4.02.1 rebuild.
+
+* Sat Nov 15 2014 Jerry James <loganjerry@gmail.com> - 2.34-16
+- Fix gwhy-2.33.patch (bz 1164470)
+
+* Thu Nov 13 2014 Richard W.M. Jones <rjones@redhat.com> - 2.34-15
+- Bump and rebuild for broken dependencies.
+
+* Thu Oct 30 2014 Jerry James <loganjerry@gmail.com> - 2.34-14
+- Rebuild for coq 8.4pl5
+
+* Thu Sep 18 2014 Jerry James <loganjerry@gmail.com> - 2.34-13
+- Rebuild for why3 0.85
+
+* Mon Sep  8 2014 Jerry James <loganjerry@gmail.com> - 2.34-12
+- Rebuild for fixed frama-c
+- Fix license handling
+
+* Tue Sep  2 2014 Jerry James <loganjerry@gmail.com> - 2.34-11
+- Rebuild for the final ocaml 4.02.0 release
+
+* Mon Aug 25 2014 Jerry James <loganjerry@gmail.com> - 2.34-10
+- ocaml-4.02.0+rc1 rebuild.
+
+* Mon Aug 18 2014 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.34-9
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild
+
+* Mon Aug  4 2014 Jerry James <loganjerry@gmail.com> - 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 <loganjerry@gmail.com> - 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 <rel-eng@lists.fedoraproject.org> - 2.34-6
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild
+
+* Tue May 13 2014 Jerry James <loganjerry@gmail.com> - 2.34-5
+- Rebuild for coq 8.4pl4
+
+* Mon Apr 21 2014 Jerry James <loganjerry@gmail.com> - 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 <rjones@redhat.com> - 2.34-3
+- Remove ocaml_arches macro (RHBZ#1087794).
+
+* Mon Mar 24 2014 Jerry James <loganjerry@gmail.com> - 2.34-2
+- Remove dropped patches
+- Add icons
+- Fix the desktop icon entries
+
+* Tue Mar 18 2014 Jerry James <loganjerry@gmail.com> - 2.34-1
+- New upstream release
+- Drop upstreamed -hashtbl, -flocq, and -or patches
+- Add ocaml-findlib BR
+
+* Wed Feb 26 2014 Jerry James <loganjerry@gmail.com> - 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 <loganjerry@gmail.com> - 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ä <ville.skytta@iki.fi> - 2.33-4
+- Install docs to %%{_pkgdocdir} where available.
+
+* Fri Jun 21 2013 Jerry James <loganjerry@gmail.com> - 2.33-3
+- Rebuild for frama-c Fluorine 20130601
+
+* Thu May 23 2013 Jerry James <loganjerry@gmail.com> - 2.33-2
+- Rebuild for new frama-c and why3 builds
+
+* Tue May 14 2013 Jerry James <loganjerry@gmail.com> - 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 <paragn AT fedoraproject DOT org> - 2.31-7
+- Remove vendor tag from desktop file as per https://fedorahosted.org/fesco/ticket/1077
+
+* Mon Jan 14 2013 Jerry James <loganjerry@gmail.com> - 2.31-6
+- Rebuild for alt-ergo 0.95
+
+* Mon Jan  7 2013 Jerry James <loganjerry@gmail.com> - 2.31-5
+- Rebuild for coq 8.4pl1
+
+* Fri Oct 19 2012 Jerry James <loganjerry@gmail.com> - 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 <loganjerry@gmail.com> - 2.31-3
+- Rebuild for new frama-c build with altered API.
+
+* Mon Aug 27 2012 Jerry James <loganjerry@gmail.com> - 2.31-2
+- Frama-c is fixed; rebuild with the Jessie plugin enabled and functioning
+
+* Thu Aug 23 2012 Jerry James <loganjerry@gmail.com> - 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 <rjones@redhat.com> - 2.30-7
+- Rebuild for OCaml 4.00.0 official.
+
+* Sun Jul 22 2012 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.30-6
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild
+
+* 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.
				`@ -1 +0,0 @@`
				`Abandoned by upstream and fails to build from source`