Commit 134a8572 authored by François Bobot's avatar François Bobot
Browse files

session_scheduler : provide the scheduler of replay inside the library

parent 2601188f
...@@ -151,14 +151,8 @@ let () = ...@@ -151,14 +151,8 @@ let () =
Debug.Opt.set_flags_selected (); Debug.Opt.set_flags_selected ();
if Debug.Opt.option_list () then exit 0 if Debug.Opt.option_list () then exit 0
let usleep t = ignore (Unix.select [] [] [] t)
let idle_handler = ref None
let timeout_handler = ref None
module O = module O =
(struct struct
type key = int type key = int
let create ?parent () = let create ?parent () =
...@@ -170,20 +164,6 @@ module O = ...@@ -170,20 +164,6 @@ module O =
let reset () = () let reset () = ()
let idle f =
match !idle_handler with
| None -> idle_handler := Some f;
| Some _ -> failwith "Replay.idle: already one handler installed"
let timeout ~ms f =
match !timeout_handler with
| None -> timeout_handler := Some(float ms /. 1000.0 ,f);
| Some _ -> failwith "Replay.timeout: already one handler installed"
let notify_timer_state w s r =
Printf.eprintf "Progress: %d/%d/%d \r%!" w s r
let init = let init =
(* (*
let cpt = ref 0 in let cpt = ref 0 in
...@@ -232,7 +212,11 @@ let unknown_prover _ _ = None ...@@ -232,7 +212,11 @@ let unknown_prover _ _ = None
let replace_prover _ _ = false let replace_prover _ _ = false
end) module Scheduler = Session_scheduler.Base_scheduler(struct end)
include Scheduler
end
module M = Session_scheduler.Make(O) module M = Session_scheduler.Make(O)
...@@ -246,46 +230,7 @@ let print_result fmt ...@@ -246,46 +230,7 @@ let print_result fmt
if ans == Call_provers.HighFailure then if ans == Call_provers.HighFailure then
fprintf fmt "@\nProver output:@\n%s@." out fprintf fmt "@\nProver output:@\n%s@." out
let main_loop () = let main_loop = O.main_loop
let last = ref (Unix.gettimeofday ()) in
while true do
let time = Unix.gettimeofday () -. !last in
(* attempt to run timeout handler *)
let timeout =
match !timeout_handler with
| None -> false
| Some(ms,f) ->
if time > ms then
let b = f () in
if b then true else
begin
timeout_handler := None;
true
end
else false
in
if timeout then
last := Unix.gettimeofday ()
else
(* attempt to run the idle handler *)
match !idle_handler with
| None ->
begin
let ms =
match !timeout_handler with
| None -> 100.0 (* raise Exit *)
| Some(ms,_) -> ms
in
usleep (ms -. time)
end
| Some f ->
let b = f () in
if b then () else
begin
idle_handler := None;
end
done
(* (*
let model_index = Hashtbl.create 257 let model_index = Hashtbl.create 257
*) *)
...@@ -723,8 +668,7 @@ let () = ...@@ -723,8 +668,7 @@ let () =
else else
begin begin
add_to_check found_obs env_session sched; add_to_check found_obs env_session sched;
try main_loop () main_loop (); eprintf "main replayer exited unexpectedly@."; exit 1
with Exit -> eprintf "main replayer exited unexpectedly@."
end end
with with
| S.OutdatedSession -> | S.OutdatedSession ->
......
...@@ -809,6 +809,77 @@ let convert_unknown_prover = ...@@ -809,6 +809,77 @@ let convert_unknown_prover =
Session_tools.convert_unknown_prover ~keygen:O.create Session_tools.convert_unknown_prover ~keygen:O.create
end end
module Base_scheduler (X : sig end) =
(struct
let usleep t = ignore (Unix.select [] [] [] t)
let idle_handler = ref None
let timeout_handler = ref None
let idle f =
match !idle_handler with
| None -> idle_handler := Some f;
| Some _ -> failwith "Replay.idle: already one handler installed"
let timeout ~ms f =
match !timeout_handler with
| None -> timeout_handler := Some(float ms /. 1000.0 ,f);
| Some _ -> failwith "Replay.timeout: already one handler installed"
let notify_timer_state w s r =
Printf.eprintf "Progress: %d/%d/%d \r%!" w s r
let main_loop () =
let last = ref (Unix.gettimeofday ()) in
try while true do
let time = Unix.gettimeofday () -. !last in
(* attempt to run timeout handler *)
let timeout =
match !timeout_handler with
| None -> false
| Some(ms,f) ->
if time > ms then
let b = f () in
if b then true else
begin
timeout_handler := None;
true
end
else false
in
if timeout then
last := Unix.gettimeofday ()
else
(* attempt to run the idle handler *)
match !idle_handler with
| None ->
begin
let ms =
match !timeout_handler with
| None -> raise Exit
| Some(ms,_) -> ms
in
usleep (ms -. time)
end
| Some f ->
let b = f () in
if b then () else
begin
idle_handler := None;
end
done
with Exit -> ()
end)
(* (*
Local Variables: Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3ide.byte" compile-command: "unset LANG; make -C ../.. bin/why3ide.byte"
......
...@@ -227,6 +227,21 @@ module Make(O: OBSERVER) : sig ...@@ -227,6 +227,21 @@ module Make(O: OBSERVER) : sig
end end
(** A functor (a state is hidden) that provide a working scheduler
and which can be used as base for an OBSERVER *)
module Base_scheduler (X : sig end) : sig
val timeout: ms:int -> (unit -> bool) -> unit
val idle: (unit -> bool) -> unit
val notify_timer_state : int -> int -> int -> unit
(** These functions have the properties required by OBSERVER *)
val main_loop : unit -> unit
(** [main_loop ()] run the main loop. Run the timeout handler and the
the idle handler registered until the two of them are done. Nothing is run
until this function is called *)
end
(* (*
Local Variables: Local Variables:
......
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