Commit 04db3cff authored by MARCHE Claude's avatar MARCHE Claude

why3web: use the wserver scheduler

parent dd2f09b9
......@@ -3,19 +3,38 @@ open Why3
module P = struct
let notify _ = ()
let get_requests () = []
let requests = ref []
let push_request r =
requests := r :: !requests
let get_requests () =
let l = !requests in requests := []; l
end
module S = Itp_server.Make (Unix_scheduler.Unix_scheduler) (P)
module S = Itp_server.Make (Wserver) (P)
open Format
let interp_request args =
match args with
| "button1" -> (Itp_server.Command_req "list-provers", 0)
| _ -> invalid_arg "Why3web.interp_request"
let handle_script s args =
match s with
| "request" -> "{ \"request\": \"" ^ args ^ "\" }"
| "request" ->
begin
try P.push_request (interp_request args);
"{ \"request_received\": \"" ^ args ^ "\" }"
with e ->
"{ \"request_error\": \"" ^ args ^ "\" ; \"error\": \"" ^
(Pp.sprintf "%a" Exn_printer.exn_printer e) ^ "\" } "
end
| "getNotifications" ->
let n = Random.int 4 in
"{ \"kind\": \"Random\", \"value\" = \"" ^ string_of_int n ^ "\" }"
......@@ -42,4 +61,14 @@ let handler (addr,req) script cont fmt =
fprintf fmt "%s" ans;
fprintf fmt "@."
let () = Wserver.main_loop None 6789 handler
let help () =
printf "Available commands:@.";
printf "q : quit@."
let stdin_handler s =
match s with
| "?" -> help ()
| "q" -> exit 0
| _ -> printf "unknown command '%s'@." s
let () = Wserver.main_loop None 6789 handler stdin_handler
......@@ -261,36 +261,46 @@ let treat_connection _tmout callback addr fd fmt =
| exc -> print_err_exc exc
end
let accept_connection delay callback s =
let (a,_,_) = Unix.select [s] [] [] delay in
match a with
| [] ->
begin
Printf.eprintf "No connection. Compacting... ";
flush stderr;
Gc.compact ();
Printf.eprintf "Ok\n";
flush stderr
end
| [a] ->
assert (a == s);
let (t, addr) = Unix.accept s in
Unix.setsockopt t Unix.SO_KEEPALIVE true;
let cleanup () =
begin try Unix.shutdown t Unix.SHUTDOWN_SEND with
_ -> ()
end;
begin try Unix.shutdown t Unix.SHUTDOWN_RECEIVE with
_ -> ()
end;
try Unix.close t with
_ -> ()
in
let oc = Unix.out_channel_of_descr t in
treat_connection delay callback addr t (formatter_of_out_channel oc);
close_out oc;
cleanup ()
| _ -> assert false
(* buffer for storing character read on stdin *)
let buf = Bytes.create 256
exception Nothing_to_do
let accept_connection delay callback stdin_callback s =
(* eprintf "Unix.select...@."; *)
let (a,_,_) = Unix.select [s;Unix.stdin] [] [] delay in
(* eprintf " done@."; *)
if a = [] then raise Nothing_to_do
else
List.iter
(fun a ->
if a == s then
let (t, addr) = Unix.accept s in
eprintf "got a connection@.";
Unix.setsockopt t Unix.SO_KEEPALIVE true;
let cleanup () =
begin try Unix.shutdown t Unix.SHUTDOWN_SEND with
_ -> ()
end;
begin try Unix.shutdown t Unix.SHUTDOWN_RECEIVE with
_ -> ()
end;
try Unix.close t with
_ -> ()
in
let oc = Unix.out_channel_of_descr t in
treat_connection delay callback addr t (formatter_of_out_channel oc);
close_out oc;
eprintf "connection treated@.";
cleanup ()
else
if a == Unix.stdin then
let n = Unix.read Unix.stdin buf 0 256 in
eprintf "got a stdin input@.";
stdin_callback (Bytes.sub_string buf 0 (n-1));
eprintf "stdin treated@.";
()
else assert false) a
(* the private list of functions to call on idle, sorted higher
......@@ -333,7 +343,7 @@ let timeout ~ms f =
let time = Unix.gettimeofday () in
insert_timeout_handler ms (time +. ms) f
let main_loop addr_opt port g =
let main_loop addr_opt port callback stdin_callback =
let addr =
match addr_opt with
Some addr ->
......@@ -348,12 +358,9 @@ let main_loop addr_opt port g =
Unix.listen s 4;
Sys.set_signal Sys.sigpipe Sys.Signal_ignore;
let tm = Unix.localtime (Unix.time ()) in
Printf.eprintf "Ready %4d-%02d-%02d %02d:%02d port"
eprintf "Ready %4d-%02d-%02d %02d:%02d port %d...@."
(1900 + tm.Unix.tm_year) (succ tm.Unix.tm_mon) tm.Unix.tm_mday
tm.Unix.tm_hour tm.Unix.tm_min;
Printf.eprintf " %d" port;
Printf.eprintf "...\n";
flush stderr;
tm.Unix.tm_hour tm.Unix.tm_min port;
while true do
(* attempt to run the first timeout handler *)
let time = Unix.gettimeofday () in
......@@ -364,16 +371,10 @@ let main_loop addr_opt port g =
let time = Unix.gettimeofday () in
if b then insert_timeout_handler ms (ms +. time) f
| _ ->
(* time is not yet passed *)
(* attempt to run the first idle handler *)
match !idle_handler with
| (p,f) :: rem ->
idle_handler := rem;
let b = f () in
if b then insert_idle_handler p f
| [] ->
(* no idle handler *)
(* check connection for a some delay *)
(*
eprintf "check connection for a some delay@.";
*)
let delay =
match !timeout_handler with
| [] -> 0.125
......@@ -382,12 +383,21 @@ let main_loop addr_opt port g =
(* or the time left until the next timeout otherwise *)
in
begin
try accept_connection delay g s
try accept_connection delay callback stdin_callback s
with
Unix.Unix_error (Unix.ECONNRESET, "accept", _) -> ()
| Unix.Unix_error ((Unix.EBADF | Unix.ENOTSOCK), "accept", _) as x ->
raise x
| exc -> print_err_exc exc
end;
flush stderr
| Nothing_to_do ->
begin
(* attempt to run the first idle handler *)
match !idle_handler with
| (p,f) :: rem ->
idle_handler := rem;
let b = f () in
if b then insert_idle_handler p f
| [] -> ()
end
| Unix.Unix_error (Unix.ECONNRESET, "accept", _) -> ()
| Unix.Unix_error ((Unix.EBADF | Unix.ENOTSOCK), "accept", _) as x ->
raise x
| e -> eprintf "Anomaly: %a@." Why3.Exn_printer.exn_printer e
end
done
......@@ -2,18 +2,21 @@
val main_loop : string option -> int ->
(Unix.sockaddr * string list -> string -> string -> Format.formatter -> unit) -> unit
(** [main_loop addr port g] starts an elementary httpd server at port
[port] in the current machine. The variable [addr] is [Some
the-address-to-use] or [None] for any of the available addresses
of the present machine. The port number is any number greater than
1024 (to create a client < 1024, you must be root). At each
connection, the function [g] is called: [g (addr, request) scr
cont fmt] where [addr] is the client identification socket,
[request] the browser request, [scr] the script name (extracted
from [request]) and [cont] the stdin contents. [fmt] is the
formatter where the answer should be written. It must start by a
call to [http_header] below. *)
(Unix.sockaddr * string list -> string ->
string -> Format.formatter -> unit) ->
(string -> unit) -> unit
(** [main_loop addr port callback stdin_callback] starts an elementary
httpd server at port [port] in the current machine. The variable
[addr] is [Some the-address-to-use] or [None] for any of the
available addresses of the present machine. The port number is any
number greater than 1024 (to create a client < 1024, you must be
root). At each connection, the function [callback] is called as
[callback (addr, request) scr cont fmt] where [addr] is the client
identification socket, [request] the browser request, [scr] the
script name (extracted from [request]) and [cont] the stdin
contents. [fmt] is the formatter where the answer should be
written, it must start by a call to [http_header] below.
[stdin_callback] is called on any stdin input line received. *)
val timeout: ms:int -> (unit -> bool) -> unit
(** [timeout ~ms f] registers the function [f] as a function to be
......
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