STM delegation policy can be customized

The command line option is named:
  - async-proofs-delegation-threshold
Values are of type float, default 1.0 (seconds).
Proofs taking less that the threshold are not delegated to
a worker.

4 files changed, 12 insertions, 3 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index c1ec9738c..7de4fe854 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -73,6 +73,7 @@ let async_proofs_is_worker () =
   !async_proofs_worker_id <> "master"
 let async_proofs_is_master () =
   !async_proofs_mode = APon && !async_proofs_worker_id = "master"
+let async_proofs_delegation_threshold = ref 1.0
 
 let debug = ref false
 let in_debugger = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 24780f0dc..5aef2d5cf 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -34,6 +34,7 @@ type priority = Low | High
 val async_proofs_worker_priority : priority ref
 val string_of_priority : priority -> string
 val priority_of_string : string -> priority
+val async_proofs_delegation_threshold : float ref
 
 val debug : bool ref
 val in_debugger : bool ref
diff --git a/stm/stm.ml b/stm/stm.ml
index 8f11875b6..4eb2c4b2d 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1676,9 +1676,9 @@ let async_policy () =
     (!compilation_mode = BuildVio || !async_proofs_mode <> APoff)
 
 let delegate name =
-  let time = get_hint_bp_time name in
-  time >= 1.0 || !Flags.compilation_mode = Flags.BuildVio
-              || !Flags.async_proofs_full
+     get_hint_bp_time name >= !Flags.async_proofs_delegation_threshold
+  || !Flags.compilation_mode = Flags.BuildVio
+  || !Flags.async_proofs_full
  
 let collect_proof keep cur hd brkind id =
  prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id);
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c4222b330..62578b9cb 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -368,6 +368,11 @@ let get_int opt n =
   with Failure _ ->
     prerr_endline ("Error: integer expected after option "^opt); exit 1
 
+let get_float opt n =
+  try float_of_string n
+  with Failure _ ->
+    prerr_endline ("Error: float expected after option "^opt); exit 1
+
 let get_host_port opt s =
   match CString.split ':' s with
   | [host; portr; portw] ->
@@ -490,6 +495,8 @@ let parse_args arglist =
         Flags.async_proofs_worker_priority := get_priority opt (next ())
     |"-async-proofs-private-flags" ->
         Flags.async_proofs_private_flags := Some (next ());
+    |"-async-proofs-delegation-threshold" ->
+        Flags.async_proofs_delegation_threshold:= get_float opt (next ())
     |"-worker-id" -> set_worker_id opt (next ())
     |"-compat" -> let v = get_compat_version (next ()) in Flags.compat_version := v; add_compat_require v
     |"-compile" -> add_compile false (next ())