diff options
| -rw-r--r-- | lib/feedback.ml | 11 | ||||
| -rw-r--r-- | lib/feedback.mli | 2 | ||||
| -rw-r--r-- | lib/flags.ml | 2 | ||||
| -rw-r--r-- | lib/flags.mli | 3 | ||||
| -rw-r--r-- | library/library.ml | 1 | ||||
| -rw-r--r-- | printing/printer.ml | 4 | ||||
| -rw-r--r-- | printing/printer.mli | 2 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 1 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 1 | ||||
| -rw-r--r-- | stm/stm.ml | 21 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 1 |
11 files changed, 46 insertions, 3 deletions
diff --git a/lib/feedback.ml b/lib/feedback.ml index b532c2653..4eb611157 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -24,6 +24,8 @@ type feedback_content = | InProgress of int | SlaveStatus of int * string | ProcessingInMaster + | Goals of Loc.t * string + | FileLoaded of string * string type feedback = { id : edit_or_state_id; @@ -46,6 +48,9 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with | "slavestatus", [ns] -> let n, s = to_pair to_int to_string ns in SlaveStatus(n,s) + | "goals", [loc;s] -> Goals (to_loc loc, to_string s) + | "fileloaded", [dirpath; filename] -> + FileLoaded(to_string dirpath, to_string filename) | _ -> raise Marshal_error) let of_feedback_content = function | AddedAxiom -> constructor "feedback_content" "addedaxiom" [] @@ -72,6 +77,12 @@ let of_feedback_content = function | SlaveStatus(n,s) -> constructor "feedback_content" "slavestatus" [of_pair of_int of_string (n,s)] + | Goals (loc,s) -> + constructor "feedback_content" "goals" [of_loc loc;of_string s] + | FileLoaded(dirpath, filename) -> + constructor "feedback_content" "fileloaded" [ + of_string dirpath; + of_string filename ] let of_edit_or_state_id = function | Edit id -> ["object","edit"], of_edit_id id diff --git a/lib/feedback.mli b/lib/feedback.mli index e7645ca16..c245ec76a 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -24,6 +24,8 @@ type feedback_content = | InProgress of int | SlaveStatus of int * string | ProcessingInMaster + | Goals of Loc.t * string + | FileLoaded of string * string type feedback = { id : edit_or_state_id; diff --git a/lib/flags.ml b/lib/flags.ml index 36bb447ae..9dd65db6d 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -70,6 +70,8 @@ let xml_export = 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 ea50d41da..a0ff0f55e 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -34,6 +34,9 @@ val xml_export : 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 diff --git a/library/library.ml b/library/library.ml index 4f023ce6d..9552a6ca9 100644 --- a/library/library.ml +++ b/library/library.ml @@ -488,6 +488,7 @@ let rec intern_library (needed, contents) (dir, f) = (str ("The file " ^ f ^ " contains library") ++ spc () ++ pr_dirpath m.library_name ++ spc () ++ str "and not library" ++ spc() ++ pr_dirpath dir); + Pp.feedback(Feedback.FileLoaded(DirPath.to_string dir, f)); m, intern_library_deps (needed, contents) dir m and intern_library_deps libs dir m = diff --git a/printing/printer.ml b/printing/printer.ml index 3b5c80c62..03f416a51 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -549,12 +549,12 @@ let pr_goal x = !printer_pr.pr_goal x (* End abstraction layer *) (**********************************************************************) -let pr_open_subgoals () = +let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = (* spiwack: it shouldn't be the job of the printer to look up stuff in the [evar_map], I did stuff that way because it was more straightforward, but seriously, [Proof.proof] should return [evar_info]-s instead. *) - let p = Proof_global.give_me_the_proof () in + let p = proof in let (goals , stack , shelf, given_up, sigma ) = Proof.proof p in let stack = List.map (fun (l,r) -> List.length l + List.length r) stack in let seeds = Proof.V82.top_evars p in diff --git a/printing/printer.mli b/printing/printer.mli index eb181d426..aa949232a 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -128,7 +128,7 @@ val pr_subgoals : ?pr_first:bool -> string option -> evar_map -> evar val pr_subgoal : int -> evar_map -> goal list -> std_ppcmds val pr_concl : int -> evar_map -> goal -> std_ppcmds -val pr_open_subgoals : unit -> std_ppcmds +val pr_open_subgoals : ?proof:Proof.proof -> unit -> std_ppcmds val pr_nth_open_subgoal : int -> std_ppcmds val pr_evar : (evar * evar_info) -> std_ppcmds val pr_evars_int : int -> evar_info Evar.Map.t -> std_ppcmds diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 06afc2fa9..7c7ff0c94 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -515,4 +515,5 @@ let freeze ~marshallable = | `Shallow -> !pstates | `No -> !pstates let unfreeze s = pstates := s; update_proof_mode () +let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index d5229c562..2b54b24ef 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -188,3 +188,4 @@ end type state val freeze : marshallable:[`Yes | `No | `Shallow] -> state val unfreeze : state -> unit +val proof_of_state : state -> Proof.proof diff --git a/stm/stm.ml b/stm/stm.ml index 2007dba81..2af43db66 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -495,6 +495,16 @@ end = struct end +let print_goals_of_state id = + try + Option.iter (fun { proof = pstate } -> 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 -> () + (* Fills in the nodes of the VCS *) module State : sig @@ -722,6 +732,14 @@ end = struct let build_proof_here (id,valid) loc eop = Future.create (State.exn_on id ~valid) (build_proof_here_core loc eop) + let slave_print_all_goals id = + let rec aux id = + try aux (VCS.visit id).next + with + | VCS.Expired -> () + | e when Errors.noncritical e -> () in + Future.purify (fun id -> !reach_known_state ~cache:`No id; aux id) id + let slave_respond msg = match msg with | ReqBuildProof(exn_info,eop,vcs,loc,_,_) -> @@ -739,6 +757,7 @@ end = struct se) (fst l); l, Unix.gettimeofday () -. wall_clock in VCS.print (); + if !Flags.feedback_goals then slave_print_all_goals eop; RespBuiltProof(rc,time) let check_task_aux extra name l i = @@ -1120,6 +1139,7 @@ end = struct | Some id -> aux (n+1) m id in (if is_cached safe_id then [safe_id,get_cached safe_id] else []) @ aux 1 (prog 1 1) safe_id in + if !Flags.feedback_goals then slave_print_all_goals safe_id; marshal_response !slave_oc (RespError(err_id, safe_id, print e, states)) | e -> pr_err ("Slave: critical exception: " ^ Pp.string_of_ppcmds (print e)); @@ -1349,6 +1369,7 @@ let known_state ?(redefine_qed=false) ~cache id = if !Flags.async_proofs_mode = Flags.APonParallel 0 then Pp.feedback ~state_id:id Feedback.ProcessingInMaster; State.define ~cache:cache_step ~redefine:redefine_qed 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 0ccb6faaf..be63db391 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -360,6 +360,7 @@ 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 ()) |