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

9 files changed, 90 insertions, 57 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 87387c5f9..7d1267c3a 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -480,7 +480,7 @@ let install_input_watch handle respawner feedback_processor =
 let spawn_handle args =
   let prog = coqtop_path () in
   let args = Array.of_list (
-    prog :: "-coq-slaves" :: "on" :: "-ideslave" :: args) in
+    prog :: "-async-proofs" :: "on" :: "-ideslave" :: args) in
   let pid, ic, gic, oc, close_channels = open_process_pid prog args in
   let xml_ic = Xml_parser.make (Xml_parser.SChannel ic) in
   let xml_oc = Xml_printer.make (Xml_printer.TChannel oc) in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index f7805459f..5397e42f9 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -246,6 +246,12 @@ let in_whnf (t,stk) =
 
 let steps = ref 0
 
+let slave_process =
+  let rec f = ref (fun () ->
+    match !Flags.async_proofs_mode with
+    | Flags.APonParallel n -> let b = n > 0 in f := (fun () -> b); !f ()
+    | _ -> f := (fun () -> false); !f ()) in
+  fun () -> !f ()
 
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
 let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
@@ -255,7 +261,7 @@ let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
 and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
   Util.check_for_interrupt ();
   incr steps;
-  if !steps = 10000 && !Flags.coq_slave_mode > 0 then begin
+  if !steps = 10000 && slave_process () then begin
     Thread.yield ();
     steps := 0;
   end;
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
 
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 378f493ad..5e63322c5 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -117,8 +117,10 @@ let parse_args () =
       |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
       |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit"
       |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs"
-      |"-impredicative-set"|"-vm"|"-no-native-compiler"|"-quick"
-      |"-verbose-compat-notations"|"-no-compat-notations" as o) :: rem ->
+      |"-impredicative-set"|"-vm"|"-no-native-compiler"
+      |"-verbose-compat-notations"|"-no-compat-notations"
+      |"-quick"
+      as o) :: rem ->
 	parse (cfiles,o::args) rem
 
 (* Options for coqtop : b) options with 1 argument *)
@@ -127,7 +129,8 @@ let parse_args () =
       |"-load-vernac-source"|"-l"|"-load-vernac-object"
       |"-load-ml-source"|"-require"|"-load-ml-object"
       |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"
-      |"-check-vi-tasks" as o) :: rem ->
+      |"-async-proofs-j" |"-async-proofs-worker-flags" |"-async-proofs"
+      as o) :: rem ->
 	begin
 	  match rem with
 	    | s :: rem' -> parse (cfiles,s::o::args) rem'
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();
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index bb531056f..86b7794e8 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -6,9 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+let process_id () =
+  match !Flags.async_proofs_mode with
+  | Flags.APoff | Flags.APonLazy | Flags.APonParallel 0 -> "master"
+  | Flags.APonParallel n -> "worker" ^ string_of_int n 
+
 let prerr_endline s =
   if !Flags.debug then begin
-    prerr_endline (Printf.sprintf "%d] %s" !Flags.coq_slave_mode s);
+    prerr_endline (Printf.sprintf "%s] %s" (process_id ()) s);
     flush stderr
   end else ()
 
@@ -27,8 +32,7 @@ let interactive () =
 
 let fallback_to_lazy_if_marshal_error = ref true
 let fallback_to_lazy_if_slave_dies = ref true
-let min_proof_length_to_delegate = ref 20
-let coq_slave_extra_env = ref [||]
+let async_proofs_workers_extra_env = ref [||]
 
 type ast = { verbose : bool; loc : Loc.t; mutable expr : vernac_expr }
 let pr_ast { expr } = pr_vernac expr
