Commit f6fb3b95 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

IDE: on prover upgrade, new prover name is now displayed immediately

parent d2d4a97b
......@@ -592,6 +592,7 @@ let interpNotif (n: notification) =
match up with
| Proved true -> TaskList.update_status `Valid (string_of_int nid)
| Proved false -> TaskList.update_status `Unknown (string_of_int nid)
| Name_change _n -> assert false (* TODO *)
| Proof_status_change (c, _obsolete, _rl) ->
begin
(* TODO complete other tests *)
......
......@@ -1274,6 +1274,7 @@ let on_selected_row r =
| Controller_itp.InternalFailure e ->
(Pp.sprintf "internal failure: %a" Exn_printer.exn_printer e)
| Controller_itp.Uninstalled _p -> "uninstalled prover"
| Controller_itp.UpgradeProver _p -> "upgraded prover"
in
let output_text =
if output_text = "" then
......@@ -1516,6 +1517,7 @@ let image_of_pa_status ~obsolete pa =
| Controller_itp.InternalFailure _e -> !image_failure
| Controller_itp.Detached -> !image_undone (* TODO !image_detached *)
| Controller_itp.Uninstalled _p -> !image_undone (* TODO !image_uninstalled *)
| Controller_itp.UpgradeProver _p -> !image_undone
| Controller_itp.Done r ->
let pr_answer = r.Call_provers.pr_answer in
begin
......@@ -1606,6 +1608,7 @@ let set_status_and_time_column ?limit row =
| C.Interrupted -> "(interrupted)"
| C.Undone -> "(undone)"
| C.Uninstalled _ -> "(uninstalled prover)"
| C.UpgradeProver _ -> "(upgraded prover)"
| C.Scheduled -> "(scheduled)"
| C.Running -> "(running)"
| C.Detached -> "(detached)"
......@@ -1913,7 +1916,10 @@ let treat_notification n =
with Not_found ->
Debug.dprintf debug "Warning: no gtk row registered for node %d@." id
end
end
end
| Name_change n ->
let row = get_node_row id in
goals_model#set ~row:row#iter ~column:name_column n
| Proof_status_change (pa, obs, l) ->
let r = get_node_row id in
Hint.replace node_id_pa id (pa, obs, l);
......
......@@ -39,6 +39,7 @@ type proof_attempt_status =
| Detached (** parent goal has no task, is detached *)
| InternalFailure of exn (** external proof aborted by internal error *)
| Uninstalled of Whyconf.prover (** prover is uninstalled *)
| UpgradeProver of Whyconf.prover (** prover is upgraded *)
let print_status fmt st =
match st with
......@@ -53,6 +54,8 @@ let print_status fmt st =
fprintf fmt "InternalFailure(%a)" Exn_printer.exn_printer e
| Uninstalled pr ->
fprintf fmt "Prover %a is uninstalled" Whyconf.print_prover pr
| UpgradeProver pr ->
fprintf fmt "Prover upgrade to %a" Whyconf.print_prover pr
type transformation_status =
| TSscheduled | TSdone of transID | TSfailed of (proofNodeID * exn)
......@@ -488,6 +491,7 @@ let schedule_proof_attempt c id pr
let callback panid s =
begin
match s with
| UpgradeProver _ -> ()
| Scheduled ->
Hpan.add c.controller_running_proof_attempts panid ();
update_goal_node notification ses id
......@@ -575,10 +579,11 @@ let replay_proof_attempt c pr limit (parid: proofNodeID) id ~callback ~notificat
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 ->
| Some pr' ->
try
if pr' <> pr then callback id (UpgradeProver pr');
let _ = get_raw_task c.controller_session parid in
schedule_proof_attempt c parid pr ~counterexmp:false ~limit ~callback ~notification
schedule_proof_attempt c parid pr' ~counterexmp:false ~limit ~callback ~notification
with Not_found ->
callback id Detached
......@@ -677,6 +682,7 @@ let schedule_edition c id pr ~callback ~notification =
let callback panid s =
begin
match s with
| UpgradeProver _ -> ()
| Running -> ()
| Done res ->
(* set obsolete to true since we do not know if the manual
......@@ -750,7 +756,7 @@ let run_strategy_on_goal
let callback panid res =
callback_pa panid res;
match res with
| Scheduled | Running -> (* nothing to do yet *) ()
| UpgradeProver _ | Scheduled | Running -> (* nothing to do yet *) ()
| Done { Call_provers.pr_answer = Call_provers.Valid } ->
(* proof succeeded, nothing more to do *)
callback STShalt
......@@ -954,7 +960,7 @@ let replay ?(obsolete_only=true) ?(use_steps=false)
let craft_report count s r id pr limits pa =
match s with
| Scheduled | Running -> ()
| UpgradeProver _ | Scheduled | Running -> ()
| Undone | Interrupted ->
decr count;
r := (id, pr, limits, Replay_interrupted ) :: !r
......@@ -1072,7 +1078,7 @@ let bisect_proof_attempt ~callback_tr ~callback_pa ~notification ~removed c pa_i
let callback paid st =
callback_pa paid st;
begin match st with
| Scheduled | Running -> ()
| UpgradeProver _ | Scheduled | Running -> ()
| Detached | Uninstalled _ -> assert false
| Undone | Interrupted -> Debug.dprintf debug "Bisecting interrupted.@."
| InternalFailure exn ->
......@@ -1133,7 +1139,9 @@ later on. We do has if proof fails. *)
let limit = { limit with Call_provers.limit_time = !timelimit; } in
let callback paid st =
callback_pa paid st;
begin match st with
begin
match st with
| UpgradeProver _ -> ()
| Scheduled ->
Debug.dprintf
debug "[Bisect] prover on subtask is scheduled@."
......
......@@ -25,6 +25,7 @@ type proof_attempt_status =
| Detached (** parent goal has no task, is detached *)
| InternalFailure of exn (** external proof aborted by internal error *)
| Uninstalled of Whyconf.prover (** prover is uninstalled *)
| UpgradeProver of Whyconf.prover (** prover is upgraded *)
val print_status : Format.formatter -> proof_attempt_status -> unit
......
......@@ -68,6 +68,7 @@ type color =
type update_info =
| Proved of bool
| Name_change of string
| Proof_status_change of
Controller_itp.proof_attempt_status
* bool (* obsolete or not *)
......
......@@ -74,6 +74,7 @@ type color =
type update_info =
| Proved of bool
| Name_change of string
| Proof_status_change of
Controller_itp.proof_attempt_status
* bool (* obsolete or not *)
......
......@@ -304,7 +304,8 @@ let print_notify fmt n =
| Node_change (ni, nf) ->
begin
match nf with
| Proved b -> fprintf fmt "node change %d Proved %b" ni b
| Proved b -> fprintf fmt "node change %d: proved=%b" ni b
| Name_change n -> fprintf fmt "node change %d: renamed to '%s'" ni n
| Proof_status_change(st,b,_lim) ->
fprintf fmt "node change %d Proof_status_change res=%a obsolete=%b limits=<TODO>"
ni Controller_itp.print_status st b
......@@ -1012,6 +1013,12 @@ end
let parent = node_ID_from_pn parent_id in
new_node ~parent (APa panid)
in
begin match pa_status with
| UpgradeProver _ ->
let n = get_node_name (APa panid) in
P.notify (Node_change (node_id, Name_change n))
| _ -> ()
end;
let pa = get_proof_attempt_node ses panid in
let new_status =
Proof_status_change (pa_status, pa.proof_obsolete, pa.limit)
......
......@@ -94,6 +94,9 @@ let convert_proof_attempt (pas: proof_attempt_status) =
"exception", String (Pp.string_of Exn_printer.exn_printer e)]
| Uninstalled p ->
convert_record ["proof_attempt", String "Uninstalled";
"prover", convert_prover_to_json p]
| UpgradeProver p ->
convert_record ["proof_attempt", String "UpgradeProver";
"prover", convert_prover_to_json p])
let convert_update u =
......@@ -101,17 +104,15 @@ let convert_update u =
| Proved b ->
convert_record ["update_info", String "Proved";
"proved", Bool b]
| Name_change n ->
convert_record ["update_info", String "Name_change";
"name", String n]
| Proof_status_change (pas, b, l) ->
convert_record ["update_info", String "Proof_status_change";
"proof_attempt", convert_proof_attempt pas;
"obsolete", Bool b;
"limit", convert_limit l]
(*
| Obsolete b ->
convert_record ["update_info", String "Obsolete";
"obsolete", Bool b]
*)
)
)
let convert_notification_constructor n =
match n with
......@@ -562,6 +563,9 @@ let parse_proof_attempt j =
| "Uninstalled" ->
let p = get_field j "prover" in
Uninstalled (parse_prover_from_json p)
| "UpgradeProver" ->
let p = get_field j "prover" in
UpgradeProver (parse_prover_from_json p)
| _ -> raise NotProofAttempt
exception NotUpdate
......@@ -572,16 +576,14 @@ let parse_update j =
| "Proved" ->
let b = get_bool (get_field j "proved") in
Proved b
| "Name_change" ->
let n = get_string (get_field j "name") in
Name_change n
| "Proof_status_change" ->
let pas = get_field j "proof_attempt" in
let b = get_bool (get_field j "obsolete") in
let l = get_field j "limit" in
Proof_status_change (parse_proof_attempt pas, b, parse_limit_from_json l)
(*
| "Obsolete" ->
let b = get_bool (get_field j "obsolete") in
Obsolete b
*)
| _ -> raise NotUpdate
exception NotInfos of string
......
......@@ -223,7 +223,9 @@ let change_node fmt (n: node_ID) (u: update_info) =
node.node_proved <- b
| Proof_status_change (_pas, _b, _rl) when node.node_type = SProofAttempt ->
fprintf fmt "Not yet supported@." (* TODO *)
| _ -> fprintf fmt "Not yet supported@.") (* TODO *)
| Proof_status_change _ ->
fprintf fmt "Not yet supported@." (* TODO *)
| Name_change _ -> fprintf fmt "Not yet supported@.") (* TODO *)
with
Not_found -> fprintf fmt "Could not find node %d@." n
......
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