From d46e4bc63587c1b628cc80b3eac7a132a58d534d Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 31 May 2016 14:42:49 +0200
Subject: 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.
---
 stm/stm.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 8f11875b62..4eb2c4b2dd 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);
-- 
cgit v1.2.3