diff options
| -rw-r--r-- | ide/coqOps.ml | 10 | ||||
| -rw-r--r-- | lib/feedback.ml | 39 | ||||
| -rw-r--r-- | lib/feedback.mli | 19 | ||||
| -rw-r--r-- | lib/flags.ml | 2 | ||||
| -rw-r--r-- | lib/flags.mli | 3 | ||||
| -rw-r--r-- | lib/pp.ml | 17 | ||||
| -rw-r--r-- | lib/pp.mli | 7 | ||||
| -rw-r--r-- | stm/asyncTaskQueue.ml | 13 | ||||
| -rw-r--r-- | stm/stm.ml | 73 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 1 |
10 files changed, 58 insertions, 126 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 1d1c95aec..63b6bf140 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -336,7 +336,7 @@ object(self) let log s state_id = Minilib.log ("Feedback " ^ s ^ " on " ^ Stateid.to_string (Option.default Stateid.dummy state_id)) in - begin match msg.content, sentence with + begin match msg.contents, sentence with | AddedAxiom, Some (id,sentence) -> log "AddedAxiom" id; remove_flag sentence `PROCESSING; @@ -348,8 +348,8 @@ object(self) remove_flag sentence `PROCESSING; remove_flag sentence `ERROR; self#mark_as_needed sentence - | ProcessingInMaster, Some (id,sentence) -> - log "ProcessingInMaster" id; + | ProcessingIn _, Some (id,sentence) -> + log "ProcessingIn" id; add_flag sentence `PROCESSING; self#mark_as_needed sentence | Incomplete, Some (id, sentence) -> @@ -375,8 +375,8 @@ object(self) | InProgress n, _ -> if n < 0 then processed <- processed + abs n else to_process <- to_process + n - | SlaveStatus(id,status), _ -> - log "SlaveStatus" None; + | WorkerStatus(id,status), _ -> + log "WorkerStatus" None; slaves_status <- CString.Map.add id status slaves_status | _ -> diff --git a/lib/feedback.ml b/lib/feedback.ml index 615886468..4b74078f0 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -58,32 +58,32 @@ type edit_or_state_id = Edit of edit_id | State of state_id type route_id = int type feedback_content = - | AddedAxiom | Processed | Incomplete | Complete - | GlobRef of Loc.t * string * string * string * string - | GlobDef of Loc.t * string * string * string | ErrorMsg of Loc.t * string + | ProcessingIn of string | InProgress of int - | SlaveStatus of string * string - | ProcessingInMaster + | WorkerStatus of string * string | Goals of Loc.t * string - | StructuredGoals of Loc.t * xml + | AddedAxiom + | GlobRef of Loc.t * string * string * string * string + | GlobDef of Loc.t * string * string * string | FileDependency of string option * string | FileLoaded of string * string + | Custom of Loc.t * string * xml | Message of message type feedback = { id : edit_or_state_id; - content : feedback_content; + contents : feedback_content; route : route_id; } let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with | "addedaxiom", _ -> AddedAxiom | "processed", _ -> Processed - | "processinginmaster", _ -> ProcessingInMaster + | "processingin", [where] -> ProcessingIn (to_string where) | "incomplete", _ -> Incomplete | "complete", _ -> Complete | "globref", [loc; filepath; modpath; ident; ty] -> @@ -93,11 +93,11 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with GlobDef(to_loc loc, to_string ident, to_string secpath, to_string ty) | "errormsg", [loc; s] -> ErrorMsg (to_loc loc, to_string s) | "inprogress", [n] -> InProgress (to_int n) - | "slavestatus", [ns] -> + | "workerstatus", [ns] -> let n, s = to_pair to_string to_string ns in - SlaveStatus(n,s) + WorkerStatus(n,s) | "goals", [loc;s] -> Goals (to_loc loc, to_string s) - | "structuredgoals", [loc;x]-> StructuredGoals (to_loc loc, x) + | "custom", [loc;name;x]-> Custom (to_loc loc, to_string name, x) | "filedependency", [from; dep] -> FileDependency (to_option to_string from, to_string dep) | "fileloaded", [dirpath; filename] -> @@ -107,7 +107,8 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with let of_feedback_content = function | AddedAxiom -> constructor "feedback_content" "addedaxiom" [] | Processed -> constructor "feedback_content" "processed" [] - | ProcessingInMaster -> constructor "feedback_content" "processinginmaster" [] + | ProcessingIn where -> + constructor "feedback_content" "processingin" [of_string where] | Incomplete -> constructor "feedback_content" "incomplete" [] | Complete -> constructor "feedback_content" "complete" [] | GlobRef(loc, filepath, modpath, ident, ty) -> @@ -126,13 +127,13 @@ let of_feedback_content = function | ErrorMsg(loc, s) -> constructor "feedback_content" "errormsg" [of_loc loc; of_string s] | InProgress n -> constructor "feedback_content" "inprogress" [of_int n] - | SlaveStatus(n,s) -> - constructor "feedback_content" "slavestatus" + | WorkerStatus(n,s) -> + constructor "feedback_content" "workerstatus" [of_pair of_string of_string (n,s)] | Goals (loc,s) -> constructor "feedback_content" "goals" [of_loc loc;of_string s] - | StructuredGoals (loc, x) -> - constructor "feedback_content" "structuredgoals" [of_loc loc; x] + | Custom (loc, name, x) -> + constructor "feedback_content" "custom" [of_loc loc; of_string name; x] | FileDependency (from, depends_on) -> constructor "feedback_content" "filedependency" [ of_option of_string from; @@ -148,7 +149,7 @@ let of_edit_or_state_id = function | State id -> ["object","state"], Stateid.to_xml id let of_feedback msg = - let content = of_feedback_content msg.content in + let content = of_feedback_content msg.contents in let obj, id = of_edit_or_state_id msg.id in let route = string_of_int msg.route in Element ("feedback", obj @ ["route",route], [id;content]) @@ -156,11 +157,11 @@ let to_feedback xml = match xml with | Element ("feedback", ["object","edit";"route",route], [id;content]) -> { id = Edit(to_edit_id id); route = int_of_string route; - content = to_feedback_content content } + contents = to_feedback_content content } | Element ("feedback", ["object","state";"route",route], [id;content]) -> { id = State(Stateid.of_xml id); route = int_of_string route; - content = to_feedback_content content } + contents = to_feedback_content content } | _ -> raise Marshal_error let is_feedback = function diff --git a/lib/feedback.mli b/lib/feedback.mli index bda15fc58..b7822b27b 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -35,25 +35,30 @@ type route_id = int val default_route : route_id type feedback_content = - | AddedAxiom + (* STM mandatory data (must be displayed) *) | Processed | Incomplete | Complete - | GlobRef of Loc.t * string * string * string * string - | GlobDef of Loc.t * string * string * string | ErrorMsg of Loc.t * string + (* STM optional data *) + | ProcessingIn of string | InProgress of int - | SlaveStatus of string * string - | ProcessingInMaster + | WorkerStatus of string * string + (* Generally useful metadata *) | Goals of Loc.t * string - | StructuredGoals of Loc.t * xml + | AddedAxiom + | GlobRef of Loc.t * string * string * string * string + | GlobDef of Loc.t * string * string * string | FileDependency of string option * string | FileLoaded of string * string + (* Extra metadata *) + | Custom of Loc.t * string * xml + (* Old generic messages *) | Message of message type feedback = { id : edit_or_state_id; (* The document part concerned *) - content : feedback_content; (* The payload *) + contents : feedback_content; (* The payload *) route : route_id; (* Extra routing info *) } diff --git a/lib/flags.ml b/lib/flags.ml index f95c31d9b..bcd7c59d7 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -85,8 +85,6 @@ let coqtop_ui = ref false let ide_slave = ref false let ideslave_coqtop_flags = ref None -let feedback_goals = ref false - let time = ref false let raw_print = ref false diff --git a/lib/flags.mli b/lib/flags.mli index 757563926..716d04163 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -46,9 +46,6 @@ val coqtop_ui : bool ref val ide_slave : bool ref val ideslave_coqtop_flags : string option ref -val feedback_goals : bool ref - - val time : bool ref val we_are_parsing : bool ref @@ -460,17 +460,20 @@ let std_logger lvl msg = std_logger ~id:!feedback_id lvl msg (** Feedback *) let feeder = ref ignore -let set_id_for_feedback ?(route=0) i = feedback_id := i; feedback_route := route -let feedback ?state_id ?route what = +let set_id_for_feedback ?(route=Feedback.default_route) i = + feedback_id := i; feedback_route := route +let feedback ?state_id ?edit_id ?route what = !feeder { - Feedback.content = what; + Feedback.contents = what; Feedback.route = Option.default !feedback_route route; Feedback.id = - match state_id with - | Some id -> Feedback.State id - | None -> !feedback_id; + match state_id, edit_id with + | Some id, _ -> Feedback.State id + | None, Some eid -> Feedback.Edit eid + | None, None -> !feedback_id; } let set_feeder f = feeder := f +let get_id_for_feedback () = !feedback_id, !feedback_route (** Utility *) @@ -480,7 +483,7 @@ let string_of_ppcmds c = let log_via_feedback () = logger := (fun ~id lvl msg -> !feeder { - Feedback.content = Feedback.Message { + Feedback.contents = Feedback.Message { message_level = lvl; message_content = string_of_ppcmds msg }; Feedback.route = !feedback_route; diff --git a/lib/pp.mli b/lib/pp.mli index 0293822da..fd529e1d7 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -160,16 +160,17 @@ val is_message : Xml_datatype.xml -> bool * Morally the parser gets a string and an edit_id, and gives back an AST. * Feedbacks during the parsing phase are attached to this edit_id. * The interpreter assignes an exec_id to the ast, and feedbacks happening - * during interpretation are attached to the exec_id (still unimplemented, - * since the two phases are performed sequentially) *) + * during interpretation are attached to the exec_id. + * Only one among state_id and edit_id can be provided. *) val feedback : - ?state_id:Feedback.state_id -> + ?state_id:Feedback.state_id -> ?edit_id:Feedback.edit_id -> ?route:Feedback.route_id -> Feedback.feedback_content -> unit val set_id_for_feedback : ?route:Feedback.route_id -> Feedback.edit_or_state_id -> unit val set_feeder : (Feedback.feedback -> unit) -> unit +val get_id_for_feedback : unit -> Feedback.edit_or_state_id * Feedback.route_id (** {6 Utilities} *) diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index fa7aa9584..8b4e0844c 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -135,7 +135,7 @@ module Make(T : Task) = struct exception Expired let report_status ?(id = !Flags.async_proofs_worker_id) s = - Pp.feedback ~state_id:Stateid.initial (Feedback.SlaveStatus(id, s)) + Pp.feedback ~state_id:Stateid.initial (Feedback.WorkerStatus(id, s)) let rec manage_slave ~cancel:cancel_user_req ~die id respawn = let ic, oc, proc = @@ -265,16 +265,8 @@ module Make(T : Task) = struct let slave_handshake () = WorkersPool.worker_handshake !slave_ic !slave_oc let main_loop () = - let feedback_queue = ref [] in let slave_feeder oc fb = - match fb.Feedback.content with - | Feedback.Goals _ -> feedback_queue := fb :: !feedback_queue - | _ -> Marshal.to_channel oc (RespFeedback fb) []; flush oc in - let flush_feeder oc = - List.iter (fun fb -> Marshal.to_channel oc (RespFeedback fb) []) - !feedback_queue; - feedback_queue := []; - flush oc in + Marshal.to_channel oc (RespFeedback fb) []; flush oc in Pp.set_feeder (slave_feeder !slave_oc); Pp.log_via_feedback (); Universes.set_remote_new_univ_level (bufferize (fun () -> @@ -290,7 +282,6 @@ module Make(T : Task) = struct working := true; report_status (name_of_request request); let response = slave_respond request in - flush_feeder !slave_oc; report_status "Idle"; marshal_response !slave_oc response; Ephemeron.clear () diff --git a/stm/stm.ml b/stm/stm.ml index 15637afab..31f90d364 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -58,8 +58,10 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } = (* Wrapper for Vernac.parse_sentence to set the feedback id *) let vernac_parse ?newtip ?route eid s = - if Option.is_empty newtip then set_id_for_feedback ?route (Feedback.Edit eid) - else set_id_for_feedback ?route (Feedback.State (Option.get newtip)); + let feedback_id = + if Option.is_empty newtip then Feedback.Edit eid + else Feedback.State (Option.get newtip) in + set_id_for_feedback ?route feedback_id; let pa = Pcoq.Gram.parsable (Stream.of_string s) in Flags.with_option Flags.we_are_parsing (fun () -> try @@ -604,6 +606,7 @@ end = struct (* {{{ *) let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true) f id = + feedback ~state_id:id Feedback.(ProcessingIn !Flags.async_proofs_worker_id); let str_id = Stateid.to_string id in if is_cached id && not redefine then anomaly (str"defining state "++str str_id++str" twice"); @@ -636,69 +639,6 @@ end (* }}} *) (****************************** CRUFT *****************************************) (******************************************************************************) -(* TODO: Currently, this mimics the process_goal function of ide/ide_slave.ml, - * but we have the opportunity to provide more structure in the xml, here. *) -let process_goal sigma g = - let env = Goal.V82.env sigma g in - let id = Goal.uid g in - let ccl = - let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in - let ccl_string = string_of_ppcmds (Printer.pr_goal_concl_style_env env sigma norm_constr) in - Xml_datatype.Element ("conclusion", [], [Xml_datatype.PCData ccl_string]) in - let process_hyp env h_env acc = - let hyp_string = (string_of_ppcmds (Printer.pr_var_decl env sigma h_env)) in - (Xml_datatype.Element ("hypothesis", [], [Xml_datatype.PCData hyp_string])) :: acc in - let hyps = Xml_datatype.Element ("hypotheses", [], - (List.rev (Environ.fold_named_context process_hyp env ~init:[]))) in - Xml_datatype.Element ("goal", [("id", id)], [hyps; ccl]) - -let print_goals_of_state, forward_feedback = - let already_printed = ref Stateid.Set.empty in - let add_to_already_printed = - let m = Mutex.create () in - fun id -> - Mutex.lock m; - already_printed := Stateid.Set.add id !already_printed; - Mutex.unlock m in - (fun id -> - if Stateid.Set.mem id !already_printed then () - else begin - add_to_already_printed id; - try - Option.iter (fun { proof = pstate } -> - let pfts = Proof_global.proof_of_state pstate in - let structured_goals = Proof.map_structured_proof pfts process_goal in - let xml_bg_goal = fun (l, r) -> Xml_datatype.Element("bg_goal", [], - [Xml_datatype.Element("left_bg_goals", [], l); - Xml_datatype.Element("right_bg_goals", [], r)]) in - - let xml_structured_goals = Xml_datatype.Element("goals", [], - [ Xml_datatype.Element("focussed_goals", [], - structured_goals.Proof.fg_goals); - Xml_datatype.Element("bg_goals", [], - List.map xml_bg_goal structured_goals.Proof.bg_goals); - Xml_datatype.Element("shelved_goals", [], - structured_goals.Proof.shelved_goals); - Xml_datatype.Element("given_up_goals", [], - structured_goals.Proof.given_up_goals) - ] - ) in - Pp.feedback ~state_id:id - (Feedback.StructuredGoals (Loc.ghost, xml_structured_goals)); - Pp.feedback ~state_id:id - (Feedback.Goals - (Loc.ghost, Pp.string_of_ppcmds - (Printer.pr_open_subgoals - ~proof:(Proof_global.proof_of_state pstate) ())))) - (VCS.get_info id).state - with Proof_global.NoCurrentProof -> () - end), - fun id -> function - | Feedback.Goals _ as msg -> - add_to_already_printed id; - Pp.feedback ~state_id:id msg - | msg -> Pp.feedback ~state_id:id msg - (* The backtrack module simulates the classic behavior of a linear document *) module Backtrack : sig @@ -1657,11 +1597,8 @@ let known_state ?(redefine_qed=false) ~cache id = let cache_step = if !Flags.async_proofs_cache = Some Flags.Force then `Yes else cache_step in - if Flags.async_proofs_is_master () then - Pp.feedback ~state_id:id Feedback.ProcessingInMaster; State.define ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id; - if !Flags.feedback_goals then print_goals_of_state id; prerr_endline ("reached: "^ Stateid.to_string id) in reach ~redefine_qed id diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 913dcded4..255544d47 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -446,7 +446,6 @@ let parse_args arglist = |"-compile-verbose" -> add_compile true (next ()) |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true |"-feedback-glob" -> Dumpglob.feedback_glob () - |"-feedback-goals" -> Flags.feedback_goals := true |"-exclude-dir" -> exclude_search_in_dirname (next ()) |"-init-file" -> set_rcfile (next ()) |"-inputstate"|"-is" -> set_inputstate (next ()) |