Specific server request Set_max_tasks replaced with generic Set_config_param

Time limit and mem limit set in IDE are now effective immediately

src/ide/why3ide.ml

@@ -489,6 +489,14 @@ let provers_factory =
 
 (* File menu signals *)
 
+let send_session_config_to_server () =
+  let nb = gconfig.session_nb_processes in
+  send_request (Set_config_param("max_tasks",nb));
+  let nb = gconfig.session_time_limit in
+  send_request (Set_config_param("timelimit",nb));
+  let nb = gconfig.session_mem_limit in
+  send_request (Set_config_param("memlimit",nb))
+
 let () =
   let callback () =
     Gconfig.preferences gconfig;
@@ -509,8 +517,7 @@ let () =
         (Whyconf.get_provers gconfig.config);
      *)
      *)
-    let nb = gconfig.session_nb_processes in
-    send_request (Set_max_tasks_req nb)
+    send_session_config_to_server ()
   in
   connect_menu_item menu_preferences ~callback
 
@@ -963,10 +970,7 @@ let _ =
       | _ -> false
       )
 
-let () =
-  let n = gconfig.session_nb_processes in
-  Debug.dprintf debug "setting max proof tasks to %d@." n;
-  send_request (Set_max_tasks_req n)
+let () = send_session_config_to_server ()
 
 (********************)
 (* Locations colors *)

src/session/controller_itp.ml

@@ -82,6 +82,11 @@ type controller =
     controller_running_proof_attempts : unit Hpan.t;
   }
 
+let session_max_tasks = ref 1
+
+let set_session_max_tasks n =
+  session_max_tasks := n;
+  Prove_client.set_max_running_provers n
 
 let create_controller config env ses =
   let c =
@@ -253,11 +258,6 @@ let prover_tasks_edited = Queue.create ()
 
 let timeout_handler_running = ref false
 
-let max_number_of_running_provers = ref 1
-
-let set_max_tasks n =
-  max_number_of_running_provers := n;
-  Prove_client.set_max_running_provers n
 
 let number_of_running_provers = ref 0
 
@@ -439,7 +439,7 @@ let timeout_handler () =
   begin
     try
       for _i = Hashtbl.length prover_tasks_in_progress
-          to S.multiplier * !max_number_of_running_provers do
+          to S.multiplier * !session_max_tasks do
         let (c,id,pr,limit,proof_script,callback,cntexample,ores) =
           Queue.pop scheduled_proof_attempts in
         try

src/session/controller_itp.mli

@@ -95,10 +95,17 @@ val create_controller: Whyconf.config -> Env.env -> Session_itp.session -> contr
 (** creates a controller for the given session.
     The config and env is used to load the drivers for the provers. *)
 
+
+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 print_session : Format.formatter -> controller -> unit
 
 
 
+
 val reload_files : controller -> use_shapes:bool -> bool * bool
 (** reload the files of the given session:
 
@@ -168,10 +175,6 @@ val get_undetached_children_no_pa: Session_itp.session -> any -> any list
 
 module Make(S : Scheduler) : sig
 
-val set_max_tasks : int -> unit
-(** sets the maximum number of proof tasks that can be running at the
-    same time. Initially set to 1. *)
-
 val register_observer : (int -> int -> int -> unit) -> unit
 (** records a hook that will be called with the number of waiting
     tasks, scheduled tasks, and running tasks, each time these numbers

src/session/itp_communication.ml

@@ -102,7 +102,7 @@ type notification =
 type ide_request =
   | Command_req             of node_ID * string
   | Add_file_req            of string
-  | Set_max_tasks_req       of int
+  | Set_config_param        of string * int
   | Get_file_contents       of string
   | Get_task                of node_ID * bool * bool
   | Focus_req               of node_ID
@@ -126,7 +126,7 @@ let modify_session (r: ide_request) =
   match r with
   | Command_req _ | Add_file_req _ | Remove_subtree _ | Copy_paste _
   | Copy_detached _ | Replay_req | Clean_req | Mark_obsolete_req _ -> true
-  | Set_max_tasks_req _ | Get_file_contents _
+  | Set_config_param _ | Get_file_contents _
   | Get_task _ | Save_file_req _ | Get_first_unproven_node _
   | Get_Session_Tree_req | Save_req | Reload_req | Exit_req
   | Interrupt_req | Focus_req _ | Unfocus_req -> false

src/session/itp_communication.mli

@@ -111,7 +111,7 @@ type ide_request =
      interpreted by Server_utils.interp. This includes calling
      provers, applying transformations, stategies.  *)
   | Add_file_req            of string
-  | Set_max_tasks_req       of int
+  | Set_config_param        of string * int
   | 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 [id],

src/session/itp_server.ml

@@ -253,7 +253,7 @@ let print_request fmt r =
   match r with
   | Command_req (_nid, s)           -> fprintf fmt "command \"%s\"" s
   | Add_file_req f                  -> fprintf fmt "open file %s" f
-  | Set_max_tasks_req i             -> fprintf fmt "set max tasks %i" i
+  | Set_config_param(s,i)           -> fprintf fmt "set config param %s %i" s i
   | 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
@@ -1367,7 +1367,14 @@ end
         else
           () (* Eventually print debug here *)
 *)
