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).

1 files changed, 16 insertions, 9 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index f902206e2..b1d3e0cc2 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -218,10 +218,14 @@ let no_compat_ntn = ref false
 let print_where = ref false
 let print_config = ref false
 
-let get_slave_number = function
-  | "off" -> -1
-  | "on" -> 0
-  | s -> let n = int_of_string s in assert (n > 0); n
+let get_async_proofs_mode opt next = function
+  | "off" -> Flags.APoff
+  | "on" -> Flags.APonParallel 0
+  | "worker" ->
+      let n = int_of_string (next()) in assert (n > 0);
+      Flags.APonParallel n
+  | "lazy" -> Flags.APonLazy
+  | _ -> prerr_endline ("Error: on/off/lazy/worker expected after "^opt); exit 1
 
 let get_bool opt = function
   | "yes" -> true
@@ -310,9 +314,12 @@ let parse_args arglist =
 
     (* Options with one arg *)
     |"-coqlib" -> Flags.coqlib_spec:=true; Flags.coqlib:=(next ())
-    |"-coq-slaves" -> Flags.coq_slave_mode := (get_slave_number (next ()))
-    |"-coq-slaves-j" -> Flags.coq_slaves_number := (get_int opt (next ()))
-    |"-coq-slaves-opts" -> Flags.coq_slave_options := Some (next ())
+    |"-async-proofs" ->
+        Flags.async_proofs_mode := get_async_proofs_mode opt next (next())
+    |"-async-proofs-j" ->
+        Flags.async_proofs_n_workers := (get_int opt (next ()))
+    |"-async-proofs-worker-flags" ->
+        Flags.async_proofs_worker_flags := Some (next ())
     |"-compat" -> Flags.compat_version := get_compat_version (next ())
     |"-compile" -> add_compile false (next ())
     |"-compile-verbose" -> add_compile true (next ())
@@ -414,7 +421,7 @@ let init arglist =
       if !Flags.ide_slave then begin
         Flags.make_silent true;
         Ide_slave.init_stdout ()
-      end else if !Flags.coq_slave_mode > 0 then begin
+      end else if Flags.async_proofs_is_worker () then begin
         Flags.make_silent true;
         Stm.slave_init_stdout ()
       end;
@@ -467,7 +474,7 @@ let start () =
     Dumpglob.noglob () in
   if !Flags.ide_slave then
     Ide_slave.loop ()
-  else if !Flags.coq_slave_mode > 0 then
+  else if Flags.async_proofs_is_worker () then
     Stm.slave_main_loop ()
   else
     Coqloop.loop();