STM: add "Stm Wait" to wait for the slaves to complete their jobs

Used by fake_ide, that before editing a broken proof has to be sure
Coq known the proof is broken.

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

5 files changed, 40 insertions, 11 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index d05a25596f..2e23d22732 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -219,6 +219,7 @@ type bullet =
 type 'a stm_vernac =
   | JoinDocument
   | Finish
+  | Wait
   | PrintDag
   | Observe of Stateid.t
   | Command of 'a (* An out of flow command not to be recorded by Stm *)
@@ -436,6 +437,7 @@ and vernac_is_alias = bool
 and vernac_part_of_script = bool
 and vernac_control =
   | VtFinish
+  | VtWait
   | VtJoinDocument
   | VtPrintDag
   | VtObserve of Stateid.t
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index a00783a3bf..1288e2e79c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -80,6 +80,7 @@ GEXTEND Gram
       (* Stm backdoor *)
       | IDENT "Stm"; IDENT "JoinDocument"; "." -> VernacStm JoinDocument
       | IDENT "Stm"; IDENT "Finish"; "." -> VernacStm Finish
+      | IDENT "Stm"; IDENT "Wait"; "." -> VernacStm Wait
       | IDENT "Stm"; IDENT "PrintDag"; "." -> VernacStm PrintDag
       | IDENT "Stm"; IDENT "Observe"; id = INT; "." ->
           VernacStm (Observe (Stateid.of_int (int_of_string id)))
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index bb0f4982bc..2b66844480 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -480,6 +480,7 @@ let rec pr_vernac = function
   | VernacStm JoinDocument -> str"Stm JoinDocument"
   | VernacStm PrintDag -> str"Stm PrintDag"
   | VernacStm Finish -> str"Stm Finish"
+  | VernacStm Wait -> str"Stm Wait"
   | VernacStm (Observe id) ->
       str"Stm Observe " ++ str(Stateid.to_string id)
   | VernacStm (Command v) -> str"Stm Command " ++ pr_vernac v
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 2899098b3a..1eae14a3a5 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -23,6 +23,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 [||]
 
 (* Wrapper for Vernacentries.interp to set the feedback id *)
@@ -947,7 +948,7 @@ end = struct (* {{{ *)
 let pstate = ["meta counter"; "evar counter"; "program-tcc-table"]
 
 let delegate_policy_check l =
-  (interactive () = `Yes || List.length l > 20) &&
+  (interactive () = `Yes || List.length l > !min_proof_length_to_delegate) &&
   (if interactive () = `Yes then !Flags.coq_slave_mode = 0 else true)
 
 let collect_proof cur hd id =
@@ -1049,8 +1050,13 @@ let known_state ?(redefine_qed=false) ~cache id =
                 assert (Stateid.equal view.next eop);
                 reach eop; vernac_interp id x; Proof_global.discard_all ()
               ), `Yes
-          | `NotOptimizable _ -> (fun () ->
-                prerr_endline ("NotOptimizable " ^ Stateid.to_string id);
+          | `NotOptimizable reason -> (fun () ->
+                prerr_endline ("NotOptimizable " ^ Stateid.to_string id ^ " " ^
+                  match reason with
+                  | `Transparent -> "Transparent"
+                  | `AlreadyEvaluated -> "AlreadyEvaluated"
+                  | `TooShort -> "TooShort"
+                  | _ -> "WTF");
                 reach eop;
                 begin match keep with
                 | VtKeep ->
@@ -1224,12 +1230,18 @@ let init () =
       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;
-    try
+    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
         (Str.split_delim (Str.regexp ";") (Str.replace_first env_opt "" env))
-    with Not_found -> ()
+    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 ()
@@ -1251,6 +1263,10 @@ let finish () =
   observe (VCS.get_branch_pos (VCS.current_branch ()));
   VCS.print ()
 
+let wait () =
+  Slaves.wait_all_done ();
+  VCS.print ()
+
 let join () =
   let rec jab id =
     if Stateid.equal id Stateid.initial then ()
@@ -1261,8 +1277,7 @@ let join () =
            Future.purify observe eop; jab view.next
       | _ -> jab view.next in
   finish ();
-  VCS.print ();
-  Slaves.wait_all_done ();
+  wait ();
   prerr_endline "Joining the environment";
   Global.join_safe_environment ();
   VCS.print ();
@@ -1310,10 +1325,12 @@ let process_transaction ~tty verbose c (loc, expr) =
       (* Joining various parts of the document *)
       | VtStm (VtJoinDocument, b), VtNow -> warn_if_pos x b; join (); `Ok
       | VtStm (VtFinish, b),       VtNow -> warn_if_pos x b; finish (); `Ok
+      | VtStm (VtWait, b),       VtNow -> warn_if_pos x b; finish (); wait (); `Ok
       | VtStm (VtPrintDag, b), VtNow ->
           warn_if_pos x b; VCS.print ~now:true (); `Ok
       | VtStm (VtObserve id, b),   VtNow -> warn_if_pos x b; observe id; `Ok
-      | VtStm ((VtObserve _ | VtFinish | VtJoinDocument|VtPrintDag),_), VtLater ->
+      | VtStm ((VtObserve _ | VtFinish | VtJoinDocument
+                |VtPrintDag |VtWait),_), VtLater ->
           anomaly(str"classifier: join actions cannot be classified as VtLater")
       
       (* Back *)
@@ -1467,8 +1484,15 @@ let query ~at s =
   Future.purify (fun s ->
     if Stateid.equal at Stateid.dummy then finish ()
     else Reach.known_state ~cache:`Yes at;
-    let loc_ast = vernac_parse 0 s in
-    ignore(process_transaction ~tty:false true (VtQuery false, VtNow) loc_ast))
+    let _, ast as loc_ast = vernac_parse 0 s in
+    let clas = classify_vernac ast in
+    match clas with
+    | VtStm (w,_), _ ->
+       ignore(process_transaction
+         ~tty:false true (VtStm (w,false), VtNow) loc_ast)
+    | _ ->
+       ignore(process_transaction
+         ~tty:false true (VtQuery false, VtNow) loc_ast))
   s
 
 let add ~ontop ?(check=ignore) verb eid s =
diff --git a/toplevel/vernac_classifier.ml b/toplevel/vernac_classifier.ml
index 2edd2fa2de..3c19e887c1 100644
--- a/toplevel/vernac_classifier.ml
+++ b/toplevel/vernac_classifier.ml
@@ -21,7 +21,7 @@ let string_of_vernac_type = function
   | VtProofStep -> "ProofStep"
   | VtProofMode s -> "ProofMode " ^ s
   | VtQuery b -> "Query" ^ string_of_in_script b
-  | VtStm ((VtFinish|VtJoinDocument|VtObserve _|VtPrintDag), b) ->
+  | VtStm ((VtFinish|VtJoinDocument|VtObserve _|VtPrintDag|VtWait), b) ->
       "Stm" ^ string_of_in_script b
   | VtStm (VtBack _, b) -> "Stm Back" ^ string_of_in_script b
 
@@ -52,6 +52,7 @@ let rec classify_vernac e =
   let static_classifier e = match e with
     (* Stm *)
     | VernacStm Finish -> VtStm (VtFinish, true), VtNow
+    | VernacStm Wait -> VtStm (VtWait, true), VtNow
     | VernacStm JoinDocument -> VtStm (VtJoinDocument, true), VtNow
     | VernacStm PrintDag -> VtStm (VtPrintDag, true), VtNow
     | VernacStm (Observe id) -> VtStm (VtObserve id, true), VtNow