Commit bf928f12 authored by MARCHE Claude's avatar MARCHE Claude

upgrade provers during replay (partial)

partial because non interactive: prover upgrade policy must be set in config file
it remains to reactivate prover policy dialog in gtk.
parent 302b089a
......@@ -446,6 +446,52 @@ let schedule_proof_attempt ?proof_script c id pr
in
schedule_proof_attempt_r ?proof_script c id pr ~counterexmp ~limit ~callback
(* replay *)
let find_prover notification c goal_id pr =
if Hprover.mem c.controller_provers pr then Some pr else
match Whyconf.get_prover_upgrade_policy c.controller_config pr with
| exception Not_found -> None
| Whyconf.CPU_keep -> None
| Whyconf.CPU_upgrade new_pr ->
(* does a proof using new_pr already exists ? *)
if Hprover.mem (get_proof_attempt_ids c.controller_session goal_id) new_pr
then (* yes, then we do nothing *)
None
else
begin
(* we modify the prover in-place *)
Session_itp.change_prover notification c.controller_session goal_id pr new_pr;
Some new_pr
end
| Whyconf.CPU_duplicate _new_pr ->
assert false (* TODO *)
(*
(* does a proof using new_p already exists ? *)
if Hprover.mem (goal_external_proofs parid) new_pr
then (* yes, then we do nothing *)
None
else
begin
(* we duplicate the proof_attempt *)
let new_a = copy_external_proof
~notify ~keygen:O.create ~prover:new_p ~env_session:eS a
in
Some new_pr
end
*)
let replay_proof_attempt ?proof_script c pr limit (parid: proofNodeID) id ~callback ~notification =
(* The replay can be done on a different machine so we need
to check more things before giving the attempt to the scheduler *)
match find_prover notification c parid pr with
| None -> callback id (Uninstalled pr)
| Some pr ->
schedule_proof_attempt ?proof_script c parid pr ~counterexmp:false ~limit ~callback ~notification
(* TODO to be simplified *)
(* create the path to a file for saving the external proof script *)
let create_file_rel_path c pr pn =
......@@ -497,14 +543,6 @@ let update_edit_external_proof c pn ?panid pr =
close_out ch;
file
let replay_proof_attempt ?proof_script c pr limit (parid: proofNodeID) id ~callback ~notification =
(* The replay can be done on a different machine so we need
to check more things before giving the attempt to the scheduler *)
if not (Hprover.mem c.controller_provers pr) then
callback id (Uninstalled pr)
else
schedule_proof_attempt ?proof_script c parid pr ~counterexmp:false ~limit ~callback ~notification
exception Editor_not_found
let schedule_edition c id pr ~no_edit ~do_check_proof ?file ~callback ~notification =
......
......@@ -49,7 +49,7 @@ type proof_parent = Trans of transID | Theory of theory
type proof_attempt_node = {
parent : proofNodeID;
prover : Whyconf.prover;
mutable prover : Whyconf.prover;
limit : Call_provers.resource_limit;
mutable proof_state : Call_provers.prover_result option;
(* None means that the call was not done or never returned *)
......@@ -694,7 +694,6 @@ let update_proof_attempt ?(obsolete=false) s id pr st =
| BadID when not (Debug.test_flag debug_stack_trace) -> assert false
(* proved status *)
......@@ -825,6 +824,22 @@ let update_any_node s notification a =
| ATh th -> update_theory_node notification s th
let change_prover notification s id opr npr =
try
let n = get_proofNode s id in
let paid = Hprover.find n.proofn_attempts opr in
let pa = get_proof_attempt_node s paid in
Hprover.remove n.proofn_attempts opr;
pa.prover <- npr;
pa.proof_obsolete <- true;
Hprover.add n.proofn_attempts npr paid;
update_goal_node notification s id
with
| Not_found -> ()
| BadID when not (Debug.test_flag debug_stack_trace) -> assert false
(* Remove elements of the session tree *)
let remove_transformation (s : session) (id : transID) =
......
......@@ -71,13 +71,13 @@ val theory_detached_goals : theory -> proofNodeID list
val theory_parent : session -> theory -> file
type proof_attempt_node = private {
parent : proofNodeID;
prover : Whyconf.prover;
limit : Call_provers.resource_limit;
mutable proof_state : Call_provers.prover_result option;
parent : proofNodeID;
mutable prover : Whyconf.prover;
limit : Call_provers.resource_limit;
mutable proof_state : Call_provers.prover_result option;
(* None means that there is a prover call in progress *)
mutable proof_obsolete : bool;
proof_script : string option; (* non empty for external ITP *)
mutable proof_obsolete : bool;
proof_script : string option; (* non empty for external ITP *)
}
(* [is_below s a b] true if a is below b in the session tree *)
......@@ -197,14 +197,6 @@ val graft_proof_attempt : ?file:string -> session -> proofNodeID ->
proof_script field equal to [file].
*)
val update_proof_attempt : ?obsolete:bool -> session -> proofNodeID ->
Whyconf.prover -> Call_provers.prover_result -> unit
(** [update_proof_attempt ?obsolete s id pr st] update the status of the
corresponding proof attempt with [st].
If [obsolete] is set to true, it marks the proof_attempt obsolete
direclty (useful for interactive prover).
*)
val apply_trans_to_goal :
allow_no_effect:bool -> session -> Env.env -> string -> string list ->
proofNodeID -> Task.task list
......@@ -286,3 +278,18 @@ val update_trans_node : notifier -> session -> transID -> unit
(** updates the proved status of the given transformation node. If
necessary, propagates the update to ancestors. [notifier] is
called on all nodes whose status changes *)
val update_proof_attempt : ?obsolete:bool (*-> notifier*) -> session -> proofNodeID ->
Whyconf.prover -> Call_provers.prover_result -> unit
(** [update_proof_attempt ?obsolete s id pr st] update the status of the
corresponding proof attempt with [st].
If [obsolete] is set to true, it marks the proof_attempt obsolete
direclty (useful for interactive prover).
*)
val change_prover : notifier -> session -> proofNodeID -> Whyconf.prover -> Whyconf.prover -> unit
(** [change_prover s id opr npr] changes the prover of the proof
attempt using prover [opr] by the new prover [npr]. Proof attempt
status is set to obsolete.
*)
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