Adding Edit_req

Unfinished work to retrieve manual proofs.
(minor) added a use case for stack_trace

src/session/controller_itp.ml

 open Format
 open Session_itp
 
+
+let debug_sched = Debug.register_info_flag "scheduler"
+  ~desc:"Print@ debugging@ messages@ about@ scheduling@ of@ prover@ calls@ \
+         and@ transformation@ applications."
+
 exception Noprogress
 
 let () = Exn_printer.register
@@ -568,6 +573,135 @@ let schedule_proof_attempt c id pr ~counterexmp ~limit ~callback ~notification =
   in
   schedule_proof_attempt_r c id pr ~counterexmp ~limit ~callback
 
+(* create the path to a file for saving the external proof script *)
+let create_file_rel_path c pr pn =
+  let config = c.controller_config in
+  let c_env = c.controller_env in
+  let session = c.controller_session in
+  let prover_conf = Whyconf.get_prover_config config pr in
+  let driver = prover_conf.Whyconf.driver in
+  let driver = Driver.load_driver c_env driver prover_conf.Whyconf.extra_drivers in
+  let task = Session_itp.get_task session pn in
+  let session_dir = Session_itp.get_dir session in
+  let th = get_encapsulating_theory session (APn pn) in
+  let th_name = (Session_itp.theory_name th).Ident.id_string in
+  let f = get_encapsulating_file session (ATh th) in
+  let fn = f.file_name in
+  let file = Driver.file_of_task driver fn th_name task in
+  let file = Filename.concat session_dir file in
+  let file = Sysutil.uniquify file in
+  let file = Sysutil.relativize_filename session_dir file in
+  file
+
+let update_edit_external_proof c pn ?panid pr =
+  let config = c.controller_config in
+  let c_env = c.controller_env in
+  let session = c.controller_session in
+  let prover_conf = Whyconf.get_prover_config config pr in
+  let driver = prover_conf.Whyconf.driver in
+  let driver = Driver.load_driver c_env driver prover_conf.Whyconf.extra_drivers in
+  let task = Session_itp.get_task session pn in
+  let session_dir = Session_itp.get_dir session in
+  let file =
+    match panid with
+    | None ->
+        create_file_rel_path c pr pn
+    | Some panid ->
+        let pa = get_proof_attempt_node session panid in
+        Opt.get pa.proof_script
+  in
+  let file = Filename.concat session_dir file in
+  let old =
+    if Sys.file_exists file
+    then
+      begin
+        let backup = file ^ ".bak" in
+        if Sys.file_exists backup
+        then Sys.remove backup;
+        Sys.rename file backup;
+        Some(open_in backup)
+      end
+    else None
+  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;
+  file
+
+(* TODO
+let schedule_from_spark =
+  graft_proof_attempt with file given
+  schedule_edition
+*)
+
+exception Editor_not_found
+
+let schedule_edition c id pr ?file ~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
+  (* Notification node *)
+  let callback panid s = callback panid s;
+    match s with
+    | Scheduled | Running | Done _ -> update_goal_node notification c id
+    | _ -> ()
+  in
+
+  let limit = Call_provers.empty_limit in
+  let editor =
+    match prover_conf.Whyconf.editor with
+    | "" -> None
+    | s ->
+        try
+          let ed = Whyconf.editor_by_id config s in
+          Some (String.concat " "(ed.Whyconf.editor_command ::
+                                  ed.Whyconf.editor_options))
+        with Not_found -> None
+  in
+  let proof_attempts_id = get_proof_attempt_ids session id in
+  let panid =
+    try Some (Hprover.find proof_attempts_id pr) with
+    | _ -> None
+  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
+
+  Debug.dprintf debug_sched "[Editing] goal %s with command '%s' on file %s@."
+    (Session_itp.get_proof_name session id).Ident.id_string
+    (match editor with None -> "" | Some s -> s) file;
+  match editor with
+  | None ->
+      begin
+        raise Editor_not_found
+      end
+  | Some editor ->
+      begin
+        let call = Call_provers.call_editor ~command:editor file in
+        callback panid Running;
+        Queue.add (c.controller_session,id,pr,callback panid,false,call) prover_tasks_in_progress;
+        run_timeout_handler ()
+      end;
+  ()
+
 let schedule_transformation_r c id name args ~callback =
   let apply_trans () =
     let task = get_task c.controller_session id in

src/session/controller_itp.mli