-    | Set_max_tasks_req i     -> C.set_max_tasks i
+    | Set_config_param(s,i)   ->
+       begin
+         match s with
+         | "max_tasks" -> Controller_itp.set_session_max_tasks i
+         | "timelimit" -> Server_utils.set_session_timelimit i
+         | "memlimit" -> Server_utils.set_session_memlimit i
+         | _ -> P.notify (Message (Error ("Unknown config parameter "^s)))
+       end
     | Exit_req                -> exit 0
      )
     with e when not (Debug.test_flag Debug.stack_trace)->

src/session/json_util.ml

@@ -143,7 +143,7 @@ let convert_request_constructor (r: ide_request) =
   | Command_req _             -> String "Command_req"
   | Add_file_req _            -> String "Add_file_req"
   | Save_file_req _           -> String "Save_file_req"
-  | Set_max_tasks_req _       -> String "Set_max_tasks_req"
+  | Set_config_param _        -> String "Set_config_param"
   | Get_file_contents _       -> String "Get_file_contents"
   | Focus_req _               -> String "Focus_req"
   | Unfocus_req               -> String "Unfocus_req"
@@ -175,9 +175,9 @@ let print_request_to_json (r: ide_request): Json_base.json =
   | Save_file_req (f,_) ->
       convert_record ["ide_request", cc r;
            "file", String f]
-  | Set_max_tasks_req n ->
+  | Set_config_param(s,n) ->
       convert_record ["ide_request", cc r;
-           "tasks", Int n]
+           "param", String s; "value", Int n]
   | Get_task(n,b,loc) ->
       convert_record ["ide_request", cc r;
            "node_ID", Int n; "do_intros", Bool b; "loc", Bool loc]
@@ -441,9 +441,10 @@ let parse_request (constr: string) j =
     let f = get_string (get_field j "file") in
     Add_file_req f
 
-  | "Set_max_tasks_req" ->
-    let n = get_int (get_field j "tasks") in
-    Set_max_tasks_req n
+  | "Set_config_param" ->
+    let s = get_string (get_field j "param") in
+    let n = get_int (get_field j "value") in
+    Set_config_param(s,n)
 
   | "Get_task" ->
     let n = get_int (get_field j "node_ID") in

src/session/server_utils.ml

@@ -281,11 +281,16 @@ let return_prover name config =
   end else
     Some (snd (Whyconf.Mprover.choose provers))
 
+let session_timelimit = ref 2
+let session_memlimit = ref 1000
+let set_session_timelimit n = session_timelimit := n
+let set_session_memlimit n = session_memlimit := n
+
+
 (* Parses the Other command. If it fails to parse it, it answers None otherwise
    it returns the config of the prover together with the ressource_limit *)
 let parse_prover_name config name args :
   (Whyconf.config_prover * Call_provers.resource_limit) option =
-  let main = Whyconf.get_main config in
   match (return_prover name config) with
   | None -> None
   | Some prover_config ->
@@ -294,12 +299,13 @@ let parse_prover_name config name args :
       match args with
       | [] ->
         let default_limit = Call_provers.{empty_limit with
-                                          limit_time = Whyconf.timelimit main;
-                                          limit_mem = Whyconf.memlimit main} in
+                                          limit_time = !session_timelimit;
+                                          limit_mem = !session_memlimit} in
           Some (prover_config, default_limit)
       | [timeout] -> Some (prover_config,
                            Call_provers.{empty_limit with
-                                         limit_time = int_of_string timeout})
+                                          limit_time = int_of_string timeout;
+                                          limit_mem = !session_memlimit})
       | [timeout; oom ] ->
         Some (prover_config, Call_provers.{empty_limit with
                                            limit_time = int_of_string timeout;

src/session/server_utils.mli

@@ -25,6 +25,13 @@ val get_session_dir : allow_mkdir:bool -> string Queue.t -> string
 
  *)
 
+val set_session_timelimit : int -> unit
+(** sets the default timelimit in seconds. Initially set to 2. *)
+
+val set_session_memlimit : int -> unit
+(** sets the default mem in Mb. Initially set to 1000. *)
+
+
 (** Simple queries *)
 
 (* The id you are trying to use is undefined *)

src/tools/why3replay.ml

@@ -114,7 +114,7 @@ let found_upgraded_prover = ref false
 module C = Controller_itp.Make(Unix_scheduler.Unix_scheduler)
 
 let () =
-  C.set_max_tasks (Whyconf.running_provers_max (Whyconf.get_main config));
+  Controller_itp.set_session_max_tasks (Whyconf.running_provers_max (Whyconf.get_main config));
   C.register_observer
     (fun w s r ->
       if Debug.test_flag debug then