diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 37 | ||||
| -rw-r--r-- | stm/proofworkertop.ml | 6 | ||||
| -rw-r--r-- | stm/queryworkertop.ml | 6 | ||||
| -rw-r--r-- | stm/stm.ml | 78 | ||||
| -rw-r--r-- | stm/stm.mllib | 1 | ||||
| -rw-r--r-- | stm/tacworkertop.ml | 6 | ||||
| -rw-r--r-- | stm/workerLoop.ml | 19 | ||||
| -rw-r--r-- | stm/workerLoop.mli | 9 |
8 files changed, 84 insertions, 78 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 8acc3c233a..1254919880 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -10,9 +10,9 @@ open CErrors open Pp open Util -let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr +let stm_pr_err pp = Format.eprintf "%s] @[%a@]%!\n" (System.process_id ()) Pp.pp_with pp -let prerr_endline s = if !Flags.debug then begin pr_err s end else () +let stm_prerr_endline s = if !Flags.debug then begin stm_pr_err (str s) end else () type 'a worker_status = [ `Fresh | `Old of 'a ] @@ -147,23 +147,23 @@ module Make(T : Task) = struct let stop_waiting = ref false in let expiration_date = ref (ref false) in let pick_task () = - prerr_endline "waiting for a task"; + stm_prerr_endline "waiting for a task"; let pick age (t, c) = not !c && T.task_match age t in let task, task_expiration = TQueue.pop ~picky:(pick !worker_age) ~destroy:stop_waiting queue in expiration_date := task_expiration; last_task := Some task; - prerr_endline ("got task: "^T.name_of_task task); + stm_prerr_endline ("got task: " ^ T.name_of_task task); task in let add_tasks l = List.iter (fun t -> TQueue.push queue (t,!expiration_date)) l in let get_exec_token () = ignore(CoqworkmgrApi.get 1); got_token := true; - prerr_endline ("got execution token") in + stm_prerr_endline ("got execution token") in let kill proc = Worker.kill proc; - prerr_endline ("Worker exited: " ^ + stm_prerr_endline ("Worker exited: " ^ match Worker.wait proc with | Unix.WEXITED 0x400 -> "exit code unavailable" | Unix.WEXITED i -> Printf.sprintf "exit(%d)" i @@ -196,7 +196,7 @@ module Make(T : Task) = struct report_status ~id "Idle"; let task = pick_task () in match T.request_of_task !worker_age task with - | None -> prerr_endline ("Task expired: " ^ T.name_of_task task) + | None -> stm_prerr_endline ("Task expired: " ^ T.name_of_task task) | Some req -> try get_exec_token (); @@ -222,8 +222,7 @@ module Make(T : Task) = struct raise e (* we pass the exception to the external handler *) | MarshalError s -> T.on_marshal_error s task; raise Die | e -> - pr_err ("Uncaught exception in worker manager: "^ - string_of_ppcmds (print e)); + stm_pr_err Pp.(seq [str "Uncaught exception in worker manager: "; print e]); flush_all (); raise Die done with | (Die | TQueue.BeingDestroyed) -> @@ -261,7 +260,7 @@ module Make(T : Task) = struct let broadcast { queue } = TQueue.broadcast queue let enqueue_task { queue; active } (t, _ as item) = - prerr_endline ("Enqueue task "^T.name_of_task t); + stm_prerr_endline ("Enqueue task "^T.name_of_task t); TQueue.push queue item let cancel_worker { active } n = Pool.cancel n active @@ -298,18 +297,11 @@ module Make(T : Task) = struct let slave_handshake () = Pool.worker_handshake (Option.get !slave_ic) (Option.get !slave_oc) - let pp_pid pp = - (* Breaking all abstraction barriers... very nice *) - let get_xml pp = match Richpp.repr pp with - | Xml_datatype.Element("_", [], xml) -> xml - | _ -> assert false in - Richpp.richpp_of_xml (Xml_datatype.Element("_", [], - get_xml (Richpp.richpp_of_pp Pp.(str (System.process_id ()^ " "))) @ - get_xml pp)) + let pp_pid pp = Pp.(str (System.process_id () ^ " ") ++ pp) let debug_with_pid = Feedback.(function | { contents = Message(Debug, loc, pp) } as fb -> - { fb with contents = Message(Debug,loc,pp_pid pp) } + { fb with contents = Message(Debug,loc, pp_pid pp) } | x -> x) let main_loop () = @@ -317,7 +309,6 @@ module Make(T : Task) = struct let slave_feeder oc fb = Marshal.to_channel oc (RespFeedback (debug_with_pid fb)) []; flush oc in Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x); - Feedback.set_logger Feedback.feedback_logger; (* We ask master to allocate universe identifiers *) Universes.set_remote_new_univ_level (bufferize (fun () -> marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel; @@ -337,11 +328,11 @@ module Make(T : Task) = struct CEphemeron.clear () with | MarshalError s -> - pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2 + stm_pr_err Pp.(prlist str ["Fatal marshal error: "; s]); flush_all (); exit 2 | End_of_file -> - prerr_endline "connection lost"; flush_all (); exit 2 + stm_prerr_endline "connection lost"; flush_all (); exit 2 | e -> - pr_err ("Slave: critical exception: " ^ Pp.string_of_ppcmds (print e)); + stm_pr_err Pp.(seq [str "Slave: critical exception: "; print e]); flush_all (); exit 1 done diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml index 23538a467e..0d2f9cb747 100644 --- a/stm/proofworkertop.ml +++ b/stm/proofworkertop.ml @@ -8,11 +8,7 @@ module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask) -let () = Coqtop.toploop_init := (fun args -> - Flags.make_silent true; - W.init_stdout (); - CoqworkmgrApi.init !Flags.async_proofs_worker_priority; - args) +let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout let () = Coqtop.toploop_run := W.main_loop diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml index fff6d55434..9d30473739 100644 --- a/stm/queryworkertop.ml +++ b/stm/queryworkertop.ml @@ -8,11 +8,7 @@ module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask) -let () = Coqtop.toploop_init := (fun args -> - Flags.make_silent true; - W.init_stdout (); - CoqworkmgrApi.init !Flags.async_proofs_worker_priority; - args) +let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout let () = Coqtop.toploop_run := W.main_loop diff --git a/stm/stm.ml b/stm/stm.ml index e698d1c72e..b9dbb78917 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -6,14 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr +let stm_pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr +let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n" (System.process_id ()) Pp.pp_with pp; flush stderr -let prerr_endline s = if false then begin pr_err (s ()) end else () -let prerr_debug s = if !Flags.debug then begin pr_err (s ()) end else () +let stm_prerr_endline s = if false then begin stm_pr_err (s ()) end else () +let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else () -(* Opening ppvernac below aliases Richpp, see PR#185 *) -let pp_to_richpp = Richpp.richpp_of_pp -let str_to_richpp = Richpp.richpp_of_string +let stm_pperr_endline s = if false then begin stm_pp_err (s ()) end else () open Vernacexpr open CErrors @@ -26,7 +25,7 @@ open Feedback let execution_error state_id loc msg = feedback ~id:(State state_id) - (Message (Error, Some loc, pp_to_richpp msg)) + (Message (Error, Some loc, msg)) module Hooks = struct @@ -48,7 +47,7 @@ let forward_feedback, forward_feedback_hook = let parse_error, parse_error_hook = Hook.make ~default:(fun id loc msg -> - feedback ~id (Message(Error, Some loc, pp_to_richpp msg))) () + feedback ~id (Message(Error, Some loc, msg))) () let unreachable_state, unreachable_state_hook = Hook.make ~default:(fun _ _ -> ()) () @@ -544,7 +543,7 @@ end = struct (* {{{ *) let branch, mode = match Vcs_aux.find_proof_at_depth !vcs pl with | h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in checkout branch; - prerr_endline (fun () -> "mode:" ^ mode); + stm_prerr_endline (fun () -> "mode:" ^ mode); Proof_global.activate_proof_mode mode with Failure _ -> checkout Branch.master; @@ -856,7 +855,7 @@ end = struct (* {{{ *) if is_cached id && not redefine then anomaly (str"defining state "++str str_id++str" twice"); try - prerr_endline (fun () -> "defining "^str_id^" (cache="^ + stm_prerr_endline (fun () -> "defining "^str_id^" (cache="^ if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)"); let good_id = match safe_id with None -> !cur_id | Some id -> id in fix_exn_ref := exn_on id ~valid:good_id; @@ -864,7 +863,7 @@ end = struct (* {{{ *) fix_exn_ref := (fun x -> x); if cache = `Yes then freeze `No id else if cache = `Shallow then freeze `Shallow id; - prerr_endline (fun () -> "setting cur id to "^str_id); + stm_prerr_endline (fun () -> "setting cur id to "^str_id); cur_id := id; if feedback_processed then Hooks.(call state_computed id ~in_cache:false); @@ -998,11 +997,11 @@ let stm_vernac_interp ?proof id ?route { verbose; loc; expr } = in let aux_interp cmd = if is_filtered_command cmd then - prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr)) + stm_pperr_endline Pp.(fun () -> str "ignoring " ++ pr_vernac expr) else match cmd with | VernacShow ShowScript -> ShowScript.show_script () | expr -> - prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr)); + stm_pperr_endline Pp.(fun () -> str "interpreting " ++ pr_vernac expr); try Vernacentries.interp ?verbosely:(Some verbose) ?proof (loc, expr) with e -> let e = CErrors.push e in @@ -1435,11 +1434,10 @@ end = struct (* {{{ *) | Some (safe, err) -> err, safe | None -> Stateid.dummy, Stateid.dummy in let e_msg = iprint (e, info) in - prerr_endline (fun () -> "failed with the following exception:"); - prerr_endline (fun () -> string_of_ppcmds e_msg); + stm_pperr_endline Pp.(fun () -> str "failed with the following exception: " ++ fnl () ++ e_msg); let e_safe_states = List.filter State.is_cached_and_valid my_states in RespError { e_error_at; e_safe_id; e_msg; e_safe_states } - + let perform_states query = if query = [] then [] else let is_tac e = match classify_vernac e with @@ -1618,9 +1616,9 @@ end = struct (* {{{ *) Future.from_val (Option.get (Global.body_of_constant_body c)) in let uc = Future.chain - ~greedy:true ~pure:true uc Univ.hcons_universe_context_set in - let pr = Future.chain ~greedy:true ~pure:true pr discharge in - let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in + ~pure:true uc Univ.hcons_universe_context_set in + let pr = Future.chain ~pure:true pr discharge in + let pr = Future.chain ~pure:true pr Constr.hcons in Future.sink pr; let extra = Future.join uc in u.(bucket) <- uc; @@ -1701,7 +1699,7 @@ end = struct (* {{{ *) | Some (ReqBuildProof (r, b, _)) -> Some(r, b) | _ -> None) tasks in - prerr_endline (fun () -> Printf.sprintf "dumping %d tasks\n" (List.length reqs)); + stm_prerr_endline (fun () -> Printf.sprintf "dumping %d tasks\n" (List.length reqs)); reqs let reset_task_queue () = TaskQueue.clear (Option.get !queue) @@ -1785,7 +1783,7 @@ end = struct (* {{{ *) `Stay ((),[]) let on_marshal_error err { t_name } = - pr_err ("Fatal marshal error: " ^ t_name ); + stm_pr_err ("Fatal marshal error: " ^ t_name ); flush_all (); exit 1 let on_task_cancellation_or_expiration_or_slave_death = function @@ -1884,10 +1882,10 @@ end = struct (* {{{ *) let open Notations in try let pt, uc = Future.join f in - prerr_endline (fun () -> string_of_ppcmds(hov 0 ( + stm_pperr_endline (fun () -> hov 0 ( str"g=" ++ int (Evar.repr gid) ++ spc () ++ str"t=" ++ (Printer.pr_constr pt) ++ spc () ++ - str"uc=" ++ Evd.pr_evar_universe_context uc))); + str"uc=" ++ Evd.pr_evar_universe_context uc)); (if abstract then Tactics.tclABSTRACT None else (fun x -> x)) (V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*> Tactics.exact_no_check pt) @@ -1929,7 +1927,7 @@ end = struct (* {{{ *) let use_response _ _ _ = `End let on_marshal_error _ _ = - pr_err ("Fatal marshal error in query"); + stm_pr_err ("Fatal marshal error in query"); flush_all (); exit 1 let on_task_cancellation_or_expiration_or_slave_death _ = () @@ -1945,7 +1943,7 @@ end = struct (* {{{ *) feedback ~id:(State r_for) Processed with e when CErrors.noncritical e -> let e = CErrors.push e in - let msg = pp_to_richpp (iprint e) in + let msg = iprint e in feedback ~id:(State r_for) (Message (Error, None, msg)) let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what) @@ -2004,7 +2002,7 @@ let warn_deprecated_nested_proofs = "stop working in a future Coq version")) let collect_proof keep cur hd brkind id = - prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id); + stm_prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id); let no_name = "" in let name = function | [] -> no_name @@ -2104,7 +2102,7 @@ let string_of_reason = function | `NoPU_NoHint_NoES -> "no 'Proof using..', no .aux file, inside a section" | `Unknown -> "unsupported case" -let log_string s = prerr_debug (fun () -> "STM: " ^ s) +let log_string s = stm_prerr_debug (fun () -> "STM: " ^ s) let log_processing_async id name = log_string Printf.(sprintf "%s: proof %s: asynch" (Stateid.to_string id) name ) @@ -2191,16 +2189,16 @@ let known_state ?(redefine_qed=false) ~cache id = Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env () in let rec pure_cherry_pick_non_pstate safe_id id = Future.purify (fun id -> - prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id); + stm_prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id); reach ~safe_id id; cherry_pick_non_pstate ()) id (* traverses the dag backward from nodes being already calculated *) and reach ?safe_id ?(redefine_qed=false) ?(cache=cache) id = - prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id); + stm_prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id); if not redefine_qed && State.is_cached ~cache id then begin Hooks.(call state_computed id ~in_cache:true); - prerr_endline (fun () -> "reached (cache)"); + stm_prerr_endline (fun () -> "reached (cache)"); State.install_cached id end else let step, cache_step, feedback_processed = @@ -2352,7 +2350,7 @@ let known_state ?(redefine_qed=false) ~cache id = else cache_step in State.define ?safe_id ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id; - prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in + stm_prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in reach ~redefine_qed id end (* }}} *) @@ -2367,7 +2365,7 @@ let init () = Backtrack.record (); Slaves.init (); if Flags.async_proofs_is_master () then begin - prerr_endline (fun () -> "Initializing workers"); + stm_prerr_endline (fun () -> "Initializing workers"); Query.init (); let opts = match !Flags.async_proofs_private_flags with | None -> [] @@ -2419,9 +2417,9 @@ let rec join_admitted_proofs id = let join () = finish (); wait (); - prerr_endline (fun () -> "Joining the environment"); + stm_prerr_endline (fun () -> "Joining the environment"); Global.join_safe_environment (); - prerr_endline (fun () -> "Joining Admitted proofs"); + stm_prerr_endline (fun () -> "Joining Admitted proofs"); join_admitted_proofs (VCS.get_branch_pos (VCS.current_branch ())); VCS.print (); VCS.print () @@ -2495,7 +2493,7 @@ let handle_failure (e, info) vcs tty = anomaly(str"error with no safe_id attached:" ++ spc() ++ CErrors.iprint_no_report (e, info)) | Some (safe_id, id) -> - prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); + stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); VCS.restore vcs; if tty && interactive () = `Yes then begin (* We stay on a valid state *) @@ -2518,13 +2516,13 @@ let reset_task_queue = Slaves.reset_task_queue (* Document building *) let process_transaction ?(newtip=Stateid.fresh ()) ~tty ({ verbose; loc; expr } as x) c = - prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x)); + stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x); let vcs = VCS.backup () in try let head = VCS.current_branch () in VCS.checkout head; let rc = begin - prerr_endline (fun () -> + stm_prerr_endline (fun () -> " classified as: " ^ string_of_vernac_classification c); match c with (* PG stuff *) @@ -2562,7 +2560,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty VCS.commit id (Alias (oid,x)); Backtrack.record (); if w == VtNow then finish (); `Ok | VtStm (VtBack id, false), VtNow -> - prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id); + stm_prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id); Backtrack.backto id; VCS.checkout_shallowest_proof_branch (); Reach.known_state ~cache:(interactive ()) id; `Ok @@ -2712,7 +2710,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty expr = VernacShow (ShowGoal OpenSubgoals) } | _ -> () end; - prerr_endline (fun () -> "processed }}}"); + stm_prerr_endline (fun () -> "processed }}}"); VCS.print (); rc with e -> @@ -2898,7 +2896,7 @@ let edit_at id = anomaly (str ("edit_at "^Stateid.to_string id^": ") ++ CErrors.print_no_report e) | Some (_, id) -> - prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); + stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); VCS.restore vcs; VCS.print (); iraise (e, info) diff --git a/stm/stm.mllib b/stm/stm.mllib index 4b254e8113..72b5380162 100644 --- a/stm/stm.mllib +++ b/stm/stm.mllib @@ -5,6 +5,7 @@ TQueue WorkerPool Vernac_classifier CoqworkmgrApi +WorkerLoop AsyncTaskQueue Stm ProofBlockDelimiter diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml index d5333d1077..256532c6b6 100644 --- a/stm/tacworkertop.ml +++ b/stm/tacworkertop.ml @@ -8,11 +8,7 @@ module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) -let () = Coqtop.toploop_init := (fun args -> - Flags.make_silent true; - W.init_stdout (); - CoqworkmgrApi.init !Flags.async_proofs_worker_priority; - args) +let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout let () = Coqtop.toploop_run := W.main_loop diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml new file mode 100644 index 0000000000..50b42512cb --- /dev/null +++ b/stm/workerLoop.ml @@ -0,0 +1,19 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +let rec parse = function + | "--xml_format=Ppcmds" :: rest -> parse rest + | x :: rest -> x :: parse rest + | [] -> [] + +let loop init args = + let args = parse args in + Flags.make_silent true; + init (); + CoqworkmgrApi.init !Flags.async_proofs_worker_priority; + args diff --git a/stm/workerLoop.mli b/stm/workerLoop.mli new file mode 100644 index 0000000000..dcbf9c88d6 --- /dev/null +++ b/stm/workerLoop.mli @@ -0,0 +1,9 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val loop : (unit -> unit) -> string list -> string list |