From 96ed6c8a3d7e28f8063ec4c431e88796745ce8ba Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Wed, 6 Sep 2017 19:58:25 +0100 Subject: [PATCH 1/2] Update to 2.39. Because 2.38 did not know about OCaml 4.05. --- .gitignore | 1 + sources | 2 +- why.spec | 7 ++++--- 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/.gitignore b/.gitignore index 71c4898..ba8b107 100644 --- a/.gitignore +++ b/.gitignore @@ -2,3 +2,4 @@ /why-icons.tar.xz /why-2.36.tar.gz /why-2.38.tar.gz +/why-2.39.tar.gz diff --git a/sources b/sources index d04e7bd..03523ce 100644 --- a/sources +++ b/sources @@ -1,3 +1,3 @@ SHA512 (krakatoa.pdf) = 5d0f4e6b938ddc1eafa48264c02cf99e68f776a7e190b997e35fb2cd154627b5d27369886f570cbcfdfe5f3a1929a97a1fec9457a6f6662f83cbb2e51f65ca04 -SHA512 (why-2.38.tar.gz) = 304cda3aa2f0ca2e114cf3bc6f2bb89327ec97b0f2217d605dbcda3b7601550992bb757724af43ba4ee7ca8eb7ca8bcacb218265acbe7b7b275de9cca86f88a9 SHA512 (why-icons.tar.xz) = d6ca78cf09540f5742564912470fb8c49f7d11ca16cd8bb60c8790af10c1591198f6020bd792cff8e3464f762b7ef0a690d3e4ba1a2cf670c286c8056d266bc3 +SHA512 (why-2.39.tar.gz) = b36e9423ff82fa2f51fea40a33021ed0def3719d9421b2f7f1e2aa1d6113faacf932984ac293b6d0ac92f800fd48efbdd8cc3ec6a929003a57da20efab682bad diff --git a/why.spec b/why.spec index bf21dc4..51b52eb 100644 --- a/why.spec +++ b/why.spec @@ -9,8 +9,8 @@ %global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0) Name: why -Version: 2.38 -Release: 6%{?dist} +Version: 2.39 +Release: 1%{?dist} Summary: Software verification platform License: LGPLv2 with exceptions @@ -247,7 +247,8 @@ gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || : %changelog -* Wed Sep 06 2017 Richard W.M. Jones - 2.38-6 +* Wed Sep 06 2017 Richard W.M. Jones - 2.39-1 +- Update to 2.39. - OCaml 4.05.0 rebuild. * Thu Aug 03 2017 Fedora Release Engineering - 2.38-5 From c7cd340a99738b21a8488313dd394a640ca48e4a Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 11 Dec 2017 21:03:53 -0700 Subject: [PATCH 2/2] Bring back the -project patch, still needed (bz 1520483). --- why-project.patch | 115 ++++++++++++++++++++++++++++++++++++++++++++++ why.spec | 13 +++++- 2 files changed, 127 insertions(+), 1 deletion(-) create mode 100644 why-project.patch diff --git a/why-project.patch b/why-project.patch new file mode 100644 index 0000000..e50186a --- /dev/null +++ b/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.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 "
Save Proj + " ns; + wprint ""; + List.iter (fun prover -> +- wprint "" (Project.provers_name prover)) ++ wprint "" (Whyproject.provers_name prover)) + provers; + wprint " + "; diff --git a/why.spec b/why.spec index c7e7301..cf74d92 100644 --- a/why.spec +++ b/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,6 +252,9 @@ gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || : %changelog +* Sat Dec 9 2017 Jerry James - 2.39-3 +- Bring back the -project patch, still needed (bz 1520483) + * Sat Oct 7 2017 Jerry James - 2.39-2 - Rebuild for why3 0.88.0
%s%s