diff --git a/why-flocq23.patch b/why-flocq23.patch
new file mode 100644
index 0000000..b54d85a
--- /dev/null
+++ b/why-flocq23.patch
@@ -0,0 +1,11 @@
+--- lib/coq/WhyFloats.v.orig 2014-03-17 16:01:46.000000000 -0600
++++ lib/coq/WhyFloats.v 2014-04-21 15:39:55.680771647 -0600
+@@ -108,7 +108,7 @@
+ generalize (Zeq_bool_eq _ _ H1). clear.
+ rewrite Fcalc_digits.Z_of_nat_S_digits2_Pnat.
+ intros H.
+-apply (Fcalc_digits.Zpower_gt_Zdigits Fcalc_digits.radix2 (Zpos prec) (Zpos m)).
++apply (Fcore_digits.Zpower_gt_Zdigits Fcalc_digits.radix2 (Zpos prec) (Zpos m)).
+ revert H.
+ unfold FLT_exp.
+ generalize (Fcore_digits.Zdigits radix2 (Zpos m)).
diff --git a/why-project.patch b/why-project.patch
new file mode 100644
index 0000000..a280c81
--- /dev/null
+++ b/why-project.patch
@@ -0,0 +1,124 @@
+--- ./Makefile.in.orig 2014-03-17 16:01:46.000000000 -0600
++++ ./Makefile.in 2014-06-26 12:30:00.000000000 -0600
+@@ -222,7 +222,7 @@ CMO_EXPORT = src/lib.cmo src/rc.cmo src
+ src/effect.cmo src/pp.cmo src/option_misc.cmo \
+ src/parser.cmo src/lexer.cmo src/report.cmo \
+ src/explain.cmo \
+- src/xml.cmo src/project.cmo
++ src/xml.cmo src/whyproject.cmo
+
+ CMO = src/lib.cmo src/rc.cmo tools/dpConfig.cmo \
+ src/version.cmo src/options.cmo src/linenum.cmo src/loc.cmo \
+@@ -239,7 +239,7 @@ CMO = src/lib.cmo src/rc.cmo tools/dpCon
+ src/holl.cmo src/harvey.cmo src/simplify.cmo \
+ src/regen.cmo src/mizar.cmo src/smtlib.cmo src/coq.cmo \
+ src/zenon.cmo src/z3.cmo src/cvcl.cmo tools/calldp.cmo \
+- src/xml.cmo src/project.cmo \
++ src/xml.cmo src/whyproject.cmo \
+ src/why3_kw.cmo src/why3.cmo src/pretty.cmo \
+ src/unionfind.cmo src/theoryreducer.cmo \
+ src/theory_filtering.cmo src/hypotheses_filtering.cmo \
+--- ./src/options.mli.orig 2014-03-17 16:01:46.000000000 -0600
++++ ./src/options.mli 2014-06-26 12:30:00.000000000 -0600
+@@ -185,7 +185,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 2014-03-17 16:01:46.000000000 -0600
++++ ./src/pretty.ml 2014-06-26 12:30:00.000000000 -0600
+@@ -415,12 +415,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 ->
+@@ -430,15 +430,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 2014-03-17 16:01:46.000000000 -0600
++++ ./src/pretty.mli 2014-06-26 12:30:00.000000000 -0600
+@@ -51,4 +51,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.why] for i=1,2,... *)
+-val output_project : string -> Project.t
++val output_project : string -> Whyproject.t
+--- ./src/whyweb.ml.orig 2014-03-17 16:01:46.000000000 -0600
++++ ./src/whyweb.ml 2014-06-26 12:30:00.000000000 -0600
+@@ -30,7 +30,7 @@
+ (**************************************************************************)
+
+ open Format
+-open Project
++open Whyproject
+
+ (*prover*)
+ let provers = [Ergo ; Simplify ; Z3 ; Yices ; Cvc3]
+@@ -169,7 +169,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 ""
+
+@@ -261,7 +261,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 -> Whyroject.save !proj !proj.project_name
+ end;
+ loc
+ with Not_found -> ("",0,0,0)
+@@ -344,7 +344,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 _ ->
+@@ -527,7 +527,7 @@ wprint "Save Proj
+ " ns;
+ wprint " | ";
+ List.iter (fun prover ->
+- wprint "%s | " (Project.provers_name prover))
++ wprint "%s | " (Whyproject.provers_name prover))
+ provers;
+ wprint "
|---|
+ ";
diff --git a/why.spec b/why.spec
index e0d4822..802f203 100644
--- a/why.spec
+++ b/why.spec
@@ -17,7 +17,7 @@
Name: why
Version: 2.34
-Release: 2%{?dist}
+Release: 5%{?dist}
Summary: Software verification platform
Group: Applications/Engineering
@@ -55,6 +55,13 @@ Patch0: gwhy-2.33.patch
# this case.
Patch1: %{name}-2.34-Makefile.in.patch
+# Adapt to flocq 2.3.0
+Patch2: %{name}-flocq23.patch
+
+# Avoid a clash between Frama-C and why modules both named "Project".
+# Sent upstream 26 Jun 2014.
+Patch3: %{name}-project.patch
+
BuildRequires: auto-destdir
BuildRequires: cvc3
BuildRequires: desktop-file-utils
@@ -217,12 +224,18 @@ based on Why, including various automated and interactive provers.
%setup -q -T -D -a 15
%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 %SOURCE1 %SOURCE2 %SOURCE6 %SOURCE7 ./
-# Harden the build for network-using binaries
-sed -e '\%^bin/jessie\.opt%,\%^bin/jessie\.byte%s/-o/-ccopt -Wl,-z,relro,-z,now &/' \
- -e '/gtkThread\.cmx/s/-o/-ccopt -Wl,-z,relro,-z,now &/' \
+# Link with Fedora LDFLAGS
+sed -e "\%^bin/jessie\.opt%,\%^bin/jessie\.byte%s/-o/-ccopt $RPM_LD_FLAGS &/" \
+ -e "/gtkThread\.cmx/s/-o/-ccopt $RPM_LD_FLAGS &/" \
-i Makefile.in
%define fix_encoding() \
@@ -447,6 +460,17 @@ gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || :
%changelog
+* Tue Jun 24 2014 Jerry James - 2.34-5
+- Omit "-z now" when building with relro (bz 1105265)
+- Resolve a conflict between Frama-C and why modules both named "Project"
+
+* Tue May 13 2014 Jerry James - 2.34-4
+- Rebuild for coq 8.4pl4
+
+* Mon Apr 21 2014 Jerry James - 2.34-3
+- Rebuild for ocamlgraph 1.8.5 and flocq 2.3.0
+- Add -flocq23 patch to adapt to flocq 2.3.0
+
* Mon Mar 24 2014 Jerry James - 2.34-2
- Remove dropped patches
- Add icons