STM: proof block detection made optional + simple test

6 files changed, 86 insertions, 11 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index c1ec9738c..ecf3c3f16 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -68,6 +68,8 @@ let priority_of_string = function
   | "low" -> Low
   | "high" -> High
   | _ -> raise (Invalid_argument "priority_of_string")
+let async_proofs_tac_error_resilience = ref true
+let async_proofs_cmd_error_resilience = ref true
 
 let async_proofs_is_worker () =
   !async_proofs_worker_id <> "master"
diff --git a/lib/flags.mli b/lib/flags.mli
index 24780f0dc..b26ef027c 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -34,6 +34,8 @@ type priority = Low | High
 val async_proofs_worker_priority : priority ref
 val string_of_priority : priority -> string
 val priority_of_string : string -> priority
+val async_proofs_tac_error_resilience : bool ref
+val async_proofs_cmd_error_resilience : bool ref
 
 val debug : bool ref
 val in_debugger : bool ref
diff --git a/stm/stm.ml b/stm/stm.ml
index 35f7295dd..c1158928d 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 20dd40bcd..37ec1f0a1 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
diff --git a/test-suite/interactive/proof_block.v b/test-suite/interactive/proof_block.v
new file mode 100644
index 000000000..ff920b671
--- /dev/null
+++ b/test-suite/interactive/proof_block.v
@@ -0,0 +1,56 @@
+
+Lemma baz :  (exists n, n = 3 /\ n = 3) /\ True.
+Proof.
+split. { eexists. split. par: trivial. }
+trivial.
+Qed.
+
+Lemma baz1 :  (True /\ False) /\ True.
+Proof.
+split. { split. par: trivial. }
+trivial.
+Qed.
+
+Lemma foo : (exists n, n = 3 /\ n = 3) /\ True.
+Proof.
+split.
+  { idtac.
+    unshelve eexists.
+    { apply 3. }
+    { split.
+      { idtac. trivialx. }
+      { reflexivity. } } }
+  trivial.
+Qed.
+
+Lemma foo1 : False /\ True.
+Proof.
+split.
+  exact I.
+  { exact I. }
+Qed.
+
+Definition banana := true + 4. 
+
+Check banana.
+
+Lemma bar : (exists n, n = 3 /\ n = 3) /\ True.
+Proof.
+split.
+  - idtac.
+    unshelve eexists.
+    + apply 3.
+    + split.
+      * idtacx. trivial. 
+      * reflexivity.
+  - trivial.
+Qed.
+
+Lemma baz2 :  ((1=0 /\ False) /\ True) /\ False.
+Proof.
+split. split. split.
+ - solve [ auto ].
+ - solve [ trivial ].
+ - solve [ trivial ].
+ - exact 6.
+Qed.
\ No newline at end of file
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 869f6bb93..c52830ea7 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -492,6 +492,10 @@ let parse_args arglist =
         Flags.async_proofs_worker_priority := get_priority opt (next ())
     |"-async-proofs-private-flags" ->
         Flags.async_proofs_private_flags := Some (next ());
+    |"-async-proofs-tactic-error-resilience" ->
+        Flags.async_proofs_tac_error_resilience := get_bool opt (next ())
+    |"-async-proofs-command-error-resilience" ->
+        Flags.async_proofs_cmd_error_resilience := get_bool opt (next ())
     |"-worker-id" -> set_worker_id opt (next ())
     |"-compat" -> let v = get_compat_version (next ()) in Flags.compat_version := v; add_compat_require v
     |"-compile" -> add_compile false (next ())