@@ -183,13 +183,27 @@ val schedule_proof_attempt :
   limit:Call_provers.resource_limit ->
   callback:(proofAttemptID -> proof_attempt_status -> unit) ->
   notification:notifier -> unit
-(** [schedule_proof_attempt s id p ~timelimit ~callback] schedules a
+(** [schedule_proof_attempt c id p ~timelimit ~callback ~notification] schedules a
    proof attempt for a goal specified by [id] with the prover [p] with
    time limit [timelimit]; the function [callback] will be called each
    time the proof attempt status changes. Typically at Scheduled, then
    Running, then Done. If there is already a proof attempt with [p] it
    is updated. *)
 
+val schedule_edition :
+  controller ->
+  proofNodeID ->
+  Whyconf.prover ->
+  ?file: string ->
+  callback:(proofAttemptID -> proof_attempt_status -> unit) ->
+  notification:notifier -> unit
+(** [schedule_edition c id pr ?file ~callback ~notification] runs
+    the editor for prover [pr] on proofnode [id] on a file automatically
+    generated in [file] (or created path). It will runs callback each time
+    the proof status changes and notification will be called each time a
+    change is made to the proof_state (in the whole proof tree of the session)
+*)
+
 val schedule_transformation :
   controller ->
   proofNodeID ->

src/session/itp_communication.ml

@@ -92,6 +92,7 @@ type ide_request =
   | 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
 (*
   | Open_session_req        of string
  *)
@@ -118,7 +119,7 @@ let modify_session (r: ide_request) =
   match r with
   | Command_req _ | Prove_req _ | Transform_req _ | Strategy_req _
   | Add_file_req _ | Remove_subtree _ | Copy_paste _ | Copy_detached _
-  | Replay_req | Clean_req | Mark_obsolete_req _ -> true
+  | Replay_req | Clean_req | Mark_obsolete_req _ | Edit_req _ -> true
 
   (*| Open_session_req _ *)
   | Set_max_tasks_req _ | Get_file_contents _

src/session/itp_communication.mli

@@ -98,6 +98,7 @@ type ide_request =
   | 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
 (*
   | Open_session_req        of string
  *)

src/session/itp_server.ml

@@ -247,6 +247,7 @@ let print_request fmt r =
   | 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
 (*
   | Open_session_req f              -> fprintf fmt "open session file %s" f
 *)
@@ -913,6 +914,34 @@ let get_locations t =
                 ~limit ~callback ~notification:(notify_change_proved d.cont))
       unproven_goals
 
+  let callback_edition cont panid pa_status =
+    let ses = cont.controller_session in
+    begin match pa_status with
+    | Running ->
+      begin
+        try
+          ignore (node_ID_from_pan panid)
+        with Not_found ->
+          let parent_id = get_proof_attempt_parent ses panid in
+          let parent = node_ID_from_pn parent_id in
+          ignore (new_node ~parent (APa panid))
+      end
+    | _  -> ()
+    end;
+    let limit = (get_proof_attempt_node cont.controller_session panid).limit in
+    let new_status = Proof_status_change (pa_status, false, limit) in
+    P.notify (Node_change (node_ID_from_pan panid, new_status))
+
+  let schedule_edition (nid: node_ID) (p: Whyconf.config_prover) =
+    let d = get_server_data () in
+    let prover = p.Whyconf.prover in
+    let callback = callback_edition d.cont in
+    match any_from_node_ID nid with
+    | APn id ->
+        C.schedule_edition d.cont id prover ?file:None
+          ~callback ~notification:(notify_change_proved d.cont)
+    | _ -> ()
+
   (* ----------------- Schedule transformation -------------------- *)
 
   (* Callback of a transformation *)
@@ -1075,6 +1104,15 @@ let get_locations t =
     | Strategy_req (nid, st)       ->
         let counterexmp = Whyconf.cntexample (Whyconf.get_main config) in
         run_strategy_on_task ~counterexmp nid st
+    | Edit_req (nid, p)            ->
+      let p = try Some (get_prover p) with
+      | Bad_prover_name p -> P.notify (Message (Proof_error (nid, "Bad prover name" ^ p))); None
+      in
+      begin match p with
+      | None -> ()
+      | Some p ->
+          schedule_edition nid p
+      end
     | Clean_req                    -> clean_session ()
     | Save_req                     -> save_session ()
     | Reload_req                   -> reload_session ()
