Commit c35f496f authored by François Bobot's avatar François Bobot

Replayer should remain straight. The convert-unknown and remove-converted

have too complicated semantics. why3session should do the job.

Revert "Why3 replayer: add option remove_converted"

This reverts commit f188489a.

Revert "replay remove converted external proof"

This reverts commit c2887483.

Conflicts:

	src/session/session_tools.ml
parent ab24b3e2
......@@ -32,7 +32,8 @@ let opt_latex2 = ref ""
let opt_longtable = ref false
let opt_force = ref false
let opt_convert_unknown_provers = ref false
let opt_remove_converted = ref false
(** {2 Smoke detector} *)
type smoke_detector =
......@@ -76,9 +77,7 @@ let spec = Arg.align [
Arg.Set opt_longtable,
" produce latex statistics using longtable package") ;
"--convert-unknown-provers", Arg.Set opt_convert_unknown_provers,
" try to find compatible provers for all unknown provers.";
"--remove-converted", Arg.Set opt_remove_converted,
" The external proof which have been converted are removed";
" try to find compatible provers for all unknown provers";
Debug.Opt.desc_debug_list;
Debug.Opt.desc_shortcut "parse_only" "--parse-only" " Stop after parsing";
Debug.Opt.desc_shortcut
......@@ -610,12 +609,9 @@ session NOT updated)@." n m
printf " %d/%d@." n m ;
if !opt_stats && n<m then print_statistics files;
eprintf "Everything replayed OK.@.";
if (!opt_convert_unknown_provers || found_obs)
&& (n=m || !opt_force) then
if found_obs && (n=m || !opt_force) then
begin
eprintf "Updating %s%ssession...@?"
(if !opt_convert_unknown_provers then "converted " else "")
(if found_obs then "obsolete " else "");
eprintf "Updating obsolete session...@?";
S.save_session session;
eprintf " done@."
end;
......@@ -674,9 +670,7 @@ let () =
let session = S.read_session project_dir in
M.update_session ~allow_obsolete:true session env config in
transform_smoke env_session;
if !opt_convert_unknown_provers then
M.convert_unknown_prover
~remove_converted:!opt_remove_converted env_session;
if !opt_convert_unknown_provers then M.convert_unknown_prover env_session;
let sched =
M.init (Whyconf.running_provers_max (Whyconf.get_main config)) in
if found_obs then begin
......
......@@ -178,8 +178,7 @@ module Make(O: OBSERVER) : sig
which are triples (goal name, prover, report)
*)
val convert_unknown_prover :
?remove_converted:bool -> O.key env_session -> unit
val convert_unknown_prover : O.key env_session -> unit
(** Same as {!Session_tools.convert_unknown_prover} *)
end
......
......@@ -36,7 +36,7 @@ let utkp provers pu () =
let _,name,version = unknown_to_known_provers provers pu in
version@name
let convert_unknown_prover ?(remove_converted=false) ~keygen env_session =
let convert_unknown_prover ~keygen env_session =
let known_provers = get_provers env_session.whyconf in
let provers = get_used_provers env_session.session in
let unknown_provers = Mprover.set_diff provers known_provers in
......@@ -46,15 +46,11 @@ let convert_unknown_prover ?(remove_converted=false) ~keygen env_session =
Mprover.mapi (utkp known_provers) unknown_provers in
session_iter_proof_attempt (fun pr ->
let pks = Mprover.find_default pr.proof_prover [] unknown_provers in
let converted = ref false in
List.iter (fun pk ->
(** If such a prover already exists we add nothing *)
if not (PHprover.mem pr.proof_parent.goal_external_proofs pk) then
converted := true;
ignore (copy_external_proof ~keygen ~prover:pk pr)
) pks;
(** pks = [] (!converted = false) also for the one which are known *)
if remove_converted && !converted then Session.remove_external_proof pr
) env_session.session
end
......
......@@ -28,11 +28,9 @@ val unknown_to_known_provers :
Whyconf.Mprover.key list
(** return others, same name, same version *)
val convert_unknown_prover :
?remove_converted:bool -> keygen:'a keygen -> 'a env_session -> unit
val convert_unknown_prover : keygen:'a keygen -> 'a env_session -> unit
(** try to add new proof_attempt with known provers for all proof
attempt with unknown provers. If [remove_converted] is true the
proof_attempt which have been converted are removed *)
attempt with unknown provers *)
val filter_proof_attempt :
?notify:'key notify ->
......
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