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

[Session] allow to update a session and that at the end all the tasks are released

parent dfb839fe
......@@ -1908,6 +1908,64 @@ let merge_metas_in_task ~theories env task from_metas =
in
Task.add_tdecl task goal,metas,to_idpos,!obsolete
(** Release and recover goal task *)
let release_task g =
Debug.dprintf debug "[Session] release %s@." g.goal_name.id_string;
g.goal_task <- None
let rec release_sub_tasks g =
release_task g;
PHstr.iter (fun _ t -> List.iter release_sub_tasks t.transf_goals)
g.goal_transformations;
Mmetas_args.iter (fun _ t -> release_sub_tasks t.metas_goal) g.goal_metas
exception UnrecoverableTask of Ident.ident
let rec recover_sub_tasks ~theories env_session task g =
g.goal_task <- Some task;
(** Check that the sum and shape don't change (the order is kept)
It seems an acceptable limitation. Non-deterministic transformation seems
ugly.
*)
let version = env_session.session.session_shape_version in
let sum = Termcode.task_checksum ~version task in
let shape = Termcode.t_shape_task ~version task in
if not (Termcode.equal_checksum sum g.goal_checksum &&
Termcode.equal_shape shape g.goal_shape) then
raise (UnrecoverableTask g.goal_name);
PHstr.iter (fun _ t ->
let task = goal_task g in
let subgoals = Trans.apply_transform t.transf_name env_session.env task in
List.iter2 (recover_sub_tasks ~theories env_session) subgoals t.transf_goals)
g.goal_transformations;
Mmetas_args.iter (fun _ t ->
let task,_metas,_to_idpos,_obsolete =
merge_metas_in_task ~theories env_session task t in
(** It is better to keep the original metas and idpos *)
(** If it is obsolete the next task will see it *)
recover_sub_tasks ~theories env_session task t.metas_goal
) g.goal_metas
let recover_theory_tasks env_session th =
let theories = Opt.get_exn NoTask th.theory_parent.file_for_recovery in
let theory = Opt.get_exn NoTask th.theory_task in
let tasks = List.rev (Task.split_theory theory None None) in
List.iter2 (recover_sub_tasks ~theories env_session) tasks th.theory_goals
let rec theory_goal g =
match g.goal_parent with
| Parent_theory th -> th
| Parent_transf t -> theory_goal t.transf_parent
| Parent_metas t -> theory_goal t.metas_parent
let goal_task_or_recover env_session g =
match g.goal_task with
| Some task -> task
| None ->
recover_theory_tasks env_session (theory_goal g);
Opt.get g.goal_task
(** merge session *)
(** ~theories is the current theory library path empty : [] *)
let rec merge_any_goal ~keygen ~theories env obsolete from_goal to_goal =
......@@ -1978,7 +2036,8 @@ and merge_metas ~keygen ~theories env to_goal s from_metas =
exception OutdatedSession
let merge_theory ~keygen ~theories env ~allow_obsolete from_th to_th =
let merge_theory
?(release=false) ~keygen ~theories env ~allow_obsolete from_th to_th =
set_theory_expanded to_th from_th.theory_expanded;
let from_goals = List.fold_left
(fun from_goals g ->
......@@ -1999,13 +2058,15 @@ let merge_theory ~keygen ~theories env ~allow_obsolete from_th to_th =
if not allow_obsolete then raise OutdatedSession;
found_obsolete := true;
end;
merge_any_goal ~keygen ~theories env goal_obsolete from_goal to_goal
merge_any_goal ~keygen ~theories env goal_obsolete from_goal to_goal;
if release then release_sub_tasks to_goal
with
| Not_found when allow_obsolete -> ()
| Not_found when allow_obsolete ->
if release then release_sub_tasks to_goal
| Not_found -> raise OutdatedSession
) to_th.theory_goals
let merge_file ~keygen ~theories env ~allow_obsolete from_f to_f =
let merge_file ?release ~keygen ~theories env ~allow_obsolete from_f to_f =
dprintf debug "[Info] merge_file, shape_version = %d@\n"
env.session.session_shape_version;
set_file_expanded to_f from_f.file_expanded;
......@@ -2022,7 +2083,7 @@ let merge_file ~keygen ~theories env ~allow_obsolete from_f to_f =
(* TODO: remove this later when all sessions are updated *)
with Not_found -> Mstr.find ("WP "^name) from_theories
in
merge_theory ~keygen ~theories env ~allow_obsolete from_th to_th
merge_theory ?release ~keygen ~theories env ~allow_obsolete from_th to_th
with
| Not_found when allow_obsolete -> ()
| Not_found -> raise OutdatedSession
......@@ -2050,7 +2111,7 @@ let recompute_all_shapes session =
session.session_shape_version <- Termcode.current_shape_version;
PHstr.iter recompute_all_shapes_file session.session_files
let update_session ~keygen ~allow_obsolete old_session env whyconf =
let update_session ?release ~keygen ~allow_obsolete old_session env whyconf =
dprintf debug "[Info] update_session: shape_version = %d@\n"
old_session.session_shape_version;
let new_session =
......@@ -2074,8 +2135,9 @@ let update_session ~keygen ~allow_obsolete old_session env whyconf =
?format:old_file.file_format old_file.file_name
in
let theories = Opt.get new_file.file_for_recovery in
dprintf debug "[Merge] file '%s'@\n" old_file.file_name;
merge_file ~keygen ~theories
new_env_session ~allow_obsolete old_file new_file;
?release new_env_session ~allow_obsolete old_file new_file;
let fname =
Filename.basename (Filename.chop_extension old_file.file_name)
in
......@@ -2220,62 +2282,6 @@ and add_transf_to_goal ~keygen env to_goal from_transf =
) associated;
to_transf
(** Release and recover goal task *)
let release_task g =
g.goal_task <- None
let rec release_sub_tasks g =
release_task g;
PHstr.iter (fun _ t -> List.iter release_sub_tasks t.transf_goals)
g.goal_transformations;
Mmetas_args.iter (fun _ t -> release_sub_tasks t.metas_goal) g.goal_metas
exception UnrecoverableTask of Ident.ident
let rec recover_sub_tasks ~theories env_session task g =
g.goal_task <- Some task;
(** Check that the sum and shape don't change (the order is kept)
It seems an acceptable limitation. Non-deterministic transformation seems
ugly.
*)
let version = env_session.session.session_shape_version in
let sum = Termcode.task_checksum ~version task in
let shape = Termcode.t_shape_task ~version task in
if not (Termcode.equal_checksum sum g.goal_checksum &&
Termcode.equal_shape shape g.goal_shape) then
raise (UnrecoverableTask g.goal_name);
PHstr.iter (fun _ t ->
let task = goal_task g in
let subgoals = Trans.apply_transform t.transf_name env_session.env task in
List.iter2 (recover_sub_tasks ~theories env_session) subgoals t.transf_goals)
g.goal_transformations;
Mmetas_args.iter (fun _ t ->
let task,_metas,_to_idpos,_obsolete =
merge_metas_in_task ~theories env_session task t in
(** It is better to keep the original metas and idpos *)
(** If it is obsolete the next task will see it *)
recover_sub_tasks ~theories env_session task t.metas_goal
) g.goal_metas
let recover_theory_tasks env_session th =
let theories = Opt.get_exn NoTask th.theory_parent.file_for_recovery in
let theory = Opt.get_exn NoTask th.theory_task in
let tasks = List.rev (Task.split_theory theory None None) in
List.iter2 (recover_sub_tasks ~theories env_session) tasks th.theory_goals
let rec theory_goal g =
match g.goal_parent with
| Parent_theory th -> th
| Parent_transf t -> theory_goal t.transf_parent
| Parent_metas t -> theory_goal t.metas_parent
let goal_task_or_recover env_session g =
match g.goal_task with
| Some task -> task
| None ->
recover_theory_tasks env_session (theory_goal g);
Opt.get g.goal_task
let get_project_dir fname =
if not (Sys.file_exists fname) then raise Not_found;
let d =
......
......@@ -226,7 +226,9 @@ type 'key keygen = ?parent:'key -> unit -> 'key
exception OutdatedSession
val update_session : keygen:'a keygen ->
val update_session :
?release:bool (* default false *) ->
keygen:'a keygen ->
allow_obsolete:bool -> 'b session ->
Env.env -> Whyconf.config -> 'a env_session * bool
(** reload the given session with the given environnement :
......
......@@ -334,10 +334,11 @@ let schedule_delayed_action t callback =
(* session function *)
(**************************)
let update_session ~allow_obsolete old_session env whyconf =
let update_session ?release ~allow_obsolete old_session env whyconf =
O.reset ();
let (env_session,_) as res =
update_session ~keygen:O.create ~allow_obsolete old_session env whyconf in
update_session ?release
~keygen:O.create ~allow_obsolete old_session env whyconf in
dprintf debug "Init_session@\n";
init_session env_session.session;
res
......@@ -503,7 +504,7 @@ let run_external_proof_v3 eS eT a callback =
~driver:npc.prover_driver
~callback:cb
eT
(goal_task a.proof_parent)
(goal_task_or_recover eS a.proof_parent)
with NoFile f ->
callback a ap 0 None (MissingFile f)
end
......@@ -784,7 +785,8 @@ let play_all eS eT ~callback ~timelimit ~memlimit l =
(** Transformation *)
let transformation_on_goal_aux eS tr keep_dumb_transformation g =
let subgoals = Trans.apply_transform tr eS.env (goal_task g) in
let gtask = goal_task_or_recover eS g in
let subgoals = Trans.apply_transform tr eS.env gtask in
let b = keep_dumb_transformation ||
match subgoals with
| [task] ->
......@@ -798,7 +800,7 @@ let transformation_on_goal_aux eS tr keep_dumb_transformation g =
(Obj.magic task); *)
(* *\) *)
(* s1 <> s2 *)
not (Task.task_equal task (goal_task g))
not (Task.task_equal task gtask)
| _ -> true
in
if b then
......@@ -877,11 +879,8 @@ let edit_proof_v3 eS sched ~default_editor callback a =
with Not_found -> default_editor
in
let file = update_edit_external_proof eS a in
dprintf debug "[Editing] goal %a with command '%s' on file %s@."
(fun fmt a -> pp_print_string fmt
(Task.task_goal (goal_task a.proof_parent))
. Decl.pr_name.Ident.id_string)
a editor file;
dprintf debug "[Editing] goal %s with command '%s' on file %s@."
a.proof_parent.goal_name.Ident.id_string editor file;
schedule_edition sched editor file (fun res -> callback a res)
let edit_proof eS sched ~default_editor a =
......
......@@ -112,6 +112,7 @@ module Make(O: OBSERVER) : sig
(** {2 Save and load a state} *)
val update_session :
?release:bool ->
allow_obsolete:bool ->
'key session ->
Env.env -> Whyconf.config ->
......
......@@ -9,7 +9,6 @@
(* *)
(********************************************************************)
open Format
open Why3
......@@ -364,7 +363,7 @@ let add_to_check_no_smoke config found_obs env_session sched =
exit 1
end
in
M.check_all ~release:true ~callback env_session sched
M.check_all ~release:false ~callback env_session sched
let add_to_check_smoke env_session sched =
let callback report =
......@@ -432,13 +431,14 @@ let run_as_bench env_session =
eprintf "main replayer (in bench mode) exited unexpectedly@.";
exit 1
let () =
try
Debug.dprintf debug "Opening session...@?";
O.verbose := Debug.test_flag debug;
let env_session,found_obs =
let session = S.read_session project_dir in
M.update_session ~allow_obsolete:true session env config
M.update_session ~release:true ~allow_obsolete:true session env config
in
Debug.dprintf debug " done.@.";
if !opt_obsolete_only && not found_obs
......
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