Commit f188489a authored by François Bobot's avatar François Bobot
Browse files

Why3 replayer: add option remove_converted

parent c2887483
...@@ -32,7 +32,7 @@ let opt_latex2 = ref "" ...@@ -32,7 +32,7 @@ let opt_latex2 = ref ""
let opt_longtable = ref false let opt_longtable = ref false
let opt_force = ref false let opt_force = ref false
let opt_convert_unknown_provers = ref false let opt_convert_unknown_provers = ref false
let opt_remove_converted = ref false
(** {2 Smoke detector} *) (** {2 Smoke detector} *)
type smoke_detector = type smoke_detector =
...@@ -76,8 +76,9 @@ let spec = Arg.align [ ...@@ -76,8 +76,9 @@ let spec = Arg.align [
Arg.Set opt_longtable, Arg.Set opt_longtable,
" produce latex statistics using longtable package") ; " produce latex statistics using longtable package") ;
"--convert-unknown-provers", Arg.Set opt_convert_unknown_provers, "--convert-unknown-provers", Arg.Set opt_convert_unknown_provers,
" try to find compatible provers for all unknown provers. The external \ " try to find compatible provers for all unknown provers.";
proof which have been converted are removed"; "--remove-converted", Arg.Set opt_remove_converted,
" The external proof which have been converted are removed";
Debug.Opt.desc_debug_list; Debug.Opt.desc_debug_list;
Debug.Opt.desc_shortcut "parse_only" "--parse-only" " Stop after parsing"; Debug.Opt.desc_shortcut "parse_only" "--parse-only" " Stop after parsing";
Debug.Opt.desc_shortcut Debug.Opt.desc_shortcut
...@@ -694,7 +695,8 @@ let () = ...@@ -694,7 +695,8 @@ let () =
M.update_session ~allow_obsolete:true session env config in M.update_session ~allow_obsolete:true session env config in
transform_smoke env_session; transform_smoke env_session;
if !opt_convert_unknown_provers then if !opt_convert_unknown_provers then
M.convert_unknown_prover ~remove_converted:true env_session; M.convert_unknown_prover
~remove_converted:!opt_remove_converted env_session;
let sched = let sched =
M.init (Whyconf.running_provers_max (Whyconf.get_main config)) in M.init (Whyconf.running_provers_max (Whyconf.get_main config)) in
if found_obs then begin if found_obs then begin
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment