diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-14 10:51:00 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-14 10:51:00 +0200 |
| commit | ff67a511a358ada3daefea0839e18d474531e13d (patch) | |
| tree | b5dfb7b8d79394d1aabbe0d125d30e12a0fbf621 /toplevel | |
| parent | 19330a458b907b5e66a967adbfe572d92194913c (diff) | |
| parent | 1334a657052a2385c3f3b01cc65c3ccae448fa96 (diff) | |
Merge remote-tracking branch 'origin/pr/173' into trunk
This is the "error resiliency" mode for STM
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index aab20650a..ceaaa112e 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 [] @@ -492,6 +497,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_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 ()) |"-compat" -> let v = get_compat_version (next ()) in Flags.compat_version := v; add_compat_require v |"-compile" -> add_compile false (next ()) |