new uninstalled prover policy is now taken into account in the next replay

There is no need to exit and restart IDE anymore

src/driver/whyconf.ml

@@ -119,6 +119,14 @@ type prover_upgrade_policy =
   | CPU_upgrade of prover
   | CPU_duplicate of prover
 
+let print_prover_upgrade_policy fmt p =
+  match p with
+  | CPU_keep -> Format.fprintf fmt "keep"
+  | CPU_upgrade p -> Format.fprintf fmt "upgrade to %a" print_prover p
+  | CPU_duplicate p -> Format.fprintf fmt "copy to %a" print_prover p
+
+
+
 type config_prover = {
   prover  : prover;
   command : string;

src/driver/whyconf.mli

@@ -174,6 +174,8 @@ type prover_upgrade_policy =
   | CPU_upgrade of prover
   | CPU_duplicate of prover
 
+val print_prover_upgrade_policy : Format.formatter -> prover_upgrade_policy -> unit
+
 val set_prover_upgrade_policy :
   config -> prover -> prover_upgrade_policy -> config
 (** [set_prover_upgrade c p cpu] sets or updates the policy to follow if the

src/ide/gconfig.ml

@@ -1005,7 +1005,7 @@ let alternatives_frame c (notebook:GPack.notebook) =
   in
   let remove button p () =
     button#destroy ();
-    c.config <- set_policies c.config (Mprover.remove p (get_policies c.config))
+    c.config <- set_policies c.config (Mprover.remove p (get_policies c.config));
   in
   let iter p policy =
     let label =
@@ -1170,7 +1170,7 @@ let run_auto_detection gconfig =
 
 (*let () = Debug.dprintf debug "[config] end of configuration initialization@."*)
 
-let uninstalled_prover_dialog c unknown =
+let uninstalled_prover_dialog ~callback c unknown =
   let others,names,versions =
     Whyconf.unknown_to_known_provers
       (Whyconf.get_provers c.config) unknown
@@ -1194,13 +1194,26 @@ let uninstalled_prover_dialog c unknown =
     (* header *)
     let hb = GPack.hbox ~packing:vbox#add () in
     let _ = GMisc.image ~stock:`DIALOG_WARNING ~packing:hb#add () in
-    let _ =
+    let (_:GMisc.label) =
       let text =
         Pp.sprintf "The prover %a is not installed"
-          Whyconf.print_prover unknown
+                   Whyconf.print_prover unknown
       in
       GMisc.label ~ypad:20 ~text ~xalign:0.5 ~packing:hb#add ()
     in
+    let (_:GMisc.label) =
+      let text =
+        "WARNING: this policy will not be taken into account immediately \
+         but only if you replay again the proofs."
+      in
+      GMisc.label ~text ~line_wrap:true ~packing:vbox#add ()
+    in
+    let (_:GMisc.label) =
+      let text =
+        "WARNING: do not forget to save preferences to keep this policy in future sessions"
+      in
+      GMisc.label ~text ~line_wrap:true ~packing:vbox#add ()
+    in
     (* choices *)
     let vbox_pack =
       vbox#pack ~fill:true ~expand:true ?from:None ?padding:None
@@ -1277,6 +1290,7 @@ let uninstalled_prover_dialog c unknown =
         | _ -> assert false
     in
     c.config <- set_prover_upgrade_policy c.config unknown policy;
+    let () = callback unknown policy in
     ()
 
 

src/ide/gconfig.mli

@@ -116,6 +116,7 @@ val show_about_window : unit -> unit
 val preferences : t -> unit
 
 val uninstalled_prover_dialog :
+  callback: (Whyconf.prover -> Whyconf.prover_upgrade_policy -> unit) ->
   t -> Whyconf.prover -> unit
 
 

src/ide/why3ide.ml

@@ -2186,9 +2186,13 @@ let check_uninstalled_prover =
   let uninstalled_prover_seen = Whyconf.Hprover.create 3 in
   fun p ->
   if not (Whyconf.Hprover.mem uninstalled_prover_seen p)
-  then begin
+  then
+    begin
       Whyconf.Hprover.add uninstalled_prover_seen p ();
-      uninstalled_prover_dialog gconfig p
+      let callback p u =
+        send_request (Set_prover_policy(p,u))
+      in
+      uninstalled_prover_dialog ~callback gconfig p
     end
 
 let treat_notification n =

src/session/controller_itp.ml

@@ -78,7 +78,7 @@ let print_strategy_status fmt st =
 
 type controller =
   { mutable controller_session: Session_itp.session;
-    controller_config : Whyconf.config;
+    mutable controller_config : Whyconf.config;
     mutable controller_env: Env.env;
     controller_provers:
       (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
@@ -92,6 +92,9 @@ let set_session_max_tasks n =
   session_max_tasks := n;
   Prove_client.set_max_running_provers n
 
+let set_session_prover_upgrade_policy c p u =
+  c.controller_config <- Whyconf.set_prover_upgrade_policy c.controller_config p u
+
 let load_drivers c =
   let env = c.controller_env in
   let config = c.controller_config in

src/session/controller_itp.mli

@@ -85,7 +85,7 @@ end
 
 type controller = private
   { mutable controller_session : Session_itp.session;
-    controller_config : Whyconf.config;
+    mutable controller_config : Whyconf.config;
     mutable controller_env : Env.env;
     controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
     controller_strategies : (string * string * string * Strategy.instruction array) Wstdlib.Hstr.t;
@@ -101,6 +101,9 @@ val set_session_max_tasks : int -> unit
 (** sets the maximum number of proof tasks that can be running at the
     same time. Initially set to 1. *)
 
+val set_session_prover_upgrade_policy :
+  controller -> Whyconf.prover -> Whyconf.prover_upgrade_policy -> unit
+
 
 val print_session : Format.formatter -> controller -> unit
 

src/session/itp_communication.ml

@@ -10,7 +10,6 @@
 (********************************************************************)
 
 (* Information that the IDE may want to have *)
-type prover = string
 type transformation = (string * string)
 type strategy = string
 
@@ -109,6 +108,7 @@ type ide_request =
   | Command_req             of node_ID * string
   | Add_file_req            of string
   | Set_config_param        of string * int
+  | Set_prover_policy       of Whyconf.prover * Whyconf.prover_upgrade_policy
   | Get_file_contents       of string
   | Get_task                of node_ID * bool * bool
   | Remove_subtree          of node_ID
@@ -127,7 +127,7 @@ let modify_session (r: ide_request) =
   | Command_req _ | Add_file_req _ | Remove_subtree _ | Copy_paste _
   | Reload_req -> true
 
-  | Set_config_param _ | Get_file_contents _
+  | Set_config_param _ | Set_prover_policy _ | Get_file_contents _
   | Get_task _ | Save_file_req _ | Get_first_unproven_node _
   | Save_req | Exit_req | Get_global_infos
   | Interrupt_req -> false
@@ -142,6 +142,9 @@ let print_request fmt r =
   | Command_req (_nid, s)           -> fprintf fmt "command \"%s\"" s
   | Add_file_req f                  -> fprintf fmt "open file %s" f
   | Set_config_param(s,i)           -> fprintf fmt "set config param %s %i" s i
+  | Set_prover_policy(p1,p2)        ->
+     fprintf fmt "set prover policy %a -> %a" Whyconf.print_prover p1
+             Whyconf.print_prover_upgrade_policy p2
   | Get_file_contents _f            -> fprintf fmt "get file contents"
   | Get_first_unproven_node _nid    -> fprintf fmt "get first unproven node"
   | Get_task(nid,b,loc)           -> fprintf fmt "get task(%d,%b,%b)" nid b loc

src/session/itp_communication.mli

@@ -9,7 +9,7 @@
 (*                                                                  *)
 (********************************************************************)
 
-type prover = string
+
 (* Name and description *)
 type transformation = (string * string)
 type strategy = string
@@ -121,6 +121,7 @@ type ide_request =
      provers, applying transformations, stategies.  *)
   | Add_file_req            of string
   | Set_config_param        of string * int
+  | Set_prover_policy       of Whyconf.prover * Whyconf.prover_upgrade_policy
   | Get_file_contents       of string
   | Get_task                of node_ID * bool * bool
   (** [Get_task(id,b,loc)] requests for the text of the task in node

src/session/itp_server.ml

@@ -1296,8 +1296,8 @@ end
    let request_is_valid r =
      match r with
      | Save_req | Reload_req | Get_file_contents _ | Save_file_req _
-     | Interrupt_req | Add_file_req _ | Set_config_param _ | Exit_req
-     | Get_global_infos -> true
+     | Interrupt_req | Add_file_req _ | Set_config_param _ | Set_prover_policy _
+     | Exit_req | Get_global_infos -> true
      | Get_first_unproven_node ni ->
          Hint.mem model_any ni
      | Remove_subtree nid ->
@@ -1417,6 +1417,9 @@ end
          | "memlimit" -> Server_utils.set_session_memlimit i
          | _ -> P.notify (Message (Error ("Unknown config parameter "^s)))
        end
+    | Set_prover_policy(p,u)   ->
+       let c = d.cont in
+       Controller_itp.set_session_prover_upgrade_policy c p u
     | Exit_req                -> exit 0
      )
     with

src/session/json_util.ml

@@ -16,11 +16,13 @@ open Json_base
 
 (* TODO match exceptions and complete some cases *)
 
-let convert_prover_to_json (p: Whyconf.prover) =
-  Record (convert_record
-    ["prover_name", String p.Whyconf.prover_name;
-     "prover_version", String p.Whyconf.prover_version;
-     "prover_altern", String p.Whyconf.prover_altern])
+let convert_prover (prefix:string) (p: Whyconf.prover) =
+  [prefix ^ "name", String p.Whyconf.prover_name;
+   prefix ^ "version", String p.Whyconf.prover_version;
+   prefix ^ "altern", String p.Whyconf.prover_altern]
+let convert_prover_to_json (prefix:string) (p: Whyconf.prover) =
+
+  Record (convert_record (convert_prover prefix p))
 
 let convert_infos (i: global_information) =
   let convert_prover (s,h,p) =
@@ -101,10 +103,10 @@ 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]
+                      "prover", convert_prover_to_json "prover_" p]
   | UpgradeProver p ->
       convert_record ["proof_attempt", String "UpgradeProver";
-                      "prover", convert_prover_to_json p])
+                      "prover", convert_prover_to_json "prover_" p])
 
 let convert_update u =
   Record (match u with
@@ -154,6 +156,7 @@ let convert_request_constructor (r: ide_request) =
   | Add_file_req _            -> String "Add_file_req"
   | Save_file_req _           -> String "Save_file_req"
   | Set_config_param _        -> String "Set_config_param"
+  | Set_prover_policy _       -> String "Set_prover_policy"
   | Get_file_contents _       -> String "Get_file_contents"
   | Get_task _                -> String "Get_task"
   | Remove_subtree _          -> String "Remove_subtree"
@@ -165,6 +168,16 @@ let convert_request_constructor (r: ide_request) =
   | Interrupt_req             -> String "Interrupt_req"
   | Get_global_infos          -> String "Get_global_infos"
 
+open Whyconf
+
+let convert_policy u =
+  match u with
+  | CPU_keep -> ["policy", String "keep"]
+  | CPU_upgrade p ->
+     ["policy", String "upgrade"] @ convert_prover "target_" p
+  | CPU_duplicate p ->
+     ["policy", String "duplicate"] @ convert_prover "target_" p
+
 let print_request_to_json (r: ide_request): Json_base.json =
   let cc = convert_request_constructor in
   Record (
@@ -182,6 +195,9 @@ let print_request_to_json (r: ide_request): Json_base.json =
   | Set_config_param(s,n) ->
       convert_record ["ide_request", cc r;
            "param", String s; "value", Int n]
+  | Set_prover_policy(p,u) ->
+     convert_record (["ide_request", cc r] @
+                       convert_prover "" p @ convert_policy u)
   | Get_task(n,b,loc) ->
       convert_record ["ide_request", cc r;
            "node_ID", Int n; "full_context", Bool b ; "loc", Bool loc]
@@ -394,11 +410,11 @@ let print_list_request fmt (rl: ide_request list) =
 
 exception NotProver
 
-let parse_prover_from_json (j: json) =
+let parse_prover_from_json (prefix:string) (j: json) =
   try
-    let pn = get_string (get_field j "prover_name") in
-    let pv = get_string (get_field j "prover_version") in
-    let pa = get_string (get_field j "prover_altern") in
+    let pn = get_string (get_field j (prefix ^ "name")) in
+    let pv = get_string (get_field j (prefix ^ "version")) in
+    let pa = get_string (get_field j (prefix ^ "altern")) in
     {Whyconf.prover_name = pn; prover_version = pv; prover_altern = pa}
   with Not_found -> raise NotProver
 
@@ -434,6 +450,21 @@ let parse_request (constr: string) j =
     let n = get_int (get_field j "value") in
     Set_config_param(s,n)
 
+  | "Set_prover_policy" ->
+    let p = parse_prover_from_json "" j in
+    let u = get_string (get_field j "policy") in
+    begin match u with
+          | "keep" -> Set_prover_policy(p,CPU_keep)
+          | "upgrade" ->
+             let p' = parse_prover_from_json "target_" j in
+             Set_prover_policy(p,CPU_upgrade p')
+          | "duplicate" ->
+             let p' = parse_prover_from_json "target_" j in
+             Set_prover_policy(p,CPU_duplicate p')
+          | _ -> raise (NotRequest "")
+    end
+
+
   | "Get_task" ->
     let n = get_int (get_field j "node_ID") in
     let b = get_bool_opt (get_field j "full_context") false in
@@ -554,10 +585,10 @@ let parse_proof_attempt j =
     raise NotProofAttempt (* TODO *)
   | "Uninstalled" ->
     let p = get_field j "prover" in
-    Uninstalled (parse_prover_from_json p)
+    Uninstalled (parse_prover_from_json "prover_" p)
   | "UpgradeProver" ->
     let p = get_field j "prover" in
-    UpgradeProver (parse_prover_from_json p)
+    UpgradeProver (parse_prover_from_json "prover_" p)
   | _ -> raise NotProofAttempt
 
 exception NotUpdate