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 c1ec9738ca..7de4fe8548 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -73,6 +73,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 24780f0dcc..5aef2d5cf2 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -34,6 +34,7 @@ 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_delegation_threshold : float ref val debug : bool ref val in_debugger : bool ref diff --git a/stm/stm.ml b/stm/stm.ml index 8f11875b62..4eb2c4b2dd 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1676,9 +1676,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 c4222b3305..62578b9cb7 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -368,6 +368,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] -> @@ -490,6 +495,8 @@ 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-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 ()) |