[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].

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