Commit 5a879904 authored by MARCHE Claude's avatar MARCHE Claude

adding new case Undone for pa status. But it does not solve the pb:

interrupted proofs are still impossible to remove.
The pb is that the session does not store the "dynamic" state of the
running session, so it is not possible to check whether a given proof
attempt is in progress or not. The controller should have its own table
to check whether a proofattemptId has a proof in progress or not.
parent 4a86dba9
......@@ -510,10 +510,12 @@ let print_namespace fmt name th =
(* print task under the form of a sequent, with only local context, for the IDE *)
(*
let print_goal fmt d =
match d.d_node with
| Dprop (Pgoal,_pr,f) -> fprintf fmt "@[%a@]@\n" print_term f
| _ -> assert false
*)
let print_sequent fmt task =
let ut = Task.used_symbols (Task.used_theories task) in
......
......@@ -1131,6 +1131,8 @@ let on_selected_row r =
(match pa with
| Controller_itp.Done pr ->
task_view#source_buffer#set_text pr.Call_provers.pr_output
| Controller_itp.Undone ->
task_view#source_buffer#set_text "Undone"
| Controller_itp.Detached ->
task_view#source_buffer#set_text "Detached"
| Controller_itp.Interrupted ->
......@@ -1368,6 +1370,7 @@ let if_selected_alone id f =
let image_of_pa_status ~obsolete pa =
match pa with
| Controller_itp.Undone
| Controller_itp.Interrupted -> !image_undone
| Controller_itp.Scheduled -> !image_scheduled
| Controller_itp.Running -> !image_running
......@@ -1462,6 +1465,7 @@ let set_status_and_time_column ?limit row =
s
| C.InternalFailure _ -> "(internal failure)"
| C.Interrupted -> "(interrupted)"
| C.Undone -> "(undone)"
| C.Uninstalled _ -> "(uninstalled prover)"
| C.Scheduled -> "(scheduled)"
| C.Running -> "(running)"
......
......@@ -31,22 +31,24 @@ let () = Exn_printer.register
(** State of a proof *)
type proof_attempt_status =
| Detached (** parent goal has no task, is detached *)
| Interrupted (** external proof has never completed *)
| Undone (** prover was never called *)
| Scheduled (** external proof attempt is scheduled *)
| Running (** external proof attempt is in progress *)
| Done of Call_provers.prover_result (** external proof done *)
| Interrupted (** external proof has never completed *)
| Detached (** parent goal has no task, is detached *)
| InternalFailure of exn (** external proof aborted by internal error *)
| Uninstalled of Whyconf.prover (** prover is uninstalled *)
let print_status fmt st =
match st with
| Detached -> fprintf fmt "Detached"
| Interrupted -> fprintf fmt "Interrupted"
| Undone -> fprintf fmt "Undone"
| Scheduled -> fprintf fmt "Scheduled"
| Running -> fprintf fmt "Running"
| Done r ->
fprintf fmt "Done(%a)" Call_provers.print_prover_result r
| Interrupted -> fprintf fmt "Interrupted"
| Detached -> fprintf fmt "Detached"
| InternalFailure e ->
fprintf fmt "InternalFailure(%a)" Exn_printer.exn_printer e
| Uninstalled pr ->
......@@ -463,12 +465,17 @@ let schedule_proof_attempt c id pr
~counterexmp ~limit ~callback ~notification =
let ses = c.controller_session in
let callback panid s =
(match s with
begin match s with
| Scheduled | Running -> update_goal_node notification ses id
| Done res ->
update_proof_attempt ~obsolete:false notification ses id pr res;
update_goal_node notification ses id
| _ -> ());
| Detached
| InternalFailure _
| Uninstalled _
| Undone -> assert false
| Interrupted -> ()
end;
callback panid s
in
let adaptlimit,ores,proof_script =
......@@ -639,6 +646,7 @@ let schedule_edition c id pr ~callback ~notification =
let callback panid s =
begin
match s with
| Running -> ()
| Done res ->
(* set obsolete to true since we do not know if the manual
proof was completed or not *)
......@@ -647,9 +655,10 @@ let schedule_edition c id pr ~callback ~notification =
print_proofAttemptID panid print_proofNodeID id;
update_proof_attempt ~obsolete:true notification session id pr res;
update_goal_node notification session id
| Scheduled | Running -> ()
| Interrupted | InternalFailure _ -> ()
| _ -> ()
| Interrupted
| InternalFailure _ ->
update_goal_node notification session id
| Undone | Detached | Uninstalled _ | Scheduled -> assert false
end;
callback panid s
in
......@@ -664,7 +673,15 @@ let schedule_edition c id pr ~callback ~notification =
(*** { 2 transformations} *)
let schedule_transformation_r c id name args ~callback =
let schedule_transformation c id name args ~callback ~notification =
let callback s =
begin match s with
| TSdone tid -> update_trans_node notification c.controller_session tid
| TSscheduled
| TSfailed _ -> ()
end;
callback s
in
let apply_trans () =
begin
try
......@@ -689,16 +706,6 @@ let schedule_transformation_r c id name args ~callback =
S.idle ~prio:0 apply_trans;
callback TSscheduled
let schedule_transformation c id name args ~callback ~notification =
let callback s =
begin match s with
| TSdone tid -> update_trans_node notification c.controller_session tid
| TSfailed _e -> ()
| _ -> ()
end;
callback s
in
schedule_transformation_r c id name args ~callback
open Strategy
......@@ -724,7 +731,7 @@ let run_strategy_on_goal
callback (STSgoto (g,pc+1));
let run_next () = exec_strategy (pc+1) strat g; false in
S.idle ~prio:0 run_next
| Detached | Uninstalled _ ->
| Undone | Detached | Uninstalled _ ->
(* should not happen *)
assert false
in
......@@ -918,7 +925,7 @@ let replay ?(obsolete_only=true) ?(use_steps=false)
let craft_report count s r id pr limits pa =
match s with
| Scheduled | Running -> ()
| Interrupted ->
| Undone | Interrupted ->
decr count;
r := (id, pr, limits, Replay_interrupted ) :: !r
| Done new_r ->
......@@ -1037,7 +1044,7 @@ let bisect_proof_attempt ~callback_tr ~callback_pa ~notification ~removed c pa_i
begin match st with
| Scheduled | Running -> ()
| Detached | Uninstalled _ -> assert false
| Interrupted -> Debug.dprintf debug "Bisecting interrupted.@."
| Undone | Interrupted -> Debug.dprintf debug "Bisecting interrupted.@."
| InternalFailure exn ->
(* Perhaps the test can be considered false in this case? *)
Debug.dprintf debug "Bisecting interrupted by an error %a.@."
......@@ -1105,7 +1112,7 @@ later on. We do has if proof fails. *)
debug "[Bisect] prover on subtask is running@.";
| Detached
| Uninstalled _ -> assert false
| Interrupted -> Debug.dprintf debug "Bisecting interrupted.@."
| Undone | Interrupted -> Debug.dprintf debug "Bisecting interrupted.@."
| InternalFailure exn ->
(* Perhaps the test can be considered false in this case? *)
Debug.dprintf debug "[Bisect] prover interrupted by an error: %a.@."
......
......@@ -17,17 +17,14 @@ open Session_itp
(** {2 State of a proof or transformation in progress} *)
type proof_attempt_status =
(*
| Unedited (** editor not yet run for interactive proof *)
| JustEdited (** edited but not run yet *)
*)
| Undone (** prover was never called *)
| Scheduled (** external proof attempt is scheduled *)
| Running (** external proof attempt is in progress *)
| Done of Call_provers.prover_result (** external proof done *)
| Interrupted (** external proof has never completed *)
| Detached (** parent goal has no task, is detached *)
| Interrupted (** external proof has never completed *)
| Scheduled (** external proof attempt is scheduled *)
| Running (** external proof attempt is in progress *)
| Done of Call_provers.prover_result (** external proof done *)
| InternalFailure of exn (** external proof aborted by internal error *)
| Uninstalled of Whyconf.prover (** prover is uninstalled *)
| InternalFailure of exn (** external proof aborted by internal error *)
| Uninstalled of Whyconf.prover (** prover is uninstalled *)
val print_status : Format.formatter -> proof_attempt_status -> unit
......
......@@ -730,7 +730,7 @@ end
let res =
match pa.Session_itp.proof_state with
| Some pa -> Done pa
| _ -> InternalFailure Not_found
| _ -> Undone
in
P.notify (Node_change (new_id, Proof_status_change(res, obs, limit)))
......@@ -1043,7 +1043,7 @@ end
| APa pa ->
let pa = get_proof_attempt_node c.controller_session pa in
let res = match pa.Session_itp.proof_state with
| None -> InternalFailure Not_found
| None -> Undone
| Some r -> Done r
in
let obs = pa.proof_obsolete in
......
......@@ -76,6 +76,8 @@ let convert_proof_result (pr: prover_result) =
let convert_proof_attempt (pas: proof_attempt_status) =
Record (match pas with
| Undone ->
convert_record ["proof_attempt", String "Undone"]
| Interrupted ->
convert_record ["proof_attempt", String "Interrupted"]
| Scheduled ->
......@@ -547,6 +549,7 @@ exception NotProofAttempt
let parse_proof_attempt j =
let s = get_string (get_field j "proof_attempt") in
match s with
| "Undone" -> Undone
| "Detached" -> Detached
| "Interrupted" -> Interrupted
| "Scheduled" -> Scheduled
......
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