diff options
| -rw-r--r-- | lib/flags.ml | 3 | ||||
| -rw-r--r-- | lib/flags.mli | 3 | ||||
| -rw-r--r-- | stm/stm.ml | 10 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 7 |
4 files changed, 18 insertions, 5 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index ecf3c3f16..e78fa7c0c 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -68,7 +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 +type tac_error_filter = [ `None | `Only of string list | `All ] +let async_proofs_tac_error_resilience = ref (`Only [ "par" ; "proof-block" ]) let async_proofs_cmd_error_resilience = ref true let async_proofs_is_worker () = diff --git a/lib/flags.mli b/lib/flags.mli index b26ef027c..d729be385 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -34,7 +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 +type tac_error_filter = [ `None | `Only of string list | `All ] +val async_proofs_tac_error_resilience : tac_error_filter ref val async_proofs_cmd_error_resilience : bool ref val debug : bool ref diff --git a/stm/stm.ml b/stm/stm.ml index 0e33bea3b..1fd8325e8 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1115,9 +1115,15 @@ let prev_node { id } = mk_doc_node id (VCS.visit id) let cur_node id = mk_doc_node id (VCS.visit id) +let is_block_name_enabled name = + match !Flags.async_proofs_tac_error_resilience with + | `None -> false + | `All -> true + | `Only l -> List.mem name l + let detect_proof_block id name = let name = match name with None -> "indent" | Some x -> x in - if !Flags.async_proofs_tac_error_resilience && + if is_block_name_enabled name && (if Flags.async_proofs_is_master () then !Flags.async_proofs_mode != Flags.APoff else true) then @@ -2031,7 +2037,7 @@ let known_state ?(redefine_qed=false) ~cache id = (* Absorb tactic errors from f () *) let resilient_tactic id blockname f = - if not !Flags.async_proofs_tac_error_resilience || + if !Flags.async_proofs_tac_error_resilience = `None || (Flags.async_proofs_is_master () && !Flags.async_proofs_mode = Flags.APoff) then f () diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c52830ea7..e1f5a70c2 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -379,6 +379,11 @@ let get_host_port opt s = prerr_endline ("Error: host:port or stdfds expected after option "^opt); exit 1 +let get_error_resilience opt = function + | "on" | "all" | "yes" -> `All + | "off" | "no" -> `None + | s -> `Only (String.split ',' s) + let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s) let vio_tasks = ref [] @@ -493,7 +498,7 @@ let parse_args arglist = |"-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 ()) + Flags.async_proofs_tac_error_resilience := get_error_resilience opt (next ()) |"-async-proofs-command-error-resilience" -> Flags.async_proofs_cmd_error_resilience := get_bool opt (next ()) |"-worker-id" -> set_worker_id opt (next ()) |