diff options
| -rw-r--r-- | Makefile.build | 5 | ||||
| -rw-r--r-- | Makefile.common | 4 | ||||
| -rw-r--r-- | doc/refman/AsyncProofs.tex | 23 | ||||
| -rw-r--r-- | ide/ide_slave.ml | 1 | ||||
| -rw-r--r-- | lib/flags.ml | 7 | ||||
| -rw-r--r-- | lib/flags.mli | 4 | ||||
| -rw-r--r-- | stm/asyncTaskQueue.ml | 23 | ||||
| -rw-r--r-- | stm/coqworkmgrApi.ml | 140 | ||||
| -rw-r--r-- | stm/coqworkmgrApi.mli | 44 | ||||
| -rw-r--r-- | stm/stm.mllib | 1 | ||||
| -rw-r--r-- | stm/stmworkertop.ml | 1 | ||||
| -rw-r--r-- | stm/tacworkertop.ml | 1 | ||||
| -rw-r--r-- | tools/coqworkmgr.ml | 222 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 11 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 5 |
15 files changed, 484 insertions, 8 deletions
diff --git a/Makefile.build b/Makefile.build index 2963a3d7a..7cc4351be 100644 --- a/Makefile.build +++ b/Makefile.build @@ -634,6 +634,11 @@ $(COQDOC): $(patsubst %.cma,%$(BESTLIB),$(COQDOCCMO:.cmo=$(BESTOBJ))) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,str unix) +$(COQWORKMGR): $(addsuffix $(BESTOBJ), stm/coqworkmgrApi tools/coqworkmgr) \ + $(addsuffix $(BESTLIB), lib/clib) + $(SHOW)'OCAMLBEST -o $@' + $(HIDE)$(call bestocaml,, $(SYSMOD) clib) + # fake_ide : for debugging or test-suite purpose, a fake ide simulating # a connection to coqtop -ideslave diff --git a/Makefile.common b/Makefile.common index 5b90e19db..44cdc0baf 100644 --- a/Makefile.common +++ b/Makefile.common @@ -94,8 +94,10 @@ COQTEX:=bin/coq-tex$(EXE) COQWC:=bin/coqwc$(EXE) COQDOC:=bin/coqdoc$(EXE) FAKEIDE:=bin/fake_ide$(EXE) +COQWORKMGR:=bin/coqworkmgr$(EXE) -TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC) $(COQC) +TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\ + $(COQWORKMGR) PRIVATEBINARIES:=$(FAKEIDE) $(COQDEPBOOT) diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex index f4c54be26..8ccce0bf4 100644 --- a/doc/refman/AsyncProofs.tex +++ b/doc/refman/AsyncProofs.tex @@ -1,8 +1,8 @@ -\achapter{Asynchronous Proof Processing} +\achapter{Asynchronous and Parallel Proof Processing} \aauthor{Enrico Tassi} \label{pralitp} -\index{Asynchronous Proof Processing!presentation} +\index{Asynchronous and Parallel Proof Processing!presentation} This chapter explains how proofs can be asynchronously processed by Coq. This feature improves the reactiveness of the system when used in interactive @@ -145,6 +145,25 @@ are checked to be consistent for every single proof, but not globally. Hence this compilation mode is only useful for quick regression testing and on developments not making heavy use of the $Type$ hierarchy. +\subsection{Limiting the number of parallel workers} +\label{coqworkmgr} + +Many Coq processes may run on the same computer, and each of them may start +many additional worker processes. +The $coqworkmgr$ utility lets one limit the number of workers, globally. + +The utility acecpts the $-j$ argument to specify the maximum number of +workers (defaults to 2). $coqworkmgr$ autmatically starts in the +background and prints an enviroment variable assignement like +$COQWORKMGR\_SOCKET=localhost:45634$. The user must set this variable in +all the shells from which he will start Coq processes. If one uses just +one terminal running the bash shell, then $export `coqworkmgr -j 4`$ will +do the job. + +After that all Coq processes, like $coqide$ and $coqc$ will honor such +limit, globally. + + %%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 42bc939b5..7c5d7a077 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -466,6 +466,7 @@ let () = Coqtop.toploop_init := (fun args -> let args = parse args in Flags.make_silent true; init_stdout (); + CoqworkmgrApi.(init High); args) let () = Coqtop.toploop_run := loop diff --git a/lib/flags.ml b/lib/flags.ml index 75f149eb6..790acfef5 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -57,6 +57,13 @@ let async_proofs_always_delegate = ref false let async_proofs_never_reopen_branch = ref false let async_proofs_flags_for_workers = ref [] let async_proofs_worker_id = ref "master" +type priority = Low | High +let async_proofs_worker_priority = ref Low +let string_of_priority = function Low -> "low" | High -> "high" +let priority_of_string = function + | "low" -> Low + | "high" -> High + | _ -> raise (Invalid_argument "priority_of_string") let async_proofs_is_worker () = !async_proofs_worker_id <> "master" diff --git a/lib/flags.mli b/lib/flags.mli index 4697e4cac..11909c5fa 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -26,6 +26,10 @@ val async_proofs_always_delegate : bool ref val async_proofs_never_reopen_branch : bool ref val async_proofs_flags_for_workers : string list ref val async_proofs_worker_id : string ref +type priority = Low | High +val async_proofs_worker_priority : priority ref +val string_of_priority : priority -> string +val priority_of_string : string -> priority val debug : bool ref diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 5de80bbfc..cb03459cc 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -142,10 +142,14 @@ module Make(T : Task) = struct let rec set_slave_opt = function | [] -> !Flags.async_proofs_flags_for_workers @ ["-toploop"; T.name^"top"; - "-worker-id"; id] + "-worker-id"; id; + "-async-proofs-worker-priority"; + Flags.string_of_priority !Flags.async_proofs_worker_priority] | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl | ("-async-proofs" |"-toploop" |"-vi2vo" |"-compile" - | "-load-vernac-source" | "-compile-verbose")::_::tl -> set_slave_opt tl + |"-load-vernac-source" |"-compile-verbose" + |"-async-proofs-worker-priority" |"-worker-id") :: _ :: tl -> + set_slave_opt tl | x::tl -> x :: set_slave_opt tl in let args = Array.of_list (set_slave_opt (List.tl (Array.to_list Sys.argv))) in @@ -155,6 +159,9 @@ module Make(T : Task) = struct let task_expired = ref false in let task_cancelled = ref false in let worker_age = ref `Fresh in + let got_token = ref false in + let giveback_token () = + if !got_token then (CoqworkmgrApi.giveback 1; got_token := false) in CThread.prepare_in_channel_for_thread_friendly_io ic; try while not !die do @@ -166,6 +173,8 @@ module Make(T : Task) = struct begin try let req = T.request_of_task !worker_age task in if req = None then raise Expired; + ignore(CoqworkmgrApi.get 1); got_token := true; + prerr_endline ("got execution token"); marshal_request oc (Request (Option.get req)); Worker.kill_if proc ~sec:1 (fun () -> task_expired := !cancel_switch; @@ -177,7 +186,7 @@ module Make(T : Task) = struct match response with | Response resp -> (match T.use_response task resp with - | `Stay -> last_task := None; () + | `Stay -> last_task := None; giveback_token () | `StayReset -> last_task := None; raise KillRespawn) | RespGetCounterNewUnivLevel -> marshal_more_data oc (MoreDataUnivLevel @@ -205,19 +214,25 @@ module Make(T : Task) = struct raise Die with | KillRespawn -> + giveback_token (); Worker.kill proc; ignore(Worker.wait proc); manage_slave ~cancel:cancel_user_req ~die id respawn - | (Die | TQueue.BeingDestroyed) -> Worker.kill proc;ignore(Worker.wait proc) + | (Die | TQueue.BeingDestroyed) -> + giveback_token (); + Worker.kill proc;ignore(Worker.wait proc) | Sys_error _ | Invalid_argument _ | End_of_file when !task_expired -> + giveback_token (); T.on_task_cancellation_or_expiration !last_task; ignore(Worker.wait proc); manage_slave ~cancel:cancel_user_req ~die id respawn | Sys_error _ | Invalid_argument _ | End_of_file when !task_cancelled -> + giveback_token (); msg_warning(strbrk "The worker was cancelled."); T.on_task_cancellation_or_expiration !last_task; Worker.kill proc; ignore(Worker.wait proc); manage_slave ~cancel:cancel_user_req ~die id respawn | Sys_error _ | Invalid_argument _ | End_of_file -> + giveback_token (); match T.on_slave_death !last_task with | `Stay -> msg_warning(strbrk "The worker process died badly."); diff --git a/stm/coqworkmgrApi.ml b/stm/coqworkmgrApi.ml new file mode 100644 index 000000000..a22fd5427 --- /dev/null +++ b/stm/coqworkmgrApi.ml @@ -0,0 +1,140 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +let debug = false + +type request = + | Hello of Flags.priority + | Get of int + | TryGet of int + | GiveBack of int + | Ping + +type response = + | Tokens of int + | Noluck + | Pong of int * int * int + +exception ParseError + +(* make it work with telnet: strip trailing \r *) +let strip_r s = + let len = String.length s in + if s.[len - 1] <> '\r' then s else String.sub s 0 (len - 1) + +let positive_int_of_string n = + try + let n = int_of_string n in + if n <= 0 then raise ParseError else n + with Invalid_argument _ | Failure _ -> raise ParseError + +let parse_request s = + if debug then Printf.eprintf "parsing '%s'\n" s; + match Str.split (Str.regexp " ") (strip_r s) with + | [ "HELLO"; "LOW" ] -> Hello Flags.Low + | [ "HELLO"; "HIGH" ] -> Hello Flags.High + | [ "GET"; n ] -> Get (positive_int_of_string n) + | [ "TRYGET"; n ] -> TryGet (positive_int_of_string n) + | [ "GIVEBACK"; n ] -> GiveBack (positive_int_of_string n) + | [ "PING" ] -> Ping + | _ -> raise ParseError + +let parse_response s = + if debug then Printf.eprintf "parsing '%s'\n" s; + match Str.split (Str.regexp " ") (strip_r s) with + | [ "TOKENS"; n ] -> Tokens (positive_int_of_string n) + | [ "NOLUCK" ] -> Noluck + | [ "PONG"; n; m; p ] -> + let n = try int_of_string n with _ -> raise ParseError in + let m = try int_of_string m with _ -> raise ParseError in + let p = try int_of_string p with _ -> raise ParseError in + Pong (n,m,p) + | _ -> raise ParseError + +let print_request = function + | Hello Flags.Low -> "HELLO LOW\n" + | Hello Flags.High -> "HELLO HIGH\n" + | Get n -> Printf.sprintf "GET %d\n" n + | TryGet n -> Printf.sprintf "TRYGET %d\n" n + | GiveBack n -> Printf.sprintf "GIVEBACK %d\n" n + | Ping -> "PING\n" + +let print_response = function + | Tokens n -> Printf.sprintf "TOKENS %d\n" n + | Noluck -> "NOLUCK\n" + | Pong (n,m,p) -> Printf.sprintf "PONG %d %d %d\n" n m p + +let connect s = + try + match Str.split (Str.regexp ":") s with + | [ h; p ] -> + let open Unix in + let s = socket PF_INET SOCK_STREAM 0 in + connect s (ADDR_INET (inet_addr_of_string h,int_of_string p)); + Some s + | _ -> None + with Unix.Unix_error _ -> None + +let manager = ref None + +let option_map f = function None -> None | Some x -> Some (f x) + +let init p = + try + let sock = Sys.getenv "COQWORKMGR_SOCK" in + manager := option_map (fun s -> + let cout = Unix.out_channel_of_descr s in + set_binary_mode_out cout true; + let cin = Unix.in_channel_of_descr s in + set_binary_mode_in cin true; + output_string cout (print_request (Hello p)); flush cout; + cin, cout) (connect sock) + with Not_found | End_of_file -> () + +let with_manager f g = + try + match !manager with + | None -> f () + | Some (cin, cout) -> g cin cout + with + | ParseError | End_of_file -> manager := None; f () + +let get n = + with_manager + (fun () -> + min n (min !Flags.async_proofs_n_workers !Flags.async_proofs_n_tacworkers)) + (fun cin cout -> + output_string cout (print_request (Get n)); + flush cout; + let l = input_line cin in + match parse_response l with + | Tokens m -> m + | _ -> raise (Failure "coqworkmgr protocol error")) + +let tryget n = + with_manager + (fun () -> + Some + (min n + (min !Flags.async_proofs_n_workers !Flags.async_proofs_n_tacworkers))) + (fun cin cout -> + output_string cout (print_request (TryGet n)); + flush cout; + let l = input_line cin in + match parse_response l with + | Tokens m -> Some m + | Noluck -> None + | _ -> raise (Failure "coqworkmgr protocol error")) + +let giveback n = + with_manager + (fun () -> ()) + (fun cin cout -> + output_string cout (print_request (GiveBack n)); + flush cout) + diff --git a/stm/coqworkmgrApi.mli b/stm/coqworkmgrApi.mli new file mode 100644 index 000000000..453029132 --- /dev/null +++ b/stm/coqworkmgrApi.mli @@ -0,0 +1,44 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* High level api for clients of the service (like coqtop) *) + +(* Connects to a work manager if any. If no worker manager, then + -async-proofs-j and -async-proofs-tac-j are used *) +val init : Flags.priority -> unit + +(* blocking *) +val get : int -> int + +(* not blocking *) +val tryget : int -> int option +val giveback : int -> unit + +(* Low level *) +type request = + | Hello of Flags.priority + | Get of int + | TryGet of int + | GiveBack of int + | Ping + +type response = + | Tokens of int + | Noluck + | Pong of int * int * int (* cur, max, pid *) + +val connect : string -> Unix.file_descr option + +exception ParseError + +(* Intended to be used with input_line and output_string *) +val parse_request : string -> request +val parse_response : string -> response + +val print_request : request -> string +val print_response : response -> string diff --git a/stm/stm.mllib b/stm/stm.mllib index 308b2ac4c..28f097780 100644 --- a/stm/stm.mllib +++ b/stm/stm.mllib @@ -5,6 +5,7 @@ TQueue WorkerPool Vernac_classifier Lemmas +CoqworkmgrApi AsyncTaskQueue Stm Vi_checking diff --git a/stm/stmworkertop.ml b/stm/stmworkertop.ml index 50afd97ab..0d1b44e49 100644 --- a/stm/stmworkertop.ml +++ b/stm/stmworkertop.ml @@ -9,6 +9,7 @@ let () = Coqtop.toploop_init := (fun args -> Flags.make_silent true; Stm.slave_init_stdout (); + CoqworkmgrApi.init !Flags.async_proofs_worker_priority; args) let () = Coqtop.toploop_run := Stm.slave_main_loop diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml index 8a582a689..5e3d90c75 100644 --- a/stm/tacworkertop.ml +++ b/stm/tacworkertop.ml @@ -9,6 +9,7 @@ let () = Coqtop.toploop_init := (fun args -> Flags.make_silent true; Stm.tacslave_init_stdout (); + CoqworkmgrApi.init !Flags.async_proofs_worker_priority; args) let () = Coqtop.toploop_run := Stm.tacslave_main_loop diff --git a/tools/coqworkmgr.ml b/tools/coqworkmgr.ml new file mode 100644 index 000000000..23f452166 --- /dev/null +++ b/tools/coqworkmgr.ml @@ -0,0 +1,222 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open CoqworkmgrApi + +let debug = ref false + +type party = { + sock : Unix.file_descr; + cout : out_channel; + mutable tokens : int; + priority : Flags.priority; +} + +let answer party msg = + output_string party.cout (print_response msg); flush party.cout + +let mk_socket_channel () = + let open Unix in + let s = socket PF_INET SOCK_STREAM 0 in + bind s (ADDR_INET (inet_addr_loopback,0)); + listen s 1; + match getsockname s with + | ADDR_INET(host, port) -> + s, string_of_inet_addr host ^":"^ string_of_int port + | _ -> assert false + +module Queue : sig + type t + val is_empty : t -> bool + val push : int * party -> t -> unit + val pop : t -> int * party + val create : unit -> t +end = struct + type t = (int * party) list ref + let create () = ref [] + let is_empty q = !q = [] + let rec split acc = function + | [] -> List.rev acc, [] + | (_, { priority = Flags.Low }) :: _ as l -> List.rev acc, l + | x :: xs -> split (x :: acc) xs + let push (_,{ priority } as item) q = + if priority = Flags.Low then q := !q @ [item] + else + let high, low = split [] !q in + q := high @ (item :: low) + let pop q = match !q with x :: xs -> q := xs; x | _ -> assert false +end + +let read_fd fd s ~off ~len = + let rec loop () = + try Unix.read fd s off len + with Unix.Unix_error(Unix.EAGAIN,_,_) -> loop () + in + loop () + +let really_read_fd fd s off len = + let i = ref 0 in + while !i < len do + let off = off + !i in + let len = len - !i in + let r = read_fd fd s ~off ~len in + if r = 0 then raise End_of_file; + i := !i + r + done + +let raw_input_line fd = + try + let b = Buffer.create 80 in + let s = String.make 1 '\000' in + while s <> "\n" do + really_read_fd fd s 0 1; + if s <> "\n" && s <> "\r" then Buffer.add_string b s; + done; + Buffer.contents b + with Unix.Unix_error _ -> raise End_of_file + +let accept s = + let cs, _ = Unix.accept s in + let cout = Unix.out_channel_of_descr cs in + set_binary_mode_out cout true; + match parse_request (raw_input_line cs) with + | Hello p -> { sock=cs; cout; tokens=0; priority=p } + | _ -> (try Unix.close cs with _ -> ()); raise End_of_file + +let parse s = () + +let parties = ref [] + +let max_tokens = ref 2 +let cur_tokens = ref 0 + +let queue = Queue.create () + +let rec allocate n party = + let extra = min n (!max_tokens - !cur_tokens) in + cur_tokens := !cur_tokens + extra; + party.tokens <- party.tokens + extra; + answer party (Tokens extra) + +and de_allocate n party = + let back = min party.tokens n in + party.tokens <- party.tokens - back; + cur_tokens := min (!cur_tokens - back) !max_tokens; + eventually_dequeue () + +and eventually_dequeue () = + if Queue.is_empty queue || !cur_tokens >= !max_tokens then () + else + let req, party = Queue.pop queue in + if List.exists (fun { sock } -> sock = party.sock) !parties + then allocate req party + else eventually_dequeue () + +let chat s = + let party = + try List.find (fun { sock } -> sock = s) !parties + with Not_found -> Printf.eprintf "Internal error"; exit 1 in + try + match parse_request (raw_input_line party.sock) with + | Get n -> + if !cur_tokens < !max_tokens then allocate n party + else Queue.push (n,party) queue + | TryGet n -> + if !cur_tokens < !max_tokens then allocate n party + else answer party Noluck + | GiveBack n -> de_allocate n party + | Ping -> + answer party (Pong (!cur_tokens,!max_tokens,Unix.getpid ())); + raise End_of_file + | Hello _ -> raise End_of_file + with Failure _ | ParseError | Sys_error _ | End_of_file -> + (try Unix.close party.sock with _ -> ()); + parties := List.filter (fun { sock } -> sock <> s) !parties; + de_allocate party.tokens party; + eventually_dequeue () + +let check_alive s = + match CoqworkmgrApi.connect s with + | Some s -> + let cout = Unix.out_channel_of_descr s in + set_binary_mode_out cout true; + output_string cout (print_request (Hello Flags.Low)); flush cout; + output_string cout (print_request Ping); flush cout; + begin match Unix.select [s] [] [] 1.0 with + | [s],_,_ -> + let cin = Unix.in_channel_of_descr s in + set_binary_mode_in cin true; + begin match parse_response (input_line cin) with + | Pong (n,m,pid) -> n, m, pid + | _ -> raise Not_found + end + | _ -> raise Not_found + end + | _ -> raise Not_found + +let main () = + let args = [ + "-j",Arg.Set_int max_tokens, "max number of concurrent jobs"; + "-d",Arg.Set debug, "do not detach (debug)"] in + let usage = + "Prints on stdout an env variable assignement to be picked up by coq\n"^ + "instances in order to limit the maximum number of concurrent workers.\n"^ + "The default value is 2.\n"^ + "Usage:" in + Arg.parse args (fun extra -> + Arg.usage args ("Unexpected argument "^extra^".\n"^usage)) + usage; + try + let sock = Sys.getenv "COQWORKMGR_SOCK" in + if !debug then Printf.eprintf "Contacting %s\n%!" sock; + let cur, max, pid = check_alive sock in + Printf.printf "COQWORKMGR_SOCK=%s\n%!" sock; + Printf.eprintf + "coqworkmgr already up and running (pid=%d, socket=%s, j=%d/%d)\n%!" + pid sock cur max; + exit 0 + with Not_found | Failure _ | Invalid_argument _ | Unix.Unix_error _ -> + if !debug then Printf.eprintf "No running instance. Starting a new one\n%!"; + let master, str = mk_socket_channel () in + if not !debug then begin + let pid = Unix.fork () in + if pid <> 0 then begin + Printf.printf "COQWORKMGR_SOCK=%s\n%!" str; + exit 0 + end else begin + ignore(Unix.setsid ()); + Unix.close Unix.stdin; + Unix.close Unix.stdout; + end; + end else begin + Printf.printf "COQWORKMGR_SOCK=%s\n%!" str; + end; + Sys.catch_break true; + try + while true do + if !debug then + Printf.eprintf "Status: #parties=%d tokens=%d/%d \n%!" + (List.length !parties) !cur_tokens !max_tokens; + let socks = master :: List.map (fun { sock } -> sock) !parties in + let r, _, _ = Unix.select socks [] [] (-1.0) in + List.iter (fun s -> + if s = master then begin + try parties := accept master :: !parties + with _ -> () + end else chat s) + r + done; + exit 0 + with Sys.Break -> + if !parties <> [] then begin + Printf.eprintf "Some coq processes still need me\n%!"; + exit 1; + end else + exit 0 + +let () = main () diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 43ffa762e..b41826995 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 a011fc6a6..5e9d77bed 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 + |