diff options
| -rw-r--r-- | lib/flags.ml | 1 | ||||
| -rw-r--r-- | lib/flags.mli | 1 | ||||
| -rw-r--r-- | stm/stm.ml | 6 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 7 |
4 files changed, 12 insertions, 3 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index 3093e52b0..226698539 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -76,6 +76,7 @@ let async_proofs_is_worker () = !async_proofs_worker_id <> "master" let async_proofs_is_master () = !async_proofs_mode = APon && !async_proofs_worker_id = "master" +let async_proofs_delegation_threshold = ref 1.0 let debug = ref false let in_debugger = ref false diff --git a/lib/flags.mli b/lib/flags.mli index d77681553..729c21fcf 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -37,6 +37,7 @@ val priority_of_string : string -> priority 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 async_proofs_delegation_threshold : float ref val debug : bool ref val in_debugger : bool ref diff --git a/stm/stm.ml b/stm/stm.ml index 75d2e070a..358ff89b9 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1875,9 +1875,9 @@ let async_policy () = (!compilation_mode = BuildVio || !async_proofs_mode <> APoff) let delegate name = - let time = get_hint_bp_time name in - time >= 1.0 || !Flags.compilation_mode = Flags.BuildVio - || !Flags.async_proofs_full + get_hint_bp_time name >= !Flags.async_proofs_delegation_threshold + || !Flags.compilation_mode = Flags.BuildVio + || !Flags.async_proofs_full let collect_proof keep cur hd brkind id = prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id); diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index ceaaa112e..a488bb3e6 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -370,6 +370,11 @@ let get_int opt n = with Failure _ -> prerr_endline ("Error: integer expected after option "^opt); exit 1 +let get_float opt n = + try float_of_string n + with Failure _ -> + prerr_endline ("Error: float expected after option "^opt); exit 1 + let get_host_port opt s = match CString.split ':' s with | [host; portr; portw] -> @@ -501,6 +506,8 @@ let parse_args arglist = 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 ()) + |"-async-proofs-delegation-threshold" -> + Flags.async_proofs_delegation_threshold:= get_float 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 ()) |