STM: add options to disable fallbacks to ease regression testing

STM falls back to local, lazy, evaluation if the slave dies badly or
if there is a marshalling error.  Both things should never occur, but
is nice to have the system recover if a bug pops up.
Nevertheless during regression testing these fallbacks should be
disabled not to hide a new bug.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16841 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 19 insertions, 2 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index ec6469affe..4e3da3d8c7 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -49,6 +49,8 @@ let ide_slave_mode = ref false
 let coq_slave_mode = ref (-1)
 let coq_slaves_number = ref 1
 
+let coq_slave_options = ref None
+
 let debug = ref false
 
 let print_emacs = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 5774f3ad41..8525d731b7 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -16,6 +16,8 @@ val ide_slave_mode : bool ref
 val coq_slave_mode : int ref
 val coq_slaves_number : int ref
 
+val coq_slave_options : string option ref
+
 val debug : bool ref
 
 val print_emacs : bool ref
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 1187f907e2..6d7293704d 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -266,6 +266,7 @@ let parse_args arglist =
     |"-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 ())
     |"-compat" -> Flags.compat_version := get_compat_version (next ())
     |"-compile" -> add_compile false (next ())
     |"-compile-verbose" -> add_compile true (next ())
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 5889e484e5..22ee2b9c91 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -21,6 +21,9 @@ let interactive () =
   if !Flags.ide_slave || !Flags.print_emacs || not !Flags.batch_mode then `Yes
   else `No
 
+let fallback_to_lazy_if_marshal_error = ref true
+let fallback_to_lazy_if_slave_dies = ref true
+
 (* Wrapper for Vernacentries.interp to set the feedback id *)
 let vernac_interp ?proof id (verbosely, loc, expr) =
   let internal_command = function
@@ -829,7 +832,7 @@ end = struct (* {{{ *)
         | VCS.Expired -> (* task cancelled: e.g. the user did backtrack *)
             Pp.feedback (Interface.InProgress ~-1);
             prerr_endline ("Task expired: " ^ pr_task task)
-        | MarshalError s ->
+        | MarshalError s when !fallback_to_lazy_if_marshal_error ->
             msg_warning(strbrk("Marshalling error: "^s^". "^
               "The system state could not be sent to the slave process. "^
               "Falling back to local, lazy, evaluation."));
@@ -1199,7 +1202,16 @@ 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 Slaves.init ()
+  if Int.equal !Flags.coq_slave_mode 0 then begin
+    Slaves.init ();
+    let opts = match !Flags.coq_slave_options with
+      | None -> []
+      | Some s -> Str.split_delim (Str.regexp ",") s in
+    if List.mem "fallback-to-lazy-if-marshal-error=no" opts then
+      fallback_to_lazy_if_marshal_error := false;
+    if List.mem "fallback-to-lazy-if-slave-dies=no" opts then
+      fallback_to_lazy_if_slave_dies := false;
+  end
 
 let slave_main_loop () = Slaves.slave_main_loop ()