diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index c98fe4dd36abef24926b0d8dc54291de65ffe77a..f6f68681f48c4aff0665852ff94d0156a54372b2 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -1064,8 +1064,10 @@ end
type daemon = {
trigger : unit -> unit ;
+ delayed : (int -> unit) option ;
debounced : float ; (* in ms *)
- mutable next_at : float ; (* next time *)
+ mutable next_at : float ; (* next trigger time *)
+ mutable last_at : float ; (* next yield time *)
}
let pending = ref []
@@ -1073,10 +1075,12 @@ let daemons = ref []
let once trigger = pending := trigger :: !pending
-let on_progress ?(debounced=0) trigger =
+let on_progress ?(debounced=0) ?delayed trigger =
let d = {
trigger ;
debounced = float debounced /. 1000.0 ;
+ delayed ;
+ last_at = 0.0 ;
next_at = 0.0 ;
} in
daemons := List.append !daemons [d] ; d
@@ -1084,8 +1088,8 @@ let on_progress ?(debounced=0) trigger =
let off_progress d =
daemons := List.filter (fun d0 -> d != d0) !daemons
-let with_progress ?debounced trigger job data =
- let d = on_progress ?debounced trigger in
+let with_progress ?debounced ?delayed trigger job data =
+ let d = on_progress ?debounced ?delayed trigger in
try
let res = job data in
off_progress d ; trigger () ; res
@@ -1104,13 +1108,22 @@ let yield_daemons () =
| [] -> ()
| ds ->
let t = Unix.gettimeofday () in
- List.iter (fun d ->
+ List.iter
+ begin fun d ->
+ let delta = d.debounced in
if t > d.next_at then
begin
- d.next_at <- t +. d.debounced ;
+ d.next_at <- t +. delta ;
d.trigger () ;
- end
- ) ds
+ end ;
+ match d.delayed with
+ | None -> ()
+ | Some warn ->
+ let period = t -. d.last_at in
+ let delay = if delta > 0.0 then delta else 0.1 in
+ if period > delay then warn (int_of_float (period *. 1000.0)) ;
+ d.last_at <- t ;
+ end ds
let yield () =
begin
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 196f694814c7074a821cce77c9b2e4c325949ad5..1d56b3e036f9edef42dc574a8e9dda15e66e45e9 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -1346,8 +1346,11 @@ type daemon
Register a new daemon to be executed on [Db.yield()].
When specified, two succcessive calls to the daemon will be
separated by at least [~debounced] milliseconds (default is 0ms).
+ The [~delayed d] callback is invoked when [Db.yield()] has not been called
+ since a delay [d] greater than [~debounced] or 100ms.
*)
-val on_progress : ?debounced:int -> (unit -> unit) -> daemon
+val on_progress :
+ ?debounced:int -> ?delayed:(int -> unit) -> (unit -> unit) -> daemon
(** Un-register the daemon. *)
val off_progress : daemon -> unit
@@ -1370,8 +1373,11 @@ val cancel : unit -> unit
result, with [trigger] registered as a temporary (debounced) daemon.
The daemon is finally flushed and un-registered at the end
of the computation, and any exception is re-raised.
+ The callback [~on_mute d] is triggered when the deamon has not been yielded
+ for a period [d] longer than [~debounce] or 100ms by default.
*)
-val with_progress : ?debounced:int -> (unit -> unit) -> ('a -> 'b) -> 'a -> 'b
+val with_progress : ?debounced:int -> ?delayed:(int -> unit) ->
+ (unit -> unit) -> ('a -> 'b) -> 'a -> 'b
(** This exception may be raised by {!progress} to interrupt computations. *)
exception Cancel
diff --git a/src/plugins/server/main.ml b/src/plugins/server/main.ml
index c66c94f455a385f9daf577c3c7653a46fa15c712..f6b94ed2083983146c60ebbd7d931e37cc20955a 100644
--- a/src/plugins/server/main.ml
+++ b/src/plugins/server/main.ml
@@ -87,14 +87,13 @@ type 'a exec = {
}
type 'a server = {
- rate : int ;
+ yield : int ;
pretty : Format.formatter -> 'a -> unit ;
equal : 'a -> 'a -> bool ;
fetch : unit -> 'a message option ;
q_in : 'a exec Queue.t ;
q_out : 'a response Stack.t ;
mutable shutdown : bool ;
- mutable coins : int ;
mutable running : 'a exec option ;
}
@@ -145,10 +144,14 @@ let execute exec : _ response =
exec.request (Cmdline.protect exn) ;
`Error(exec.id,Printexc.to_string exn)
-let execute_debug pp yield exec =
- if Senv.debug_atleast 1 then
- Senv.debug "Trigger %s:%a" exec.request pp exec.id ;
- Db.with_progress yield execute exec
+let execute_debug server yield exec =
+ let delayed =
+ if Senv.debug_atleast 1 then
+ (Senv.debug "Trigger %s:%a" exec.request server.pretty exec.id ;
+ Some (fun delay -> Senv.debug
+ "No yield since %dms during %s" delay exec.request))
+ else None
+ in Db.with_progress ~debounced:server.yield ?delayed yield execute exec
let reply_debug server resp =
if Senv.debug_atleast 1 then
@@ -223,11 +226,7 @@ let communicate server =
let do_yield server () =
begin
option raise_if_killed server.running ;
- let n = server.coins in
- if n < server.rate then
- server.coins <- succ n
- else
- ( server.coins <- 0 ; ignore ( communicate server ) ) ;
+ ignore ( communicate server );
end
(* -------------------------------------------------------------------------- *)
@@ -246,7 +245,7 @@ let process server =
| Some exec ->
server.running <- Some exec ;
try
- reply_debug server (execute_debug server.pretty (do_yield server) exec) ;
+ reply_debug server (execute_debug server (do_yield server) exec) ;
server.running <- None ;
true
with exn ->
@@ -268,11 +267,11 @@ let signal activity =
let run ~pretty ?(equal=(=)) ~fetch () =
begin
- let rate = in_range ~min:1 ~max:200 (Senv.Rate.get ()) in
+ let yield = in_range ~min:1 ~max:200 (Senv.Yield.get ()) in
let idle_ms = in_range ~min:1 ~max:2000 (Senv.Idle.get ()) in
- let idle_s = float_of_int idle_ms /. 1000.0 in
+ let idle = float_of_int idle_ms /. 1000.0 in
let server = {
- fetch ; coins = 0 ; rate ; equal ; pretty ;
+ fetch ; yield ; equal ; pretty ;
q_in = Queue.create () ;
q_out = Stack.create () ;
running = None ;
@@ -287,7 +286,7 @@ let run ~pretty ?(equal=(=)) ~fetch () =
begin try
while not server.shutdown do
let activity = process server in
- if not activity then Unix.sleepf idle_s ;
+ if not activity then Unix.sleepf idle ;
done ;
with Sys.Break -> () (* Ctr+C, just leave the loop normally *)
end;
diff --git a/src/plugins/server/server_parameters.ml b/src/plugins/server/server_parameters.ml
index 76a572cdf0cbd164afcf0c948b5fec0f9f40e9a6..57dbdd133f9f088015fe82df6ea19932565b883f 100644
--- a/src/plugins/server/server_parameters.ml
+++ b/src/plugins/server/server_parameters.ml
@@ -37,16 +37,16 @@ module Idle = P.Int
(struct
let option_name = "-server-idle"
let arg_name = "ms"
- let default = 10
+ let default = 20
let help = "Waiting time (in milliseconds) when idle"
end)
-module Rate = P.Int
+module Yield = P.Int
(struct
- let option_name = "-server-rate"
- let arg_name = "n"
- let default = 100
- let help = "Number of analysis steps between server communications"
+ let option_name = "-server-yield"
+ let arg_name = "ms"
+ let default = 20
+ let help = "Yielding time (in milliseconds) during computations"
end)
module Doc = P.String
diff --git a/src/plugins/server/server_parameters.mli b/src/plugins/server/server_parameters.mli
index 5dc5ad153438ddc07353cb1b93cc59f22d4e91de..9bbd8a148fde84d797559b9675f44098c42e59c7 100644
--- a/src/plugins/server/server_parameters.mli
+++ b/src/plugins/server/server_parameters.mli
@@ -25,7 +25,7 @@
include Plugin.General_services
module Idle : Parameter_sig.Int (** Idle waiting time (in ms) *)
-module Rate : Parameter_sig.Int (** Number of fetch per yield *)
+module Yield : Parameter_sig.Int (** Yield time (in ms) *)
module Doc : Parameter_sig.String (** Generate documentation *)
module Log : Parameter_sig.Bool (** Monitor logs *)