diff options
-rw-r--r-- | lib/flags.ml | 2 | ||||
-rw-r--r-- | lib/flags.mli | 2 | ||||
-rw-r--r-- | stm/stm.ml | 31 | ||||
-rw-r--r-- | stm/stm.mli | 2 | ||||
-rw-r--r-- | test-suite/interactive/proof_block.v | 56 | ||||
-rw-r--r-- | toplevel/coqtop.ml | 4 |
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 ()) |