Commit ffb325bf authored by MARCHE Claude's avatar MARCHE Claude

fix several pbs with interactive provers replay and proof scripts edition

Signed-off-by: MARCHE Claude's avatarClaude Marche <Claude.Marche@inria.fr>
parent afab61c2
......@@ -1622,6 +1622,10 @@ let () =
(* complete the tools menu *)
let edit_menu_item =
create_menu_item tools_factory "Edit"
"View or edit proof script"
let replay_menu_item =
create_menu_item tools_factory "Replay obsolete"
"Replay all obsolete proofs"
......@@ -1661,6 +1665,14 @@ let () =
let id = get_node_id r#iter in
send_request (Remove_subtree id)
| _ -> print_message "Select only one node to perform this action");
connect_menu_item
edit_menu_item
~callback:(fun () ->
match get_selected_row_references () with
| [r] ->
let id = get_node_id r#iter in
send_request (Command_req (id,"edit"))
| _ -> print_message "Select only one node to perform this action");
connect_menu_item
mark_obsolete_item
~callback:(fun () ->
......
......@@ -314,9 +314,12 @@ let build_prover_call ?proof_script ~cntexample c id pr limit callback ores =
Whyconf.get_complete_command config_pr ~with_steps in
try
let task = Session_itp.get_raw_task c.controller_session id in
Debug.dprintf debug_sched "[build_prover_call] Script file = %a@."
(Pp.print_option Pp.string) proof_script;
let inplace = config_pr.Whyconf.in_place in
let call =
Driver.prove_task ?old:proof_script ~cntexample:cntexample ~inplace:false ~command
~limit (*?name_table:table*) driver task
Driver.prove_task ?old:proof_script ~cntexample:cntexample ~inplace ~command
~limit driver task
in
let pa = (c.controller_session,id,pr,proof_script,callback,false,call,ores) in
Queue.push pa prover_tasks_in_progress
......@@ -412,44 +415,41 @@ let run_timeout_handler () =
S.timeout ~ms:default_delay_ms timeout_handler;
end
let schedule_proof_attempt_r ?proof_script c id pr ~counterexmp ~limit ~callback =
let s = c.controller_session in
let adaptlimit,ores =
let schedule_proof_attempt c id pr
~counterexmp ~limit ~callback ~notification =
let ses = c.controller_session in
let callback panid s =
(match s with
| Scheduled | Running -> update_goal_node notification ses id
| Done res ->
update_proof_attempt ~obsolete:false ses id pr res;
update_goal_node notification ses id
| _ -> ());
callback panid s
in
let adaptlimit,ores,proof_script =
try
let h = get_proof_attempt_ids s id in
let h = get_proof_attempt_ids ses id in
let pa = Hprover.find h pr in
let a = get_proof_attempt_node s pa in
let a = get_proof_attempt_node ses pa in
let old_res = a.proof_state in
let config_pr,_ = Hprover.find c.controller_provers pr in
let interactive = config_pr.Whyconf.interactive in
let use_steps = Call_provers.(limit.limit_steps <> empty_limit.limit_steps) in
let limit = adapt_limits ~interactive ~use_steps limit a in
limit, old_res
with Not_found | Session_itp.BadID -> limit,None
let script = Opt.map (fun s ->
Debug.dprintf debug_sched "Script file = %s@." s;
Filename.concat (get_dir ses) s) a.proof_script
in
limit, old_res, script
with Not_found | Session_itp.BadID -> limit,None,None
in
let panid = graft_proof_attempt ~limit s id pr in
let panid = graft_proof_attempt ~limit ses id pr in
Queue.add (c,id,pr,adaptlimit,proof_script,callback panid,counterexmp,ores)
scheduled_proof_attempts;
callback panid Scheduled;
run_timeout_handler ()
let schedule_proof_attempt ?proof_script c id pr
~counterexmp ~limit ~callback ~notification =
let callback panid s =
(match s with
| Scheduled | Running -> update_goal_node notification c.controller_session id
| Done res ->
update_proof_attempt ~obsolete:false c.controller_session id pr res;
update_goal_node notification c.controller_session id
| _ -> ());
callback panid s
in
(* proof_script is specific to interactive manual provers *)
let session_dir = Session_itp.get_dir c.controller_session in
let proof_script =
Opt.map (Sysutil.absolutize_filename session_dir) proof_script
in
schedule_proof_attempt_r ?proof_script c id pr ~counterexmp ~limit ~callback
(* replay *)
......@@ -488,7 +488,7 @@ let find_prover notification c goal_id pr =
end
*)
let replay_proof_attempt ?proof_script c pr limit (parid: proofNodeID) id ~callback ~notification =
let replay_proof_attempt 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
......@@ -496,7 +496,7 @@ let replay_proof_attempt ?proof_script c pr limit (parid: proofNodeID) id ~callb
| Some pr ->
try
let _ = get_raw_task c.controller_session parid in
schedule_proof_attempt ?proof_script 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
......@@ -546,7 +546,6 @@ let update_edit_external_proof c pn ?panid pr =
in
let ch = open_out file in
let fmt = formatter_of_out_channel ch in
(* Name table is only used in ITP printing *)
Driver.print_task ~cntexample:false ?old driver fmt task;
Opt.iter close_in old;
close_out ch;
......@@ -554,13 +553,12 @@ let update_edit_external_proof c pn ?panid pr =
exception Editor_not_found
let schedule_edition c id pr ~no_edit ~do_check_proof ?file ~callback ~notification =
let schedule_edition c id pr ~callback ~notification =
Debug.dprintf debug_sched "[Sched] Scheduling an edition@.";
let config = c.controller_config in
let session = c.controller_session in
let prover_conf = Whyconf.get_prover_config config pr in
let session_dir = Session_itp.get_dir session in
let limit = Call_provers.empty_limit in
(* Make sure editor exists. Fails otherwise *)
let editor =
......@@ -575,62 +573,36 @@ let schedule_edition c id pr ~no_edit ~do_check_proof ?file ~callback ~notificat
in
let proof_attempts_id = get_proof_attempt_ids session id in
let panid =
try Some (Hprover.find proof_attempts_id pr) with
| _ -> None
try Hprover.find proof_attempts_id pr
with Not_found ->
let file = update_edit_external_proof c id pr in
let filename = Sysutil.relativize_filename session_dir file in
graft_proof_attempt c.controller_session id pr ~file:filename ~limit
in
(* make sure to actually create the file and the proof attempt *)
let panid, file =
match panid, file with
| None, None ->
let file = update_edit_external_proof c id pr in
let filename = Sysutil.relativize_filename session_dir file in
let panid = graft_proof_attempt c.controller_session id pr ~file:filename ~limit in
panid, file
| None, Some file ->
let panid = graft_proof_attempt c.controller_session id pr ~file ~limit in
let file = update_edit_external_proof c id ~panid pr in
panid, file
| Some panid, _ ->
let file = update_edit_external_proof c id ~panid pr in
panid, file
in
let pa = get_proof_attempt_node c.controller_session panid in
let file = Opt.get pa.proof_script in
(* Notification node *)
let callback panid s = callback panid s;
match s with
| Scheduled | Running -> update_goal_node notification c.controller_session id
| Done _ ->
(* TODO *)
if do_check_proof then
let file = Sysutil.relativize_filename session_dir file in
replay_proof_attempt ~proof_script:file c pr Call_provers.empty_limit id
panid ~callback ~notification
| Interrupted | InternalFailure _ ->
(* TODO *)
if do_check_proof then
let file = Sysutil.relativize_filename session_dir file in
replay_proof_attempt ~proof_script:file c pr Call_provers.empty_limit id
panid ~callback ~notification
| _ -> ()
let callback panid s =
begin
match s with
| Scheduled | Running ->
update_goal_node notification c.controller_session id
| Done _ ->
update_goal_node notification c.controller_session id
| Interrupted | InternalFailure _ -> ()
| _ -> ()
end;
callback panid s
in
Debug.dprintf debug_sched "[Editing] goal %s with command '%s' on file %s@."
(Session_itp.get_proof_name session id).Ident.id_string
editor file;
if no_edit then
begin
callback panid Running;
callback panid Interrupted
end
else
begin
let call = Call_provers.call_editor ~command:editor file in
callback panid Running;
let file = Sysutil.relativize_filename session_dir file in
Queue.add (c.controller_session,id,pr,Some file,callback panid,false,call,None)
prover_tasks_in_progress;
run_timeout_handler ()
end
let call = Call_provers.call_editor ~command:editor file in
callback panid Running;
let file = Sysutil.relativize_filename session_dir file in
Queue.add (c.controller_session,id,pr,Some file,callback panid,false,call,None)
prover_tasks_in_progress;
run_timeout_handler ()
let schedule_transformation_r c id name args ~callback =
......@@ -924,8 +896,7 @@ let replay ?(obsolete_only=true) ?(use_steps=false)
else
Call_provers.{ pa.limit with limit_steps = empty_limit.limit_steps }
in
let proof_script = pa.proof_script in
replay_proof_attempt ?proof_script c pr limit parid id
replay_proof_attempt c pr limit parid id
~callback:(fun id s ->
craft_report count s report parid pr limit pa;
callback id s;
......
......@@ -176,7 +176,6 @@ val interrupt : unit -> unit
the ones already running *)
val schedule_proof_attempt :
?proof_script:string ->
controller ->
proofNodeID ->
Whyconf.prover ->
......@@ -195,9 +194,6 @@ val schedule_edition :
controller ->
proofNodeID ->
Whyconf.prover ->
no_edit: bool ->
do_check_proof: bool ->
?file: string ->
callback:(proofAttemptID -> proof_attempt_status -> unit) ->
notification:notifier -> unit
(** [schedule_edition c id pr ~no_edit ~do_check_proof ?file ~callback
......
......@@ -100,7 +100,9 @@ type notification =
type ide_request =
| Command_req of node_ID * string
(*
| Prove_req of node_ID * prover * Call_provers.resource_limit
*)
| Transform_req of node_ID * transformation * string list
| Strategy_req of node_ID * strategy
| Edit_req of node_ID * prover
......@@ -130,7 +132,7 @@ type ide_request =
(* Return true if the request modify the session *)
let modify_session (r: ide_request) =
match r with
| Command_req _ | Prove_req _ | Transform_req _ | Strategy_req _
| Command_req _ (* | Prove_req _ *) | Transform_req _ | Strategy_req _
| Add_file_req _ | Remove_subtree _ | Copy_paste _ | Copy_detached _
| Replay_req | Clean_req | Mark_obsolete_req _ | Edit_req _ -> true
......
......@@ -106,10 +106,21 @@ type notification =
type ide_request =
| Command_req of node_ID * string
(*
| Prove_req of node_ID * prover * Call_provers.resource_limit
(** request to run the given prover on the goal of the given node
id, with the given limits. if the prover is an interactive one,
this requests for an edition of the proof script instead of
running the prover. Checking the validity of an interactive
proof must be done via a [Replay_req] request *)
*)
| Transform_req of node_ID * transformation * string list
| Strategy_req of node_ID * strategy
| Edit_req of node_ID * prover
(** Request for edition of the proof script of the proof attempt
associated to the given node id. Works also for non-interactive
provers, it simply opens an editeor on the file sent to the
prover. *)
| Add_file_req of string
| Set_max_tasks_req of int
| Get_file_contents of string
......@@ -125,7 +136,7 @@ type ide_request =
| Copy_paste of node_ID * node_ID
| Copy_detached of node_ID
| Save_file_req of string * string
(** [Save_file_req(filename, content_of_file)] save the file *)
(** [Save_file_req(filename, content_of_file)] saves the file *)
| Get_first_unproven_node of node_ID
| Mark_obsolete_req of node_ID
| Get_Session_Tree_req
......@@ -133,6 +144,11 @@ type ide_request =
| Save_req
| Reload_req
| Replay_req
(** replay all the proof attempts whose result is obsolete. TODO
[priority high]: have a similar request with a node id as
argument, to replay only in the corresponding subtree. TODO
[priority low]: have a extra boolean argument to force replay
also of non-obsolete goals. *)
| Exit_req
| Interrupt_req
......
......@@ -254,7 +254,9 @@ let get_exception_message ses id e =
let print_request fmt r =
match r with
| Command_req (_nid, s) -> fprintf fmt "command \"%s\"" s
(*
| Prove_req (_nid, prover, _rl) -> fprintf fmt "prove with %s" prover
*)
| Transform_req (_nid, tr, _args) -> fprintf fmt "transformation :%s" tr
| Strategy_req (_nid, st) -> fprintf fmt "strategy %s" st
| Edit_req (_nid, prover) -> fprintf fmt "edit with %s" prover
......@@ -341,7 +343,7 @@ end
module Make (S:Controller_itp.Scheduler) (Pr:Protocol) = struct
module C = Controller_itp.Make(S)
module C = Controller_itp.Make(S)
let debug = Debug.register_flag "itp_server" ~desc:"ITP server"
......@@ -1094,7 +1096,7 @@ end
let callback = callback_edition d.cont in
match any_from_node_ID nid with
| APn id ->
C.schedule_edition d.cont id prover ~no_edit:false ~do_check_proof:false ?file:None
C.schedule_edition d.cont id prover
~callback ~notification:(notify_change_proved d.cont)
| _ -> ()
......@@ -1223,6 +1225,11 @@ end
let () = register_command "clean" "remove unsuccessful proof attempts that are below proved goals"
(Qnotask (fun _cont _args -> clean_session (); "Cleaning done"))
(*
let () = register_command "edit" "remove unsuccessful proof attempts that are below proved goals"
(Qtask (fun cont _table _args -> schedule_editionn (); "Editor called"))
*)
(* TODO: should this remove the current selected node ?
let () = register_command
"remove_node" "removes a proof attempt or a transformation"
......@@ -1279,6 +1286,7 @@ end
let config = d.cont.controller_config in
try (
match r with
(*
| Prove_req (nid,p,limit) ->
let p = try Some (get_prover p) with
| Bad_prover_name p -> P.notify (Message (Proof_error (nid, "Bad prover name" ^ p))); None
......@@ -1289,6 +1297,7 @@ end
let counterexmp = Whyconf.cntexample (Whyconf.get_main config) in
schedule_proof_attempt ~counterexmp nid p limit
end
*)
| Transform_req (nid, t, args) -> apply_transform nid t args
| Strategy_req (nid, st) ->
let counterexmp = Whyconf.cntexample (Whyconf.get_main config) in
......
......@@ -142,7 +142,9 @@ let convert_node_type nt =
let convert_request_constructor (r: ide_request) =
match r with
| Command_req _ -> String "Command_req"
(*
| Prove_req _ -> String "Prove_req"
*)
| Transform_req _ -> String "Transform_req"
| Strategy_req _ -> String "Strategy_req"
| Edit_req _ -> String "Edit_req"
......@@ -177,11 +179,13 @@ let print_request_to_json (r: ide_request): Json_base.json =
convert_record ["ide_request", cc r;
"node_ID", Int nid;
"command", String s]
(*
| Prove_req (nid, p, l) ->
convert_record ["ide_request", cc r;
"node_ID", Int nid;
"prover", String p;
"limit", convert_limit l]
*)
| Transform_req (nid, tr, args) ->
convert_record ["ide_request", cc r;
"node_ID", Int nid;
......@@ -457,13 +461,13 @@ let parse_request (constr: string) j =
let nid = get_int (get_field j "node_ID") in
let s = get_string (get_field j "command") in
Command_req (nid, s)
(*
| "Prove_req" ->
let nid = get_int (get_field j "node_ID") in
let p = get_string (get_field j "prover") in
let l = get_field j "limit" in
Prove_req (nid, p, parse_limit_from_json l)
*)
| "Transform_req" ->
let nid = get_int (get_field j "node_ID") in
let tr = get_string (get_field j "transformation") in
......
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