@@ -1129,6 +1167,8 @@ let get_locations t =
         | Strategies st           ->
             let counterexmp = Whyconf.cntexample (Whyconf.get_main config) in
             run_strategy_on_task ~counterexmp nid st
+        | Edit p                  ->
+            schedule_edition nid p
         | Help_message s          -> P.notify (Message (Help s))
         | QError s                -> P.notify (Message (Query_Error (nid, s)))
         | Other (s, _args)        ->
@@ -1150,10 +1190,11 @@ let get_locations t =
     | Set_max_tasks_req i     -> C.set_max_tasks i
     | Exit_req                -> exit 0
      )
-    with e -> P.notify (Message (Error (Pp.string_of
-      (fun fmt (r,e) -> Format.fprintf fmt
-          "There was an unrecoverable error during treatment of request:\n %a\nwith exception: %a"
-    print_request r Exn_printer.exn_printer e ) (r, e))))
+    with e when not (Debug.test_flag Debug.stack_trace)->
+      P.notify (Message (Error (Pp.string_of
+          (fun fmt (r,e) -> Format.fprintf fmt
+             "There was an unrecoverable error during treatment of request:\n %a\nwith exception: %a"
+             print_request r Exn_printer.exn_printer e ) (r, e))))
 
   let treat_requests () : bool =
     List.iter treat_request (P.get_requests ());

src/session/json_util.ml

@@ -121,6 +121,7 @@ let convert_request_constructor (r: ide_request) =
   | Prove_req _               -> String "Prove_req"
   | Transform_req _           -> String "Transform_req"
   | Strategy_req _            -> String "Strategy_req"
+  | Edit_req _                -> String "Edit_req"
 (*
   | Open_session_req _        -> String "Open_session_req"
 *)
@@ -164,6 +165,10 @@ let print_request_to_json (r: ide_request): Json_base.json =
       convert_record ["ide_request", cc r;
            "node_ID", Int nid;
            "strategy", String str]
