From 3abbc93733b7f820a436beedcd0b9292378e1840 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 30 Jun 2014 23:25:19 +0200
Subject: option to always delegate futures to workers

---
 lib/flags.ml       | 1 +
 lib/flags.mli      | 1 +
 stm/stm.ml         | 6 ++++--
 toplevel/coqtop.ml | 2 ++
 4 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/lib/flags.ml b/lib/flags.ml
index 7fed951008..36bb447ae9 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -52,6 +52,7 @@ type async_proofs = APoff | APonLazy | APonParallel of int
 let async_proofs_mode = ref APoff
 let async_proofs_n_workers = ref 1
 let async_proofs_worker_flags = ref None
+let async_proofs_always_delegate = ref false
 
 let async_proofs_is_worker () =
   match !async_proofs_mode with
diff --git a/lib/flags.mli b/lib/flags.mli
index c1e5a9dbd0..ea50d41da9 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -21,6 +21,7 @@ val async_proofs_n_workers : int ref
 val async_proofs_worker_flags : string option ref
 
 val async_proofs_is_worker : unit -> bool
+val async_proofs_always_delegate : bool ref
 
 val debug : bool ref
 
diff --git a/stm/stm.ml b/stm/stm.ml
index f62bae4b12..2007dba811 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1151,9 +1151,11 @@ let pstate = ["meta counter"; "evar counter"; "program-tcc-table"]
 let delegate_policy_check time =
   if interactive () = `Yes then
     (!Flags.async_proofs_mode = Flags.APonParallel 0 ||
-    !Flags.async_proofs_mode = Flags.APonLazy) && time >= 1.0
+    !Flags.async_proofs_mode = Flags.APonLazy) &&
+    (time >= 1.0 || !Flags.async_proofs_always_delegate)
   else if !Flags.compilation_mode = Flags.BuildVi then true
-  else !Flags.async_proofs_mode <> Flags.APoff && time >= 1.0
+  else !Flags.async_proofs_mode <> Flags.APoff &&
+       (time >= 1.0 || !Flags.async_proofs_always_delegate)
 
 let collect_proof cur hd brkind id =
  prerr_endline ("Collecting proof ending at "^Stateid.to_string id);
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index d64e3d979d..0ccb6faafd 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -379,6 +379,8 @@ let parse_args arglist =
     |"-toploop" -> toploop := Some (next ())
 
     (* Options with zero arg *)
+    |"-async-proofs-always-delegate" ->
+        Flags.async_proofs_always_delegate := true;
     |"-batch" -> set_batch_mode ()
     |"-beautify" -> make_beautify true
     |"-boot" -> boot := true; no_load_rc ()
-- 
cgit v1.2.3