[why] Rebuild for OCaml 4.01.0. Enable debuginfo. Add -or patch to fix warnings, since warnings are errors
Jerry James
jjames at fedoraproject.org
Wed Sep 18 04:09:49 UTC 2013
commit b6131f67e6123572e9ed13757336e2d62a59d58e
Author: Jerry James <loganjerry at gmail.com>
Date: Tue Sep 17 22:09:23 2013 -0600
Rebuild for OCaml 4.01.0.
Enable debuginfo.
Add -or patch to fix warnings, since warnings are errors.
why-2.33-or.patch | 184 +++++++++++++++++++++++++++++++++++++++++++++++++++++
why.spec | 26 ++++----
2 files changed, 198 insertions(+), 12 deletions(-)
---
diff --git a/why-2.33-or.patch b/why-2.33-or.patch
new file mode 100644
index 0000000..ae4afb4
--- /dev/null
+++ b/why-2.33-or.patch
@@ -0,0 +1,184 @@
+--- ./jc/jc_typing.ml.orig 2013-04-20 00:34:04.000000000 -0600
++++ ./jc/jc_typing.ml 2013-09-17 20:52:56.359746353 -0600
+@@ -2553,7 +2553,7 @@ let field st root ((rep,abs), t, id, bit
+ jc_field_info_type = ty;
+ jc_field_info_hroot = root;
+ jc_field_info_struct = st;
+- jc_field_info_rep = rep or (not (is_pointer_type ty));
++ jc_field_info_rep = rep || (not (is_pointer_type ty));
+ jc_field_info_abstract = abs;
+ jc_field_info_bitsize = bitsize;
+ } in
+--- ./jc/output.ml.orig 2013-04-20 00:34:04.000000000 -0600
++++ ./jc/output.ml 2013-09-17 20:48:00.511361646 -0600
+@@ -825,12 +825,12 @@ let rec fprintf_type ~need_colon anon fo
+ match t with
+ | Prod_type(id,t1,t2) ->
+ if !why3syntax then
+- let id = if id="" or anon then "_anonymous" else id in
++ let id = if id="" || anon then "_anonymous" else id in
+ fprintf form "@[<hov 1>(%s:%a)@ %a@]" (why3ident id)
+ (fprintf_type ~need_colon:false anon) t1
+ (fprintf_type ~need_colon anon) t2
+ else
+- if id="" or anon then
++ if id="" || anon then
+ fprintf form "@[<hov 1>%a ->@ %a@]"
+ (fprintf_type ~need_colon:false anon) t1
+ (fprintf_type ~need_colon anon) t2
+--- ./intf/pprinter.ml.orig 2013-04-20 00:34:04.000000000 -0600
++++ ./intf/pprinter.ml 2013-09-17 20:55:39.024735111 -0600
+@@ -67,7 +67,7 @@ let print_loc = function
+ ("file \""^ff^"\", line "^l^", characters "^s^" - "^e)
+
+ let is_cfile f =
+- Filename.check_suffix f ".c" or Filename.check_suffix f ".h"
++ Filename.check_suffix f ".c" || Filename.check_suffix f ".h"
+ (* otherwise it's .why *)
+
+ let read_file = function
+--- ./intf/colors.ml.orig 2013-04-20 00:34:04.000000000 -0600
++++ ./intf/colors.ml 2013-09-17 20:54:20.591014499 -0600
+@@ -96,7 +96,7 @@ let get_bc_predicate () =
+ get_bc "lpredicate"
+
+ let color_exists ty =
+- (Hashtbl.mem fcolors ty) or (Hashtbl.mem bcolors ty)
++ (Hashtbl.mem fcolors ty) || (Hashtbl.mem bcolors ty)
+
+ let get_all_colors () =
+ List.map
+--- ./intf/stat.ml.orig 2013-04-20 00:34:04.000000000 -0600
++++ ./intf/stat.ml 2013-09-17 20:57:01.083164075 -0600
+@@ -379,8 +379,8 @@ let expand_row (view:GTree.view) path be
+ *)
+ let try_proof oblig =
+ (Cache.hard_proof ())
+- or not (Cache.is_enabled ())
+- or (Cache.is_enabled () && not (in_cache (Cache.clean oblig)))
++ || not (Cache.is_enabled ())
++ || (Cache.is_enabled () && not (in_cache (Cache.clean oblig)))
+
+
+ (*
+@@ -391,7 +391,7 @@ let run_prover_child p (_view:GTree.view
+ let column_p = p.Model.pr_icon in
+ let column_i = p.Model.pr_image in
+ let (_, _, _, oblig, seq) = o in
+- if bench or (try_proof seq) then
++ if bench || (try_proof seq) then
+ try
+ let row =
+ try Hashtbl.find Model.orows oblig
+@@ -439,7 +439,7 @@ let run_prover_child p (_view:GTree.view
+ model#set ~row ~column:p.Model.pr_result result;
+ model#set ~row ~column:Model.result
+ (max result (model#get ~row ~column:Model.result));
+- if alone or (Tools.live_update ())then begin
++ if alone || (Tools.live_update ())then begin
+ build_statistics model (model#get ~row ~column:Model.parent)
+ end;
+ result
+@@ -558,7 +558,7 @@ let main () =
+ (let old_w = ref 0
+ and old_h = ref 0 in
+ fun {Gtk.width=w;Gtk.height=h} ->
+- if !old_w <> w or !old_h <> h then begin
++ if !old_w <> w || !old_h <> h then begin
+ old_h := h;
+ old_w := w;
+ Colors.window_height := h;
+--- ./src/main.ml.orig 2013-04-20 00:34:04.000000000 -0600
++++ ./src/main.ml 2013-09-17 19:49:18.233726051 -0600
+@@ -726,7 +726,7 @@ let main () =
+ if Options.delete_old_vcs then delete_old_vcs files;
+ iter_with_last deal_file files;
+ if type_only then exit 0;
+- if (pruning) or (Options.pruning_hyp_v != -1) then
++ if (pruning) || (Options.pruning_hyp_v != -1) then
+ begin
+ let q = declarationQueue in
+ encode q
+--- ./src/hypotheses_filtering.ml.orig 2013-04-20 00:34:04.000000000 -0600
++++ ./src/hypotheses_filtering.ml 2013-09-17 18:13:29.412330314 -0600
+@@ -862,7 +862,7 @@ PdlSet
+ module PdlSet = Set.Make(struct type t = vertexLabel
+ let compare = compare end)
+ let abstr_mem_of el pdl_set =
+- PdlSet.mem { l = el.l; pol = Pos } pdl_set or
++ PdlSet.mem { l = el.l; pol = Pos } pdl_set ||
+ PdlSet.mem { l = el.l; pol = Neg } pdl_set
+
+ let is_positive el =
+@@ -874,10 +874,10 @@ let mem_of el pdl_set =
+ (PdlSet.mem { l = el.l; pol = el.pol } pdl_set )
+
+ let mem_of_or_pos el pdl_set =
+- (PdlSet.mem { l = el.l; pol = el.pol } pdl_set ) or el.pol == Pos
++ (PdlSet.mem { l = el.l; pol = el.pol } pdl_set ) || el.pol == Pos
+
+ let mem_of_or_neg el pdl_set =
+- (PdlSet.mem { l = el.l; pol = el.pol } pdl_set ) or el.pol == Neg
++ (PdlSet.mem { l = el.l; pol = el.pol } pdl_set ) || el.pol == Neg
+
+ let abstr_subset_of_pdl set1 set2 =
+ if polarized_preds then
+@@ -1099,11 +1099,11 @@ let get_suffixed_ident i1 i2 =
+ (* in (remove_percents s) *)
+
+ let is_comparison id =
+- (is_int_comparison id or is_real_comparison id or is_comparison id)
++ (is_int_comparison id || is_real_comparison id || is_comparison id)
+
+ let comparison_to_consider id =
+ use_comparison_as_criteria_for_graph_construction && (
+- ((not comparison_eqOnly) && (is_int_comparison id or is_real_comparison id))
++ ((not comparison_eqOnly) && (is_int_comparison id || is_real_comparison id))
+ || (id == t_eq || id == t_neq || id == t_eq_int || id == t_neq_int || id == t_eq_real || id == t_neq_real )
+ )
+
+@@ -2121,7 +2121,7 @@ let filter_acc_variables l concl_rep sel
+ display_str "vars" vars;
+ display_str "concl_rep" concl_rep;
+ end;
+- if (!variablesMaximumDepth< !vb) or condition then
++ if (!variablesMaximumDepth< !vb) || condition then
+ begin
+ if debug then
+ begin
+@@ -2142,7 +2142,7 @@ let filter_acc_variables l concl_rep sel
+ display_symb_of_pdl_set pred_symb;
+ end;
+
+- if (!predicateMaximumDepth< !pb) or (abstr_subset_of_pdl preds_of_p pred_symb) then
++ if (!predicateMaximumDepth< !pb) || (abstr_subset_of_pdl preds_of_p pred_symb) then
+ begin
+ if debug then
+ begin
+@@ -2182,7 +2182,7 @@ let managesContext relevantPreds decl =
+ let preds_of_p = get_preds_of p use_comparison_as_criteria_for_hypothesis_filtering in
+
+
+- if (!predicateMaximumDepth< !pb) or (abstr_subset_of_pdl preds_of_p relevantPreds) then
++ if (!predicateMaximumDepth< !pb) || (abstr_subset_of_pdl preds_of_p relevantPreds) then
+ begin
+ if debug then
+ begin
+@@ -2206,7 +2206,7 @@ let managesContext relevantPreds decl =
+
+ | (p_cnf, Dpredicate_def (loc, ident, def)) :: l ->
+ let preds_of_p_cnf = get_preds_of p_cnf use_comparison_as_criteria_for_hypothesis_filtering in
+- if (!predicateMaximumDepth< !pb) or (abstr_subset_of_pdl preds_of_p_cnf relevantPreds) then
++ if (!predicateMaximumDepth< !pb) || (abstr_subset_of_pdl preds_of_p_cnf relevantPreds) then
+ begin
+ (* On garde tout le predicat *)
+ if debug then
+@@ -2240,7 +2240,7 @@ let managesContext relevantPreds decl =
+
+ | (p_cnf, Daxiom (loc, ident, ps)) :: l ->
+ let preds_of_p_cnf = get_preds_of p_cnf use_comparison_as_criteria_for_hypothesis_filtering in
+- if (!predicateMaximumDepth< !pb) or (abstr_subset_of_pdl preds_of_p_cnf relevantPreds) then
++ if (!predicateMaximumDepth< !pb) || (abstr_subset_of_pdl preds_of_p_cnf relevantPreds) then
+ begin
+ (* On garde tout l'axiome en forme originale *)
+ if debug then
diff --git a/why.spec b/why.spec
index f5a3676..9ba9c80 100644
--- a/why.spec
+++ b/why.spec
@@ -15,12 +15,9 @@
# 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.33
-Release: 4%{?dist}
+Release: 5%{?dist}
Summary: Software verification platform
Group: Applications/Engineering
@@ -61,6 +58,9 @@ Patch2: %{name}-2.33-hashtbl.patch
# Adapt to flocq 2.2.0. Result of a conversation with upstream on 20 Aug 2013.
Patch3: %{name}-2.33-flocq.patch
+# Change from the obsolete form of the "or" operator to the new form (||).
+Patch4: %{name}-2.33-or.patch
+
BuildRequires: auto-destdir
BuildRequires: cvc3
BuildRequires: desktop-file-utils
@@ -222,6 +222,7 @@ based on Why, including various automated and interactive provers.
%patch1
%patch2
%patch3
+%patch4
cp -p %SOURCE1 %SOURCE2 %SOURCE6 %SOURCE7 ./
@@ -266,6 +267,10 @@ sed -e "s|-I +apron|-I +apron -I +gmp|" \
# Allow use of the fixed frama-c Fluorine release
sed -i 's/Fluorine-20130401/Fluorine-20130601/' configure
+# Enable debuginfo
+sed -i 's|@STRIP@|/usr/bin/true|;s/-w Z/-g &/' Makefile.in
+sed -i 's/ocamlopt/& -g/;s/ocamlc/& -g/' atp/Makefile
+
%build
%if ! %{opt}
%global opt_option OCAMLBEST=byte OCAMLC=ocamlc OCAMLDEP=ocamldep OCAMLYACC=ocamlyacc OCAMLLEX=ocamllex
@@ -292,14 +297,6 @@ sed -e 's/pvs/pvs-sbcl/' -i configure
%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 \
@@ -442,6 +439,11 @@ diff -u min.why min_why.why.result # Show differences from correct result.
%changelog
+* Tue Sep 17 2013 Jerry James <loganjerry at 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 at iki.fi> - 2.33-4
- Install docs to %%{_pkgdocdir} where available.
More information about the scm-commits
mailing list