diff options
| author | Enrico Tassi | 2016-05-31 14:42:49 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-05-31 14:42:49 +0200 |
| commit | d46e4bc63587c1b628cc80b3eac7a132a58d534d (patch) | |
| tree | 00ae2ded7013e15fcf5c98223fe20e64e0fd6454 /toplevel | |
| parent | b3485ddc8c4f98743426bb58c8d49b76edd43d61 (diff) | |
STM delegation policy can be customized
The command line option is named:
- async-proofs-delegation-threshold
Values are of type float, default 1.0 (seconds).
Proofs taking less that the threshold are not delegated to
a worker.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 7 |
1 files changed, 7 insertions, 0 deletions
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 ()) |