From 33789b2d1706194d478a25098bd1991d2c845223 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 27 Nov 2017 19:18:21 +0100 Subject: [error] Replace msg_error by a proper exception. The current error mechanism in the core part of Coq is 100% exception based; there was some confusion in the past as to whether raising and exception could be replace with `Feedback.msg_error`. As of today, this is not the case [due to some issues in the layer that generates error feedbacks in the STM] so all cases of `msg_error` must raise an exception of print at a different level [for now]. --- checker/checker.ml | 2 +- engine/logic_monad.ml | 1 - engine/logic_monad.mli | 1 - lib/coqProject_file.ml4 | 2 +- lib/feedback.mli | 5 +++-- stm/stm.ml | 28 ++++++++++++++-------------- tools/coqdep.ml | 2 +- toplevel/coqloop.ml | 4 ++-- vernac/vernacentries.ml | 4 ++-- 9 files changed, 24 insertions(+), 25 deletions(-) diff --git a/checker/checker.ml b/checker/checker.ml index b8b4d5dc2..e8eff889c 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -18,7 +18,7 @@ let () = at_exit flush_all let chk_pp = Pp.pp_with Format.std_formatter let fatal_error info anomaly = - flush_all (); Feedback.msg_error info; flush_all (); + flush_all (); Format.eprintf "@[Fatal Error: @[%a@]@]%!@\n" Pp.pp_with info; flush_all (); exit (if anomaly then 129 else 1) let coq_root = Id.of_string "Coq" diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index 9dc5d473b..3674bb943 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -107,7 +107,6 @@ struct let print_debug s = make (fun _ -> Feedback.msg_info s) let print_info s = make (fun _ -> Feedback.msg_info s) let print_warning s = make (fun _ -> Feedback.msg_warning s) - let print_error s = make (fun _ -> Feedback.msg_error s) let print_notice s = make (fun _ -> Feedback.msg_notice s) let run = fun x -> diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli index 8c8f9fe93..50b4abd8b 100644 --- a/engine/logic_monad.mli +++ b/engine/logic_monad.mli @@ -61,7 +61,6 @@ module NonLogical : sig val print_warning : Pp.t -> unit t val print_notice : Pp.t -> unit t val print_info : Pp.t -> unit t - val print_error : Pp.t -> unit t (** [Pervasives.raise]. Except that exceptions are wrapped with {!Exception}. *) diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 index 1e52af0be..e6f1d7e06 100644 --- a/lib/coqProject_file.ml4 +++ b/lib/coqProject_file.ml4 @@ -114,7 +114,7 @@ let process_cmd_line orig_dir proj args = let parsing_project_file = ref (proj.project_file <> None) in let orig_dir = (* avoids turning foo.v in ./foo.v *) if orig_dir = "." then "" else orig_dir in - let error s = Feedback.msg_error (Pp.str (s^".")); exit 1 in + let error s = Format.eprintf "@[%a]@@\n%!" Pp.pp_with Pp.(str (s^".")); exit 1 in let mk_path d = let p = CUnix.correct_path d orig_dir in { path = CUnix.remove_path_dot (post_canonize p); diff --git a/lib/feedback.mli b/lib/feedback.mli index 62b909516..37f38c8ff 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -94,8 +94,9 @@ val msg_warning : ?loc:Loc.t -> Pp.t -> unit consequences. *) val msg_error : ?loc:Loc.t -> Pp.t -> unit -(** Message indicating that something went really wrong, though still - recoverable; otherwise an exception would have been raised. *) +[@@ocaml.deprecated "msg_error is an internal function and should not be \ + used unless you know what you are doing. Use \ + [CErrors.user_err] instead."] val msg_debug : ?loc:Loc.t -> Pp.t -> unit (** For debugging purposes *) diff --git a/stm/stm.ml b/stm/stm.ml index b5848c662..6c956e134 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -85,8 +85,7 @@ let stm_purify f x = Exninfo.iraise e let execution_error ?loc state_id msg = - feedback ~id:state_id - (Message (Error, loc, msg)) + feedback ~id:state_id (Message (Error, loc, msg)) module Hooks = struct @@ -1579,12 +1578,13 @@ end = struct (* {{{ *) | ReqStates sl -> RespStates (perform_states sl) let on_marshal_error s = function - | States _ -> msg_error(Pp.strbrk("Marshalling error: "^s^". "^ - "The system state could not be sent to the master process.")) + | States _ -> + msg_warning Pp.(strbrk("Marshalling error: "^s^". "^ + "The system state could not be sent to the master process.")) | BuildProof { t_exn_info; t_stop; t_assign; t_loc; t_drop = drop_pt } -> - msg_error(Pp.strbrk("Marshalling error: "^s^". "^ - "The system state could not be sent to the worker process. "^ - "Falling back to local, lazy, evaluation.")); + msg_warning Pp.(strbrk("Marshalling error: "^s^". "^ + "The system state could not be sent to the worker process. "^ + "Falling back to local, lazy, evaluation.")); t_assign(`Comp(build_proof_here ?loc:t_loc ~drop_pt t_exn_info t_stop)); feedback (InProgress ~-1) @@ -1672,7 +1672,7 @@ end = struct (* {{{ *) let (e, info) = CErrors.push e in (try match Stateid.get info with | None -> - msg_error Pp.( + msg_warning Pp.( str"File " ++ str name ++ str ": proof of " ++ str r_name ++ spc () ++ iprint (e, info)) | Some (_, cur) -> @@ -1682,17 +1682,17 @@ end = struct (* {{{ *) | { step = `Qed ( { qast = { loc } }, _) } | { step = `Sideff (ReplayCommand { loc }, _) } -> let start, stop = Option.cata Loc.unloc (0,0) loc in - msg_error Pp.( + msg_warning Pp.( str"File " ++ str name ++ str ": proof of " ++ str r_name ++ str ": chars " ++ int start ++ str "-" ++ int stop ++ spc () ++ iprint (e, info)) | _ -> - msg_error Pp.( + msg_warning Pp.( str"File " ++ str name ++ str ": proof of " ++ str r_name ++ spc () ++ iprint (e, info)) with e -> - msg_error Pp.(str"unable to print error message: " ++ - str (Printexc.to_string e))); + msg_warning Pp.(str"unable to print error message: " ++ + str (Printexc.to_string e))); if drop then `ERROR_ADMITTED else `ERROR let finish_task name (u,cst,_) d p l i = @@ -2429,7 +2429,7 @@ let known_state ?(redefine_qed=false) ~cache id = | { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) -> assert(redefine_qed = true); if okeep != keep then - msg_error(strbrk("The command closing the proof changed. " + msg_warning(strbrk("The command closing the proof changed. " ^"The kernel cannot take this into account and will " ^(if keep == VtKeep then "not check " else "reject ") ^"the "^(if keep == VtKeep then "new" else "incomplete") @@ -2702,7 +2702,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) = (u,a,true), p with e -> let e = CErrors.push e in - msg_error (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e); + msg_warning (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e); exit 1 let merge_proof_branch ~valid ?id qast keep brname = diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 2433cb1d0..ca14b11bc 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -539,4 +539,4 @@ let _ = coqdep () with CErrors.UserError(s,p) -> let pp = (match s with | None -> p | Some s -> Pp.(str s ++ str ": " ++ p)) in - Feedback.msg_error pp + Format.eprintf "%a@\n%!" Pp.pp_with pp diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 5c1b27c33..aade101a4 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -312,7 +312,7 @@ let do_vernac ~time doc sid = top_stderr (fnl ()); raise CErrors.Quit | CErrors.Drop -> (* Last chance *) if Mltop.is_ocaml_top() then raise CErrors.Drop - else (Feedback.msg_error (str "There is no ML toplevel."); doc, sid) + else (Feedback.msg_warning (str "There is no ML toplevel."); doc, sid) (* Exception printing should be done by the feedback listener, however this is not yet ready so we rely on the exception for now. *) @@ -353,7 +353,7 @@ let rec loop ~time doc = | CErrors.Drop -> doc | CErrors.Quit -> exit 0 | any -> - Feedback.msg_error (str "Anomaly: main loop exited with exception: " ++ + top_stderr (str "Anomaly: main loop exited with exception: " ++ str (Printexc.to_string any) ++ fnl() ++ str"Please report" ++ diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index be09696d1..7223389c4 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -189,7 +189,7 @@ let print_module r = Feedback.msg_notice (Printmod.print_module (Printmod.printable_body obj_dir) obj_mp) | _ -> raise Not_found with - Not_found -> Feedback.msg_error (str"Unknown Module " ++ pr_qualid qid) + Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid) let print_modtype r = let (loc,qid) = qualid_of_reference r in @@ -202,7 +202,7 @@ let print_modtype r = let mp = Nametab.locate_module qid in Feedback.msg_notice (Printmod.print_module false mp) with Not_found -> - Feedback.msg_error (str"Unknown Module Type or Module " ++ pr_qualid qid) + user_err (str"Unknown Module Type or Module " ++ pr_qualid qid) let print_namespace ns = let ns = List.rev (Names.DirPath.repr ns) in -- cgit v1.2.3