+  | Edit_req (nid, prover) ->
+      convert_record ["ide_request", cc r;
+                      "node_ID", Int nid;
+                      "prover", String prover]
 (*
   | Open_session_req f ->
       convert_record ["ide_request", cc r;
@@ -438,6 +443,10 @@ let parse_request (constr: string) j =
     let str = get_string (get_field j "strategy") in
     Strategy_req (nid, str)
 
+  | "Edit_req" ->
+    let nid = get_int (get_field j "node_ID") in
+    let p = get_string (get_field j "prover") in
+    Edit_req (nid, p)
 (*
   | "Open_session_req" ->
     let f = get_string (get_field j "file") in

src/session/server_utils.ml

@@ -283,6 +283,7 @@ type command =
   | Transform    of string * Trans.gentrans * string list
   | Prove        of Whyconf.config_prover * Call_provers.resource_limit
   | Strategies   of string
+  | Edit         of Whyconf.config_prover
   | Help_message of string
   | Query        of string
   | QError       of string
@@ -291,7 +292,10 @@ type command =
 let interp_others commands_table config cmd args =
   match parse_prover_name config cmd args with
   | Some (prover_config, limit) ->
-      Prove (prover_config, limit)
+      if prover_config.Whyconf.interactive then
+        Edit (prover_config)
+      else
+        Prove (prover_config, limit)
   | None ->
       match cmd with
       | "auto" ->

src/session/server_utils.mli

@@ -50,6 +50,7 @@ type command =
   | Transform    of string * Trans.gentrans * string list
   | Prove        of Whyconf.config_prover * Call_provers.resource_limit
   | Strategies   of string
+  | Edit         of Whyconf.config_prover
   | Help_message of string
   | Query        of string
   | QError       of string

src/session/session_itp.ml

@@ -263,6 +263,31 @@ let is_detached (s: session) (a: any) =
     let pn = get_proofNode s pn_id in
     pn.proofn_task = None
 
+let rec get_encapsulating_theory s any =
+  match any with
+  | AFile _f -> assert (false)
+  | ATh th -> th
+  | ATn tn ->
+      let pn_id = get_trans_parent s tn in
+      get_encapsulating_theory s (APn pn_id)
+  | APn pn ->
+      (match get_proof_parent s pn with
+      | Theory th -> th
+      | Trans tn -> get_encapsulating_theory s (ATn tn)
+      )
+  | APa pa ->
+      let pn = get_proof_attempt_parent s pa in
+      get_encapsulating_theory s (APn pn)
+
+let get_encapsulating_file s any =
+  match any with
+  | AFile f -> f
+  | ATh th -> theory_parent s th
+  | _ ->
+      let th = get_encapsulating_theory s any in
+      theory_parent s th
+
+
 (* Remove elements of the session tree *)
 
 let remove_transformation (s : session) (id : transID) =
@@ -528,17 +553,20 @@ let add_proof_attempt session prover limit state obsolete edit parentID =
     Hint.replace session.proofAttempt_table id pa;
     id
 
-let graft_proof_attempt (s : session) (id : proofNodeID) (pr : Whyconf.prover)
+let graft_proof_attempt ?file (s : session) (id : proofNodeID) (pr : Whyconf.prover)
     ~limit =
   let pn = get_proofNode s id in
   try
     let id = Hprover.find pn.proofn_attempts pr in
     let pa = Hint.find s.proofAttempt_table id in
-    let pa = { pa with limit = limit; proof_state = None; proof_obsolete = false } in
+    let pa = { pa with limit = limit;
+               proof_state = None;
+               proof_obsolete = false;
+               proof_script = file } in
     Hint.replace s.proofAttempt_table id pa;
     id
   with Not_found ->
-    add_proof_attempt s pr limit None false None id
+    add_proof_attempt s pr limit None false file id
 
 
 (* [mk_proof_node s n t p id] register in the session [s] a proof node
@@ -1480,6 +1508,11 @@ let save_prover fmt id (p,mostfrequent_timelimit,mostfrequent_steplimit,mostfreq
     (opt pp_print_int "steplimit") steplimit
     mostfrequent_memlimit
 
+let save_option_def name fmt opt =
+  match opt with
+  | None -> ()
+  | Some s -> fprintf fmt "@ %s=\"%s\"" name s
+
 let save_bool_def name def fmt b =
   if b <> def then fprintf fmt "@ %s=\"%b\"" name b
 
@@ -1512,12 +1545,13 @@ let save_status fmt s =
 
 let save_proof_attempt fmt ((id,tl,sl,ml),a) =
   fprintf fmt
-    "@\n@[<h><proof@ prover=\"%i\"%a%a%a%a>"
+    "@\n@[<h><proof@ prover=\"%i\"%a%a%a%a%a>"
     id
     (save_int_def "timelimit" tl) (a.limit.Call_provers.limit_time)
     (save_int_def "steplimit" sl) (a.limit.Call_provers.limit_steps)
     (save_int_def "memlimit" ml) (a.limit.Call_provers.limit_mem)
-    (save_bool_def "obsolete" false) a.proof_obsolete;
+    (save_bool_def "obsolete" false) a.proof_obsolete
+    (save_option_def "proof_script") a.proof_script;
   save_status fmt a.proof_state;
   fprintf fmt "</proof>@]"
 

src/session/session_itp.mli

@@ -97,6 +97,11 @@ val get_any_parent: session -> any -> any option
 (* Answers true if a node is in a detached subtree *)
 val is_detached: session -> any -> bool
 
+(* get the parent theory/file of a proof node *)
+val get_encapsulating_theory: session -> any -> theory
+val get_encapsulating_file: session -> any -> file
+
+
 exception BadCopyDetached of string
 
 (** [copy s pn] copy pn and add the copy as detached subgoal of its parent *)
@@ -127,13 +132,16 @@ val merge_file_section :
     proof_attempts and transformations to the goals of the new
     theory *)
 
-val graft_proof_attempt : session -> proofNodeID -> Whyconf.prover ->
-  limit:Call_provers.resource_limit -> proofAttemptID
-(** [graft_proof_attempt s id pr l] adds a proof attempt with prover
+val graft_proof_attempt : ?file:string -> session -> proofNodeID ->
+  Whyconf.prover -> limit:Call_provers.resource_limit -> proofAttemptID
+(** [graft_proof_attempt s id pr file l] adds a proof attempt with prover
     [pr] and limits [l] in the session [s] as a child of the task
     [id]. If there already a proof attempt with the same prover, it
     updates it with the limits. It returns the id of the
-    generated proof attempt. *)
+    generated proof attempt.
+    For manual proofs, it has the same behaviour except that it adds a
+    proof_script field equal to [file].
+*)
 
 val update_proof_attempt : session -> proofNodeID -> Whyconf.prover ->
   Call_provers.prover_result -> unit