Paral-ITP: cleanup of command line flags and more conservative default

-async-proofs off
  the system behaves as in 8.4
-async-proofs lazy
  proofs are delayed (when possible) but never processed in parallel
-async-proofs on
  proofs are processed in parallel (when possible).  The number of
  workers is 1, can be changed with -async-proofs-j.  Extra options to
  the worker process can be given with -async-proofs-worker-flags.

The default for batch compilation used to be "lazy", now it is "off".
The "lazy" default was there to test the machinery, but it makes very
little sense in a batch scenario.  If you process things sequentially,
you'd better do them immediately instead of accumulating everything in
memory until the end of the file and only then force all lazy computations.

The default for -ideslave was and still is "on".  It becomes dynamically
"lazy" on a per task (proof) basis if the worker dies badly.

Note that by passing "-async-proofs on" to coqc one can produce a .vo
exploiting multiple workers.  But this is rarely profitable given
that master-to-worker communication is inefficient (i.e. it really
depends on the size of proofs v.s. size of system state).

4 files changed, 24 insertions, 12 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index 0cefc90c4..3a79a83e3 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -47,10 +47,16 @@ let batch_mode = ref false
 
 type compilation_mode = BuildVo | BuildVi
 let compilation_mode = ref BuildVo
-let coq_slave_mode = ref (-1)
-let coq_slaves_number = ref 1
 
-let coq_slave_options = ref None
+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_is_worker () =
+  match !async_proofs_mode with
+  | APonParallel n -> n > 0
+  | _ -> false
 
 let debug = ref false
 
diff --git a/lib/flags.mli b/lib/flags.mli
index f0b676641..476b52a7a 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -14,10 +14,12 @@ val batch_mode : bool ref
 type compilation_mode = BuildVo | BuildVi
 val compilation_mode : compilation_mode ref
 
-val coq_slave_mode : int ref
-val coq_slaves_number : int ref
+type async_proofs = APoff | APonLazy | APonParallel of int
+val async_proofs_mode : async_proofs ref
+val async_proofs_n_workers : int ref
+val async_proofs_worker_flags : string option ref
 
-val coq_slave_options : string option ref
+val async_proofs_is_worker : unit -> bool
 
 val debug : bool ref
 
diff --git a/lib/future.ml b/lib/future.ml
index 391f5a65c..191fc3fdd 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -17,12 +17,12 @@ let _ = Errors.register_handler (function
   | NotReady ->
       Pp.strbrk("The value you are asking for is not ready yet. " ^
                 "Please wait or pass "^
-                "the \"-coq-slaves off\" option to CoqIDE to disable "^
+                "the \"-async-proofs off\" option to CoqIDE to disable "^
                 "asynchronous script processing.")
   | NotHere ->
       Pp.strbrk("The value you are asking for is not available "^
                 "in this process. If you really need this, pass "^
-                "the \"-coq-slaves off\" option to CoqIDE to disable"^
+                "the \"-async-proofs off\" option to CoqIDE to disable"^
                 "asynchronous script processing.")
   | _ -> raise Errors.Unhandled)
 
diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml
index 1983d2722..e0e2d5cbc 100644
--- a/lib/remoteCounter.ml
+++ b/lib/remoteCounter.ml
@@ -16,14 +16,18 @@ let new_counter a ~incr ~build =
     (* - slaves must use a remote counter getter, not this one! *)
     (* - in the main process there is a race condition between slave
          managers (that are threads) and the main thread, hence the mutex *)
-    if !Flags.coq_slave_mode > 0 then
-      Errors.anomaly(Pp.str"Slave processes must install remote counters");
+    (match !Flags.async_proofs_mode with
+    | Flags.APonParallel n when n > 0 ->
+        Errors.anomaly(Pp.str"Slave processes must install remote counters");
+    | _ -> ());
     Mutex.lock m; let x = f () in Mutex.unlock m;
     build x in
   let getter = ref (mk_thsafe_getter (fun () -> data := incr !data; !data)) in
   let installer f =
-    if !Flags.coq_slave_mode < 1 then
+    (match !Flags.async_proofs_mode with
+    | Flags.APoff | Flags.APonLazy | Flags.APonParallel 0 -> 
       Errors.anomaly(Pp.str"Only slave processes can install a remote counter")
-    else getter := f in
+    | _ -> ());
+    getter := f in
   (fun () -> !getter ()), installer