Bring back the -project patch, still needed (bz 1520483).

Because 2.38 did not know about OCaml 4.05.

why-project.patch

@@ -0,0 +1,115 @@
+--- Makefile.in.orig	2017-08-23 02:08:38.000000000 -0600
++++ Makefile.in	2017-12-04 21:00:24.549232019 -0700
+@@ -154,7 +154,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	2017-08-23 02:08:38.000000000 -0600
++++ src/options.mli	2017-12-04 21:01:17.268996320 -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	2017-08-23 02:08:38.000000000 -0600
++++ src/pretty.ml	2017-12-04 21:02:42.540615229 -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	2017-08-23 02:08:38.000000000 -0600
++++ src/pretty.mli	2017-12-04 21:03:05.635512035 -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	2017-08-23 02:08:38.000000000 -0600
++++ src/whyweb.ml	2017-12-04 21:04:16.932193463 -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>
+ ";

why.spec

@@ -10,7 +10,7 @@
 
 Name:           why
 Version:        2.39
-Release:        2%{?dist}
+Release:        3%{?dist}
 Summary:        Software verification platform
 
 License:        LGPLv2 with exceptions
@@ -26,6 +26,9 @@ 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
 
 BuildRequires:  auto-destdir
 BuildRequires:  desktop-file-utils
@@ -115,6 +118,11 @@ based on Why, including various automated and interactive provers.
 %prep
 %setup -q
 %setup -q -T -D -a 9
+%patch0
+
+# 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 ./
 
@@ -244,12 +252,18 @@ gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || :
 
 
 %changelog
+* Sat Dec  9 2017 Jerry James <loganjerry@gmail.com> - 2.39-3
+- Bring back the -project patch, still needed (bz 1520483)
+
 * 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.39-1
+- Update to 2.39.
+
 * Wed Sep 06 2017 Richard W.M. Jones <rjones@redhat.com> - 2.38-6
 - OCaml 4.05.0 rebuild.