diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 11 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 5 |
2 files changed, 15 insertions, 1 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 43ffa762e2..b418269955 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -41,7 +41,9 @@ let print_header () = let warning s = msg_warning (strbrk s) let toploop = ref None -let toploop_init = ref (fun x -> x) +let toploop_init = ref (fun x -> + CoqworkmgrApi.(init !Flags.async_proofs_worker_priority); + x) let toploop_run = ref (fun () -> if Dumpglob.dump () then begin if_verbose warning "Dumpglob cannot be used in interactive mode."; @@ -228,6 +230,11 @@ let no_compat_ntn = ref false let print_where = ref false let print_config = ref false +let get_priority opt s = + try Flags.priority_of_string s + with Invalid_argument _ -> + prerr_endline ("Error: low/high expected after "^opt); exit 1 + let get_async_proofs_mode opt = function | "off" -> Flags.APoff | "on" -> Flags.APon @@ -359,6 +366,8 @@ let parse_args arglist = Flags.async_proofs_n_workers := (get_int opt (next ())) |"-async-proofs-tac-j" -> Flags.async_proofs_n_tacworkers := (get_int opt (next ())) + |"-async-proofs-worker-priority" -> + Flags.async_proofs_worker_priority := get_priority opt (next ()) |"-async-proofs-private-flags" -> Flags.async_proofs_private_flags := Some (next ()); |"-worker-id" -> set_worker_id opt (next ()) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index a011fc6a69..5e9d77bedd 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -350,3 +350,8 @@ let compile verbosely f = let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in Library.save_library_raw lfdv lib univs proofs +let compile v f = + ignore(CoqworkmgrApi.get 1); + compile v f; + CoqworkmgrApi.giveback 1 + |