Commit 60f3cf74 authored by MARCHE Claude's avatar MARCHE Claude

Fix empty node status when proof_result is None

parent 0a38df2a
......@@ -558,6 +558,12 @@ let show_legend_window () =
i " Valid but obsolete result\n";
ib image_unknown_obs;
i " Answer not conclusive and obsolete\n";
ib image_timeout_obs;
i " Time limit reached, obsolete\n";
ib image_outofmemory_obs;
i " Out of memory, obsolete\n";
ib image_steplimitexceeded_obs;
i " Step limit exceeded, obsolete\n";
ib image_invalid_obs;
i " Prover disproved goal, but obsolete\n";
ib image_failure_obs;
......
......@@ -1516,10 +1516,10 @@ let set_status_and_time_column ?limit row =
| C.Running ->
match limit with
| Some l ->
Format.sprintf "[limit=%d sec., %d M]"
Format.sprintf "(scheduled?) [limit=%d sec., %d M]"
(l.Call_provers.limit_time)
(l.Call_provers.limit_mem)
| None -> ""
| None -> "(scheduled?) [no limit known]"
in
let t = if obs then t ^ " (obsolete)" else t in
goals_model#set ~row:row#iter ~column:time_column t;
......@@ -1668,11 +1668,13 @@ let treat_notification n =
let r = get_node_row id in
Hint.replace node_id_pa id (pa, obs, l);
set_status_and_time_column ~limit:l r
(*
| Obsolete b ->
let r = get_node_row id in
let (pa, _, l) = Hint.find node_id_pa id in
Hint.replace node_id_pa id (pa, b, l);
set_status_and_time_column ~limit:l r
*)
end
| Next_Unproven_Node_Id (asked_id, next_unproved_id) ->
if_selected_alone asked_id
......
......@@ -247,11 +247,9 @@ let update_file_node notification c f =
let ps = c.proof_state in
let ths = f.file_theories in
let proved = List.for_all (th_proved c) ths in
Format.eprintf "[TEMP] notify file status is now proved = %b@." proved;
if proved <> file_proved c f then
begin
Stdlib.Hstr.replace ps.file_state f.file_name proved;
Format.eprintf "[TEMP]notify file status change@.";
notification (AFile f);
end
......@@ -262,7 +260,6 @@ let update_theory_node notification c th =
if proved <> th_proved c th then
begin
Hid.replace ps.th_state (theory_name th) proved;
Format.eprintf "[TEMP]notify theory status change@.";
notification (ATh th);
update_file_node notification c (theory_parent c.controller_session th)
end
......
......@@ -59,7 +59,6 @@ type update_info =
Controller_itp.proof_attempt_status
* bool (* obsolete or not *)
* Call_provers.resource_limit
| Obsolete of bool
type notification =
| New_node of node_ID * node_ID * node_type * string * bool
......
......@@ -65,8 +65,6 @@ type update_info =
Controller_itp.proof_attempt_status
* bool (* obsolete or not *)
* Call_provers.resource_limit
(* TODO: remove this case, it should be handled by the one above *)
| Obsolete of bool
type notification =
| New_node of node_ID * node_ID * node_type * string * bool
......
......@@ -304,7 +304,9 @@ let print_notify fmt n =
begin
match nf with
| Proved b -> fprintf fmt "node change %d Proved %b" ni b
(*
| Obsolete b -> fprintf fmt "node change %d Obsolete %b" ni b
*)
| 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
......@@ -705,16 +707,15 @@ end
P.notify (Node_change (new_id, Proved (pn_proved cont pn)))
| APa pa ->
let pa = get_proof_attempt_node cont.controller_session pa in
let is_obsolete = pa.proof_obsolete in
let resource_limit = pa.limit in
begin
let obs = pa.proof_obsolete in
let limit = pa.limit in
let res =
match pa.Session_itp.proof_state with
| Some pa ->
P.notify (Node_change (
new_id, Proof_status_change
(Done pa, is_obsolete, resource_limit)))
| _ -> ()
end
| Some pa -> Done pa
| _ -> InternalFailure Not_found
in
P.notify (Node_change (new_id, Proof_status_change(res, obs, limit)))
(*
let get_info_and_type ses (node: any) =
......@@ -977,8 +978,14 @@ end
P.notify (Node_change (node_ID, Proved b));
match x with
| APa pa ->
let obs = (get_proof_attempt_node c.controller_session pa).proof_obsolete in
P.notify (Node_change (node_ID, Obsolete obs))
let pa = get_proof_attempt_node c.controller_session pa in
let res = match pa.Session_itp.proof_state with
| None -> InternalFailure Not_found
| Some r -> Done r
in
let obs = pa.proof_obsolete in
let limit = pa.limit in
P.notify (Node_change (node_ID, Proof_status_change(res, obs, limit)))
| _ -> ()
with Not_found ->
Format.eprintf "Anomaly: Itp_server.notify_change_proved@.";
......
......@@ -90,9 +90,12 @@ let convert_update u =
"proof_attempt", convert_proof_attempt pas;
"obsolete", Bool b;
"limit", convert_limit l]
(*
| Obsolete b ->
convert_record ["update_info", String "Obsolete";
"obsolete", Bool b])
"obsolete", Bool b]
*)
)
let convert_notification_constructor n =
match n with
......@@ -609,9 +612,11 @@ let parse_update j =
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
......
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