diff options
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | ide/ide_slave.ml | 3 | ||||
| -rw-r--r-- | lib/control.ml | 7 | ||||
| -rw-r--r-- | lib/control.mli | 3 | ||||
| -rw-r--r-- | lib/flags.ml | 28 | ||||
| -rw-r--r-- | lib/flags.mli | 25 | ||||
| -rw-r--r-- | stm/asyncTaskQueue.ml | 8 | ||||
| -rw-r--r-- | stm/asyncTaskQueue.mli | 3 | ||||
| -rw-r--r-- | stm/coqworkmgrApi.ml | 25 | ||||
| -rw-r--r-- | stm/coqworkmgrApi.mli | 8 | ||||
| -rw-r--r-- | stm/stm.ml | 98 | ||||
| -rw-r--r-- | stm/stm.mli | 27 | ||||
| -rw-r--r-- | stm/workerLoop.ml | 6 | ||||
| -rw-r--r-- | stm/workerLoop.mli | 3 | ||||
| -rw-r--r-- | tools/coqworkmgr.ml | 8 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 38 |
16 files changed, 159 insertions, 133 deletions
diff --git a/Makefile.build b/Makefile.build index 39b793d2b..d548a8bd8 100644 --- a/Makefile.build +++ b/Makefile.build @@ -493,7 +493,7 @@ $(COQDOC): $(call bestobj, $(COQDOCCMO)) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,str unix) -$(COQWORKMGR): $(call bestobj, lib/clib.cma stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo) +$(COQWORKMGR): $(call bestobj, lib/clib.cma lib/lib.cma stm/spawned.cmo stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,, $(SYSMOD)) diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index cfc0e09a0..bd43d1ffc 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -13,7 +13,6 @@ open Util open Pp open Printer -module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration module CompactedDecl = Context.Compacted.Declaration @@ -517,7 +516,7 @@ let rec parse = function let () = Coqtop.toploop_init := (fun args -> let args = parse args in Flags.quiet := true; - CoqworkmgrApi.(init Flags.High); + CoqworkmgrApi.(init High); args) let () = Coqtop.toploop_run := loop diff --git a/lib/control.ml b/lib/control.ml index d936d7557..c6489938e 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -12,15 +12,12 @@ let interrupt = ref false let steps = ref 0 -let are_we_threading = lazy ( - match !Flags.async_proofs_mode with - | Flags.APon -> true - | _ -> false) +let enable_thread_delay = ref false let check_for_interrupt () = if !interrupt then begin interrupt := false; raise Sys.Break end; incr steps; - if !steps = 1000 && Lazy.force are_we_threading then begin + if !enable_thread_delay && !steps = 1000 then begin Thread.delay 0.001; steps := 0; end diff --git a/lib/control.mli b/lib/control.mli index f6c63ffb3..261b07693 100644 --- a/lib/control.mli +++ b/lib/control.mli @@ -8,6 +8,9 @@ (** Global control of Coq. *) +(** Will periodically call [Thread.delay] if set to true *) +val enable_thread_delay : bool ref + val interrupt : bool ref (** Coq interruption: set the following boolean reference to interrupt Coq (it eventually raises [Break], simulating a Ctrl-C) *) diff --git a/lib/flags.ml b/lib/flags.ml index ddc8f8482..b43d5f74d 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -35,36 +35,10 @@ let record_aux_file = ref false let test_mode = ref false -type async_proofs = APoff | APonLazy | APon -let async_proofs_mode = ref APoff -type cache = Force -let async_proofs_cache = ref None -let async_proofs_n_workers = ref 1 -let async_proofs_n_tacworkers = ref 2 -let async_proofs_private_flags = ref None -let async_proofs_full = 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") -type tac_error_filter = [ `None | `Only of string list | `All ] -let async_proofs_tac_error_resilience = ref (`Only [ "curly" ]) -let async_proofs_cmd_error_resilience = ref true - -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 0.03 +let async_proofs_is_worker () = !async_proofs_worker_id <> "master" let debug = ref false -let stm_debug = ref false let in_debugger = ref false let in_toplevel = ref false diff --git a/lib/flags.mli b/lib/flags.mli index c4afb8318..b82fe6128 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -21,35 +21,14 @@ val record_aux_file : bool ref val test_mode : bool ref (** Async-related flags *) -type async_proofs = APoff | APonLazy | APon -val async_proofs_mode : async_proofs ref -type cache = Force -val async_proofs_cache : cache option ref -val async_proofs_n_workers : int ref -val async_proofs_n_tacworkers : int ref -val async_proofs_private_flags : string option ref -val async_proofs_is_worker : unit -> bool -val async_proofs_is_master : unit -> bool -val async_proofs_full : 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 -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 async_proofs_is_worker : unit -> bool +(** Debug flags *) val debug : bool ref val in_debugger : bool ref val in_toplevel : bool ref -(** Enable STM debugging *) -val stm_debug : bool ref - val profile : bool (* -ide_slave: printing will be more verbose, will affect stm caching *) diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 28c16a656..26aef5355 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -11,10 +11,10 @@ open Pp open Util let stm_pr_err pp = Format.eprintf "%s] @[%a@]\n%!" (Spawned.process_id ()) Pp.pp_with pp - let stm_prerr_endline s = if !Flags.debug then begin stm_pr_err (str s) end else () type cancel_switch = bool ref +let async_proofs_flags_for_workers = ref [] module type Task = sig @@ -117,12 +117,12 @@ module Make(T : Task) () = struct let name = Printf.sprintf "%s:%d" !T.name id in let proc, ic, oc = let rec set_slave_opt = function - | [] -> !Flags.async_proofs_flags_for_workers @ + | [] -> !async_proofs_flags_for_workers @ ["-toploop"; !T.name^"top"; "-worker-id"; name; "-async-proofs-worker-priority"; - Flags.string_of_priority !Flags.async_proofs_worker_priority] - | ("-ideslave"|"-emacs"|"-batch")::tl -> set_slave_opt tl + CoqworkmgrApi.(string_of_priority !WorkerLoop.async_proofs_worker_priority)] + | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl | ("-async-proofs" |"-toploop" |"-vio2vo" |"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv" |"-compile" |"-compile-verbose" diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli index ccd643deb..07689389f 100644 --- a/stm/asyncTaskQueue.mli +++ b/stm/asyncTaskQueue.mli @@ -6,6 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Default flags for workers *) +val async_proofs_flags_for_workers : string list ref + (** This file provides an API for defining and managing a queue of tasks to be done by external workers. diff --git a/stm/coqworkmgrApi.ml b/stm/coqworkmgrApi.ml index 6d6a198c5..14fd97a6d 100644 --- a/stm/coqworkmgrApi.ml +++ b/stm/coqworkmgrApi.ml @@ -8,8 +8,15 @@ let debug = false +type priority = Low | High +let string_of_priority = function Low -> "low" | High -> "high" +let priority_of_string = function + | "low" -> Low + | "high" -> High + | _ -> raise (Invalid_argument "priority_of_string") + type request = - | Hello of Flags.priority + | Hello of priority | Get of int | TryGet of int | GiveBack of int @@ -36,8 +43,8 @@ let positive_int_of_string n = 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 + | [ "HELLO"; "LOW" ] -> Hello Low + | [ "HELLO"; "HIGH" ] -> Hello 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) @@ -57,8 +64,8 @@ let parse_response s = | _ -> raise ParseError let print_request = function - | Hello Flags.Low -> "HELLO LOW\n" - | Hello Flags.High -> "HELLO HIGH\n" + | Hello Low -> "HELLO LOW\n" + | Hello 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 @@ -106,8 +113,7 @@ let with_manager f g = let get n = with_manager - (fun () -> - min n (min !Flags.async_proofs_n_workers !Flags.async_proofs_n_tacworkers)) + (fun () -> n) (fun cin cout -> output_string cout (print_request (Get n)); flush cout; @@ -118,10 +124,7 @@ let get n = let tryget n = with_manager - (fun () -> - Some - (min n - (min !Flags.async_proofs_n_workers !Flags.async_proofs_n_tacworkers))) + (fun () -> Some n) (fun cin cout -> output_string cout (print_request (TryGet n)); flush cout; diff --git a/stm/coqworkmgrApi.mli b/stm/coqworkmgrApi.mli index 70d4173ae..953903810 100644 --- a/stm/coqworkmgrApi.mli +++ b/stm/coqworkmgrApi.mli @@ -8,9 +8,13 @@ (* High level api for clients of the service (like coqtop) *) +type priority = Low | High +val string_of_priority : priority -> string +val priority_of_string : string -> priority + (* 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 +val init : priority -> unit (* blocking *) val get : int -> int @@ -21,7 +25,7 @@ val giveback : int -> unit (* Low level *) type request = - | Hello of Flags.priority + | Hello of priority | Get of int | TryGet of int | GiveBack of int diff --git a/stm/stm.ml b/stm/stm.ml index 877263096..b79a4a939 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -8,13 +8,13 @@ (* enable in case of stm problems *) (* let stm_debug () = !Flags.debug *) -let stm_debug () = !Flags.stm_debug +let stm_debug = ref false let stm_pr_err s = Format.eprintf "%s] %s\n%!" (Spawned.process_id ()) s let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n%!" (Spawned.process_id ()) Pp.pp_with pp -let stm_prerr_endline s = if stm_debug () then begin stm_pr_err (s ()) end else () -let stm_pperr_endline s = if stm_debug () then begin stm_pp_err (s ()) end else () +let stm_prerr_endline s = if !stm_debug then begin stm_pr_err (s ()) end else () +let stm_pperr_endline s = if !stm_debug then begin stm_pp_err (s ()) end else () let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else () @@ -23,6 +23,35 @@ open CErrors open Feedback open Vernacexpr +module AsyncOpts = struct + + let async_proofs_n_workers = ref 1 + let async_proofs_n_tacworkers = ref 2 + + type cache = Force + let async_proofs_cache : cache option ref = ref None + + type async_proofs = APoff | APonLazy | APon + let async_proofs_mode = ref APoff + + let async_proofs_private_flags = ref None + let async_proofs_full = ref false + let async_proofs_never_reopen_branch = ref false + + type tac_error_filter = [ `None | `Only of string list | `All ] + let async_proofs_tac_error_resilience = ref (`Only [ "curly" ]) + let async_proofs_cmd_error_resilience = ref true + + let async_proofs_delegation_threshold = ref 0.03 + +end + +open AsyncOpts + +let async_proofs_is_master () = + !async_proofs_mode = APon && + !Flags.async_proofs_worker_id = "master" + (* Protect against state changes *) let stm_purify f x = let st = Vernacstate.freeze_interp_state `No in @@ -352,7 +381,7 @@ end = struct (* {{{ *) In case you are hitting the race enable stm_debug. *) - if stm_debug () then Flags.we_are_parsing := false; + if !stm_debug then Flags.we_are_parsing := false; let fname = "stm_" ^ Str.global_replace (Str.regexp " ") "_" (Spawned.process_id ()) in @@ -529,7 +558,7 @@ end = struct (* {{{ *) | None -> raise Vcs_aux.Expired let set_state id s = (get_info id).state <- s; - if Flags.async_proofs_is_master () then Hooks.(call state_ready id) + if async_proofs_is_master () then Hooks.(call state_ready id) let get_state id = (get_info id).state let reached id = let info = get_info id in @@ -1105,7 +1134,7 @@ end = struct (* {{{ *) " the \"-async-proofs-cache force\" option to Coq.")) let undo_vernac_classifier v = - if VCS.is_interactive () = `No && !Flags.async_proofs_cache <> Some Flags.Force + if VCS.is_interactive () = `No && !async_proofs_cache <> Some Force then undo_costly_in_batch_mode v; try match v with @@ -1241,7 +1270,7 @@ let prev_node { id } = let cur_node id = mk_doc_node id (VCS.visit id) let is_block_name_enabled name = - match !Flags.async_proofs_tac_error_resilience with + match !async_proofs_tac_error_resilience with | `None -> false | `All -> true | `Only l -> List.mem name l @@ -1249,7 +1278,7 @@ let is_block_name_enabled name = let detect_proof_block id name = let name = match name with None -> "indent" | Some x -> x in if is_block_name_enabled name && - (Flags.async_proofs_is_master () || Flags.async_proofs_is_worker ()) + (async_proofs_is_master () || Flags.async_proofs_is_worker ()) then ( match cur_node id with | None -> () @@ -1351,7 +1380,7 @@ end = struct (* {{{ *) let task_match age t = match age, t with | Fresh, BuildProof { t_states } -> - not !Flags.async_proofs_full || + not !async_proofs_full || List.exists (fun x -> CList.mem_f Stateid.equal x !perspective) t_states | Old my_states, States l -> List.for_all (fun x -> CList.mem_f Stateid.equal x my_states) l @@ -1388,7 +1417,7 @@ end = struct (* {{{ *) feedback (InProgress ~-1); t_assign (`Val pl); record_pb_time ?loc:t_loc t_name time; - if !Flags.async_proofs_full || t_drop + if !async_proofs_full || t_drop then `Stay(t_states,[States t_states]) else `End | Fresh, BuildProof { t_assign; t_loc; t_name; t_states }, @@ -1562,8 +1591,8 @@ end = struct (* {{{ *) let queue = ref None let init () = - if Flags.async_proofs_is_master () then - queue := Some (TaskQueue.create !Flags.async_proofs_n_workers) + if async_proofs_is_master () then + queue := Some (TaskQueue.create !async_proofs_n_workers) else queue := Some (TaskQueue.create 0) @@ -2028,7 +2057,7 @@ end = struct (* {{{ *) QueryTask.({ t_where = prev; t_for = id; t_what = q }) ~cancel_switch let init () = queue := Some (TaskQueue.create - (if !Flags.async_proofs_full then 1 else 0)) + (if !async_proofs_full then 1 else 0)) end (* }}} *) @@ -2051,9 +2080,9 @@ let async_policy () = (VCS.is_vio_doc () || !async_proofs_mode <> APoff) let delegate name = - get_hint_bp_time name >= !Flags.async_proofs_delegation_threshold + get_hint_bp_time name >= !async_proofs_delegation_threshold || VCS.is_vio_doc () - || !Flags.async_proofs_full + || !async_proofs_full let warn_deprecated_nested_proofs = CWarnings.create ~name:"deprecated-nested-proofs" ~category:"deprecated" @@ -2150,7 +2179,7 @@ let collect_proof keep cur hd brkind id = let rc = collect (Some cur) [] id in if is_empty rc then make_sync `AlreadyEvaluated rc else if (keep == VtKeep || keep == VtKeepAsAxiom) && - (not(State.is_cached_and_valid id) || !Flags.async_proofs_full) + (not(State.is_cached_and_valid id) || !async_proofs_full) then check_policy rc else make_sync `AlreadyEvaluated rc @@ -2232,9 +2261,9 @@ let known_state ?(redefine_qed=false) ~cache id = (* Absorb tactic errors from f () *) let resilient_tactic id blockname f = - if !Flags.async_proofs_tac_error_resilience = `None || - (Flags.async_proofs_is_master () && - !Flags.async_proofs_mode = Flags.APoff) + if !async_proofs_tac_error_resilience = `None || + (async_proofs_is_master () && + !async_proofs_mode = APoff) then f () else try f () @@ -2243,9 +2272,9 @@ let known_state ?(redefine_qed=false) ~cache id = error_absorbing_tactic id blockname ie in (* Absorb errors from f x *) let resilient_command f x = - if not !Flags.async_proofs_cmd_error_resilience || - (Flags.async_proofs_is_master () && - !Flags.async_proofs_mode = Flags.APoff) + if not !async_proofs_cmd_error_resilience || + (async_proofs_is_master () && + !async_proofs_mode = APoff) then f x else try f x @@ -2287,10 +2316,10 @@ let known_state ?(redefine_qed=false) ~cache id = resilient_tactic id cblock (fun () -> reach ~cache:`Shallow view.next; Partac.vernac_interp ~solve ~abstract ~cancel_switch - !Flags.async_proofs_n_tacworkers view.next id x) + !async_proofs_n_tacworkers view.next id x) ), cache, true | `Cmd { cast = x; cqueue = `QueryQueue cancel_switch } - when Flags.async_proofs_is_master () -> (fun () -> + when async_proofs_is_master () -> (fun () -> reach view.next; Query.vernac_interp ~cancel_switch view.next id x ), cache, false @@ -2304,10 +2333,10 @@ let known_state ?(redefine_qed=false) ~cache id = if eff then update_global_env () ), (if eff then `Yes else cache), true | `Cmd { cast = x; ceff = eff } -> (fun () -> - (match !Flags.async_proofs_mode with - | Flags.APon | Flags.APonLazy -> + (match !async_proofs_mode with + | APon | APonLazy -> resilient_command reach view.next - | Flags.APoff -> reach view.next); + | APoff -> reach view.next); let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); if eff then update_global_env () @@ -2434,7 +2463,7 @@ let known_state ?(redefine_qed=false) ~cache id = ), cache, true in let cache_step = - if !Flags.async_proofs_cache = Some Flags.Force then `Yes + if !async_proofs_cache = Some Force then `Yes else cache_step in State.define ?safe_id ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id; @@ -2465,6 +2494,7 @@ let doc_type_module_name (std : stm_doc_type) = *) let init_core () = + if !async_proofs_mode = APon then Control.enable_thread_delay := true; State.register_root_state () let new_doc { doc_type ; require_libs } = @@ -2503,10 +2533,10 @@ let new_doc { doc_type ; require_libs } = State.define ~cache:`Yes ~redefine:true (fun () -> ()) Stateid.initial; Backtrack.record (); Slaves.init (); - if Flags.async_proofs_is_master () then begin + if async_proofs_is_master () then begin stm_prerr_endline (fun () -> "Initializing workers"); Query.init (); - let opts = match !Flags.async_proofs_private_flags with + let opts = match !async_proofs_private_flags with | None -> [] | Some s -> Str.split_delim (Str.regexp ",") s in begin try @@ -2705,7 +2735,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) | VtQuery (true, route), w -> let id = VCS.new_node ~id:newtip () in let queue = - if !Flags.async_proofs_full then `QueryQueue (ref false) + if !async_proofs_full then `QueryQueue (ref false) else if VCS.is_vio_doc () && VCS.((get_branch head).kind = `Master) && may_pierce_opaque x @@ -2870,7 +2900,7 @@ let parse_sentence ~doc sid pa = (str "Currently, the parsing api only supports parsing at the tip of the document." ++ fnl () ++ str "You wanted to parse at: " ++ str (Stateid.to_string sid) ++ str " but the current tip is: " ++ str (Stateid.to_string cur_tip)) ; - if not (Stateid.equal sid real_tip) && !Flags.debug && stm_debug () then + if not (Stateid.equal sid real_tip) && !Flags.debug && !stm_debug then Feedback.msg_debug (str "Warning, the real tip doesn't match the current tip." ++ str "You wanted to parse at: " ++ str (Stateid.to_string sid) ++ @@ -3029,7 +3059,7 @@ let edit_at ~doc id = VCS.delete_boxes_of id; VCS.gc (); VCS.print (); - if not !Flags.async_proofs_full then + if not !async_proofs_full then Reach.known_state ~cache:(VCS.is_interactive ()) id; VCS.checkout_shallowest_proof_branch (); `NewTip in @@ -3045,7 +3075,7 @@ let edit_at ~doc id = | _, Some _, None -> assert false | false, Some { qed = qed_id ; lemma = start }, Some(mode,bn) -> let tip = VCS.cur_tip () in - if has_failed qed_id && is_pure qed_id && not !Flags.async_proofs_never_reopen_branch + if has_failed qed_id && is_pure qed_id && not !async_proofs_never_reopen_branch then reopen_branch start id mode qed_id tip bn else backto id (Some bn) | true, Some { qed = qed_id }, Some(mode,bn) -> diff --git a/stm/stm.mli b/stm/stm.mli index 9fd35a0d3..ef95be0e4 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -225,3 +225,30 @@ val state_of_id : doc:doc -> (* Queries for backward compatibility *) val current_proof_depth : doc:doc -> int val get_all_proof_names : doc:doc -> Id.t list + +(** Enable STM debugging *) +val stm_debug : bool ref + +(* Flags *) +module AsyncOpts : sig + + (* Defaults for worker creation *) + val async_proofs_n_workers : int ref + val async_proofs_n_tacworkers : int ref + + type async_proofs = APoff | APonLazy | APon + val async_proofs_mode : async_proofs ref + + type cache = Force + val async_proofs_cache : cache option ref + + val async_proofs_private_flags : string option ref + val async_proofs_full : bool ref + val async_proofs_never_reopen_branch : bool ref + + 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 + +end diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml index 64121eb3d..704119186 100644 --- a/stm/workerLoop.ml +++ b/stm/workerLoop.ml @@ -6,6 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Default priority *) +open CoqworkmgrApi +let async_proofs_worker_priority = ref Low + let rec parse = function | "--xml_format=Ppcmds" :: rest -> parse rest | x :: rest -> x :: parse rest @@ -15,5 +19,5 @@ let loop init args = let args = parse args in Flags.quiet := true; init (); - CoqworkmgrApi.init !Flags.async_proofs_worker_priority; + CoqworkmgrApi.init !async_proofs_worker_priority; args diff --git a/stm/workerLoop.mli b/stm/workerLoop.mli index 53f745935..da2e6fe0c 100644 --- a/stm/workerLoop.mli +++ b/stm/workerLoop.mli @@ -6,4 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Default priority *) +val async_proofs_worker_priority : CoqworkmgrApi.priority ref + val loop : (unit -> unit) -> string list -> string list diff --git a/tools/coqworkmgr.ml b/tools/coqworkmgr.ml index e1d1c60d7..f4777c4fb 100644 --- a/tools/coqworkmgr.ml +++ b/tools/coqworkmgr.ml @@ -14,7 +14,7 @@ type party = { sock : Unix.file_descr; cout : out_channel; mutable tokens : int; - priority : Flags.priority; + priority : priority; } let answer party msg = @@ -42,10 +42,10 @@ end = struct let is_empty q = !q = [] let rec split acc = function | [] -> List.rev acc, [] - | (_, { priority = Flags.Low }) :: _ as l -> List.rev acc, l + | (_, { priority = 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] + if priority = Low then q := !q @ [item] else let high, low = split [] !q in q := high @ (item :: low) @@ -148,7 +148,7 @@ let check_alive s = | 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 (Hello Low)); flush cout; output_string cout (print_request Ping); flush cout; begin match Unix.select [s] [] [] 1.0 with | [s],_,_ -> diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 553da2dc0..6048dae3b 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -71,7 +71,7 @@ let init_color () = let toploop_init = ref begin fun x -> let () = init_color () in - let () = CoqworkmgrApi.(init !Flags.async_proofs_worker_priority) in + let () = CoqworkmgrApi.init !WorkerLoop.async_proofs_worker_priority in x end @@ -529,18 +529,18 @@ let print_config = ref false let print_tags = ref false let get_priority opt s = - try Flags.priority_of_string s + try CoqworkmgrApi.priority_of_string s with Invalid_argument _ -> prerr_endline ("Error: low/high expected after "^opt); exit 1 -let get_async_proofs_mode opt = function - | "no" | "off" -> Flags.APoff - | "yes" | "on" -> Flags.APon - | "lazy" -> Flags.APonLazy +let get_async_proofs_mode opt = let open Stm.AsyncOpts in function + | "no" | "off" -> APoff + | "yes" | "on" -> APon + | "lazy" -> APonLazy | _ -> prerr_endline ("Error: on/off/lazy expected after "^opt); exit 1 let get_cache opt = function - | "force" -> Some Flags.Force + | "force" -> Some Stm.AsyncOpts.Force | _ -> prerr_endline ("Error: force expected after "^opt); exit 1 @@ -649,23 +649,23 @@ let parse_args arglist = (* Options with one arg *) |"-coqlib" -> Flags.coqlib_spec:=true; Flags.coqlib:=(next ()) |"-async-proofs" -> - Flags.async_proofs_mode := get_async_proofs_mode opt (next()) + Stm.AsyncOpts.async_proofs_mode := get_async_proofs_mode opt (next()) |"-async-proofs-j" -> - Flags.async_proofs_n_workers := (get_int opt (next ())) + Stm.AsyncOpts.async_proofs_n_workers := (get_int opt (next ())) |"-async-proofs-cache" -> - Flags.async_proofs_cache := get_cache opt (next ()) + Stm.AsyncOpts.async_proofs_cache := get_cache opt (next ()) |"-async-proofs-tac-j" -> - Flags.async_proofs_n_tacworkers := (get_int opt (next ())) + Stm.AsyncOpts.async_proofs_n_tacworkers := (get_int opt (next ())) |"-async-proofs-worker-priority" -> - Flags.async_proofs_worker_priority := get_priority opt (next ()) + WorkerLoop.async_proofs_worker_priority := get_priority opt (next ()) |"-async-proofs-private-flags" -> - Flags.async_proofs_private_flags := Some (next ()); + Stm.AsyncOpts.async_proofs_private_flags := Some (next ()); |"-async-proofs-tactic-error-resilience" -> - Flags.async_proofs_tac_error_resilience := get_error_resilience opt (next ()) + Stm.AsyncOpts.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 ()) + Stm.AsyncOpts.async_proofs_cmd_error_resilience := get_bool opt (next ()) |"-async-proofs-delegation-threshold" -> - Flags.async_proofs_delegation_threshold:= get_float opt (next ()) + Stm.AsyncOpts.async_proofs_delegation_threshold:= get_float opt (next ()) |"-worker-id" -> set_worker_id opt (next ()) |"-compat" -> let v = G_vernac.parse_compat_version ~allow_old:false (next ()) in @@ -705,9 +705,9 @@ let parse_args arglist = |"-async-queries-always-delegate" |"-async-proofs-always-delegate" |"-async-proofs-full" -> - Flags.async_proofs_full := true; + Stm.AsyncOpts.async_proofs_full := true; |"-async-proofs-never-reopen-branch" -> - Flags.async_proofs_never_reopen_branch := true; + Stm.AsyncOpts.async_proofs_never_reopen_branch := true; |"-batch" -> set_batch_mode () |"-test-mode" -> Flags.test_mode := true |"-beautify" -> Flags.beautify := true @@ -716,7 +716,7 @@ let parse_args arglist = |"-color" -> set_color (next ()) |"-config"|"--config" -> print_config := true |"-debug" -> Coqinit.set_debug () - |"-stm-debug" -> Flags.stm_debug := true + |"-stm-debug" -> Stm.stm_debug := true |"-emacs" -> set_emacs () |"-filteropts" -> filter_opts := true |"-h"|"-H"|"-?"|"-help"|"--help" -> usage !batch_mode |