@@ -232,7 +236,7 @@ end = struct (* {{{ *)
   open Printf
 
   let print_dag vcs () = (* {{{ *)
-    let fname = "stm" ^ string_of_int (max 0 !Flags.coq_slave_mode) in
+    let fname = "stm_" ^ process_id () in
     let string_of_transaction = function
       | Cmd (t, _) | Fork (t, _,_,_) ->
           (try string_of_ppcmds (pr_ast t) with _ -> "ERR")
@@ -692,16 +696,16 @@ end = struct (* {{{ *)
       Unix.set_close_on_exec s2c_r;
       let prog =  Sys.argv.(0) in
       let rec set_slave_opt = function
-        | [] -> ["-coq-slaves"; string_of_int n]
+        | [] -> ["-async-proofs"; "worker"; string_of_int n]
         | ("-ideslave"|"-emacs"|"-emacs-U")::tl -> set_slave_opt tl
-        | ("-coq-slaves"
+        | ("-async-proofs"
           |"-compile"
           |"-compile-verbose")::_::tl -> set_slave_opt tl
         | x::tl -> x :: set_slave_opt tl in
       let args = Array.of_list (set_slave_opt (Array.to_list Sys.argv)) in
       prerr_endline ("EXEC: " ^ prog ^ " " ^
         (String.concat " " (Array.to_list args)));
-      let env = Array.append !coq_slave_extra_env (Unix.environment ()) in
+      let env = Array.append !async_proofs_workers_extra_env (Unix.environment ()) in
       let pid = Unix.create_process_env prog args env c2s_r s2c_w Unix.stderr in
       Unix.close c2s_r;
       Unix.close s2c_w;
@@ -897,7 +901,14 @@ end = struct (* {{{ *)
 
   exception KillRespawn
     
-  let report_status ?(id = !Flags.coq_slave_mode) s =
+  let report_status ?id s =
+    let id =
+      match id with
+      | Some n -> n
+      | None ->
+          match !Flags.async_proofs_mode with
+          | Flags.APonParallel n -> n
+          | _ -> assert false in
     Pp.feedback ~state_id:Stateid.initial (Interface.SlaveStatus(id, s))
 
   let rec manage_slave respawn =
@@ -1004,7 +1015,7 @@ end = struct (* {{{ *)
         flush_all (); exit 1
                     
 
-  let init () = SlavesPool.init !Flags.coq_slaves_number manage_slave
+  let init () = SlavesPool.init !Flags.async_proofs_n_workers manage_slave
 
   let slave_ic = ref stdin
   let slave_oc = ref stdout
@@ -1077,7 +1088,7 @@ end = struct (* {{{ *)
         prerr_endline "Slave: failed with the following exception:";
         prerr_endline (string_of_ppcmds (print e))
       | e ->
-        Printf.eprintf "Slave: failed with the following CRITICAL exception: %s\n"
+        Printf.eprintf "Slave: critical exception: %s\n"
           (Pp.string_of_ppcmds (print e));  
         flush_all (); exit 1
     done
@@ -1103,9 +1114,10 @@ end = struct (* {{{ *)
 
 let pstate = ["meta counter"; "evar counter"; "program-tcc-table"]
 
-let delegate_policy_check l =
-  (interactive () = `Yes || List.length l > !min_proof_length_to_delegate) &&
-  (if interactive () = `Yes then !Flags.coq_slave_mode = 0 else true)
+let delegate_policy_check () =
+  if interactive () = `Yes then !Flags.async_proofs_mode = Flags.APonParallel 0
+  else if !Flags.compilation_mode = Flags.BuildVi then true
+  else !Flags.async_proofs_mode <> Flags.APoff
 
 let collect_proof cur hd id =
  prerr_endline ("Collecting proof ending at "^Stateid.to_string id);
@@ -1118,15 +1130,14 @@ let collect_proof cur hd id =
     match last, view.step with
     | _, `Cmd (x, _) -> collect (Some (id,x)) (id::accn) view.next
     | _, `Alias _ -> `Sync `Alias
-    | _, `Fork(_,_,_,_::_::_)->
-        `Sync `MutualProofs (* TODO: enderstand where we need that *)
+    | _, `Fork(_,_,_,_::_::_)-> `Sync `MutualProofs
     | _, `Fork(_,_,Doesn'tGuaranteeOpacity,_) ->
         `Sync `Doesn'tGuaranteeOpacity
     | Some (parent, ({ expr = VernacProof(_,Some _)} as v)),
       `Fork (_, hd', GuaranteesOpacity, ids) ->
         assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
-        if delegate_policy_check accn then `ASync (parent,Some v,accn,ids)
-        else `Sync `TooShort
+        if delegate_policy_check () then `ASync (parent,Some v,accn,ids)
+        else `Sync `Policy
     | Some (parent, ({ expr = VernacProof(t,None)} as v)),
       `Fork (_, hd', GuaranteesOpacity, ids) when
        not (State.is_cached parent) &&
@@ -1135,13 +1146,13 @@ let collect_proof cur hd id =
           let hint = get_hint_ctx loc in
           assert (VCS.Branch.equal hd hd'||VCS.Branch.equal hd VCS.edit_branch);
           v.expr <- VernacProof(t, Some hint);
-          if delegate_policy_check accn then `ASync (parent,Some v,accn,ids)
-          else `Sync `TooShort
+          if delegate_policy_check () then `ASync (parent,Some v,accn,ids)
+          else `Sync `Policy
         with Not_found -> `Sync `NoHint)
     | Some (parent, _), `Fork (_, hd', GuaranteesOpacity, ids) ->
         assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
-        if delegate_policy_check accn then `MaybeASync (parent, accn, ids)
-        else `Sync `TooShort
+        if delegate_policy_check () then `MaybeASync (parent, accn, ids)
+        else `Sync `Policy
     | _, `Sideff (`Ast (x,_)) -> collect (Some (id,x)) (id::accn) view.next
     | _, `Sideff (`Id _) -> `Sync `NestedProof
     | _ -> `Sync `Unknown in
@@ -1156,7 +1167,7 @@ let collect_proof cur hd id =
 let string_of_reason = function
   | `Transparent -> "Transparent"
   | `AlreadyEvaluated -> "AlreadyEvaluated"
-  | `TooShort -> "TooShort"
+  | `Policy -> "Policy"
   | `NestedProof -> "NestedProof"
   | `Immediate -> "Immediate"
   | `Alias -> "Alias"
@@ -1423,9 +1434,9 @@ let init () =
   set_undo_classifier Backtrack.undo_vernac_classifier;
   State.define ~cache:`Yes (fun () -> ()) Stateid.initial;
   Backtrack.record ();
-  if Int.equal !Flags.coq_slave_mode 0 then begin (* We are the master process *)
+  if !Flags.async_proofs_mode = Flags.APonParallel 0 then begin
     Slaves.init ();
-    let opts = match !Flags.coq_slave_options with
+    let opts = match !Flags.async_proofs_worker_flags with
       | None -> []
       | Some s -> Str.split_delim (Str.regexp ",") s in
     if String.List.mem "fallback-to-lazy-if-marshal-error=no" opts then
@@ -1435,15 +1446,9 @@ let init () =
     begin try
       let env_opt = Str.regexp "^extra-env=" in
       let env = List.find (fun s -> Str.string_match env_opt s 0) opts in
-      coq_slave_extra_env := Array.of_list
+      async_proofs_workers_extra_env := Array.of_list
         (Str.split_delim (Str.regexp ";") (Str.replace_first env_opt "" env))
     with Not_found -> () end;
-    begin try
-      let minlen_opt = Str.regexp "^min-proof-length-to-delegate=" in
-      let len = List.find (fun s -> Str.string_match minlen_opt s 0) opts in
-      min_proof_length_to_delegate :=
-        int_of_string (Str.replace_first minlen_opt "" len)
-    with Not_found -> () end;
   end
 
 let slave_main_loop () = Slaves.slave_main_loop Ephemeron.clear