Commit 39ed26b1 authored by Andrei Paskevich's avatar Andrei Paskevich

Prove_client: change the "standalone" logic

1. No default socket name is provided. If Why3 should connect to
   an external server, Prove_client.set_socket_name must be called
   first.

2. If Prove_client.set_socket_name was never called, Why3 assumes
   to be in the stand-alone mode, and will start the server in the
   standard tmp directory (on Unix, $TMPDIR or /tmp, on Win, $TEMP or .).
   The socket name is set to be "why3server.<PID_of_Why3>.sock",
   to avoid clashes with other Why3 processes (fixes the Coq tactic).

3. Global reference Prove_client.standalone is removed.

4. Call_provers does not reexport Prove_client.set_socket_name.

5. Prove_client.connect does nothing if the socket reference is set.
parent a3e8d499
......@@ -271,10 +271,8 @@ let adapt_limits limit on_timelimit =
(* otherwise use t *)
else limit.limit_time }
let set_socket_name =
Prove_client.set_socket_name
type server_id = int
let gen_id =
let x = ref 0 in
fun () ->
......
......@@ -169,5 +169,3 @@ val query_call : prover_call -> post_prover_call option
val wait_on_call : prover_call -> post_prover_call
(** blocking function that waits until the prover finishes. *)
val set_socket_name : string -> unit
let standalone : bool ref = ref true
let socket : Unix.file_descr option ref = ref None
let max_running_provers : int ref = ref 1
let client_connect socket_name =
if Sys.os_type = "Win32" then begin
let name = "\\\\.\\pipe\\" ^ socket_name in
socket := Some (Unix.openfile name [Unix.O_RDWR] 0)
end else begin
let sock = Unix.socket Unix.PF_UNIX Unix.SOCK_STREAM 0 in
let sock = Unix.socket Unix.PF_UNIX Unix.SOCK_STREAM 0 in
Unix.connect sock (Unix.ADDR_UNIX socket_name);
socket := Some sock
end
......@@ -15,7 +13,9 @@ let client_connect socket_name =
let client_disconnect () =
match !socket with
| None -> ()
| Some s -> Unix.close s
| Some s ->
socket := None;
Unix.close s
let send_request_string msg =
match !socket with
......@@ -54,46 +54,58 @@ type answer =
out_file : string;
}
let socket_name : string ref = ref "why3server.sock"
let socket_name : string option ref = ref None
let set_socket_name s =
socket_name := s
let buf : Buffer.t = Buffer.create 1024
socket_name := Some s
let connect () =
Buffer.clear buf;
client_connect !socket_name
let max_running_provers : int ref = ref 1
let disconnect () =
client_disconnect ()
let set_max_running_provers x =
if x <= 0 then invalid_arg "Prove_client.set_max_running_provers";
max_running_provers := x;
if !socket <> None then
send_request_string ("parallel;" ^ string_of_int x)
let run_server () =
let run_server socket_name =
let exec = Filename.concat Config.libdir "why3server" in
ignore
(Unix.create_process exec
[|exec; "--socket"; !socket_name;
Unix.create_process exec
[|exec; "--socket"; socket_name;
"--single-client";
"-j"; string_of_int !max_running_provers |]
Unix.stdin Unix.stdout Unix.stderr)
Unix.stdin Unix.stdout Unix.stderr
let force_connect () =
match !socket with
| None when !standalone ->
let _pid = run_server () in
let buf : Buffer.t = Buffer.create 1024
let connect () =
Buffer.clear buf;
match !socket_name with
| Some sname ->
(* FIXME? should we send !max_running_provers once connected?
This branch is normally only used for external servers *)
client_connect sname
| None ->
let cwd = Unix.getcwd () in
Unix.chdir (Filename.get_temp_dir_name ());
let sname = Filename.concat (Unix.getcwd ())
("why3server." ^ string_of_int (Unix.getpid ()) ^ ".sock") in
let _server_pid = run_server sname in
Unix.chdir cwd;
(* sleep is needed before connecting,
or the server will not be ready yet *)
ignore (Unix.select [] [] [] 0.1);
connect()
| _ -> ()
set_socket_name sname;
client_connect sname
let set_max_running_provers x =
max_running_provers := x;
if !socket <> None then
send_request_string ("parallel;" ^ string_of_int x)
let connect () =
(* must disconnect first *)
if !socket = None then connect ()
let disconnect () =
client_disconnect ()
let send_request ~use_stdin ~id ~timelimit ~memlimit ~cmd =
force_connect ();
let send_request ~id ~timelimit ~memlimit ~use_stdin ~cmd =
connect ();
let buf = Buffer.create 128 in
let servercommand = if use_stdin <> None then "runstdin;" else "run;" in
Buffer.add_string buf servercommand;
......
val standalone : bool ref
val set_socket_name : string -> unit
val set_max_running_provers : int -> unit
val connect : unit -> unit
val disconnect : unit -> unit
val send_request :
use_stdin:string option ->
id:int ->
timelimit:int ->
memlimit:int ->
cmd:string list->
id:int ->
timelimit:int ->
memlimit:int ->
use_stdin:string option ->
cmd:string list ->
unit
type answer =
......@@ -23,5 +22,3 @@ type answer =
}
val read_answers : blocking:bool -> answer list
val disconnect : unit -> unit
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