STM: proof block detection made optional + simple test

2 files changed, 22 insertions, 11 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 35f7295dd6..c1158928df 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1111,9 +1111,9 @@ let prev_node { id } =
 let cur_node id = mk_doc_node id (VCS.visit id)
 
 let detect_proof_block id = function
-  | None -> ()
-  | Some name ->
-      match cur_node id with
+  | Some name when !Flags.async_proofs_tac_error_resilience &&
+                   !Flags.async_proofs_mode != Flags.APoff ->
+      begin match cur_node id with
       | None -> ()
       | Some entry_point -> try
           let static, _ = List.assoc name !proof_block_delimiters in
@@ -1124,7 +1124,8 @@ let detect_proof_block id = function
           end
         with Not_found ->
           Errors.errorlabstrm "STM"
-            (str "Unknown proof block delimiter " ++ str name)
+            (str "Unknown proof block delimiter " ++ str name) end
+  | _ -> ()
 
 (****************************** THE SCHEDULER *********************************)
 (******************************************************************************)
@@ -2016,14 +2017,24 @@ let known_state ?(redefine_qed=false) ~cache id =
 
   (* Absorb tactic errors from f () *)
   let resilient_tactic id f =
-    try f ()
-    with e when Errors.noncritical e ->
-      let ie = Errors.push e in
-      error_absorbing_tactic id ie in
+    if not !Flags.async_proofs_tac_error_resilience ||
+       (Flags.async_proofs_is_master () &&
+        !Flags.async_proofs_mode = Flags.APoff)
+    then f ()
+    else
+      try f ()
+      with e when Errors.noncritical e ->
+        let ie = Errors.push e in
+        error_absorbing_tactic id ie in
   (* Absorb errors from f x *)
   let resilient_command f x =
-    try f x
-    with e when Errors.noncritical e -> () in
+    if not !Flags.async_proofs_cmd_error_resilience ||
+       (Flags.async_proofs_is_master () &&
+        !Flags.async_proofs_mode = Flags.APoff)
+    then f x
+    else
+      try f x
+      with e when Errors.noncritical e -> () in
 
   (* ugly functions to process nested lemmas, i.e. hard to reproduce
    * side effects *)
diff --git a/stm/stm.mli b/stm/stm.mli
index 20dd40bcd4..37ec1f0a13 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -130,7 +130,7 @@ module QueryTask : AsyncTaskQueue.Task
    Declaration of block  [-------------------------------------------]
 
       start = 5            the first state_id that could fail in the block
-      stop = 6             the node that may absorb the error
+      stop = 7             the node that may absorb the error
       dynamic_switch = 4   dynamic check on this node
       carry_on_data = ()   no need to carry extra data from static to dynamic
                            checks