From 18250a35127ed8913dd05f31f109b308a0f11826 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Thu, 20 Jul 2017 00:12:01 +0200
Subject: [checker] Add missing Feedback printer (BZ#5587)

This fixes longstanding bug likely introduced in the first `pp` to
`Feedback` migration, namely the checker didn't register a feedback
printer, thus no calls to `Feedback.msg_*` were printed in the
checker.

This closes bug: https://coq.inria.fr/bugs/show_bug.cgi?id=5587

We fix this by adding a custom printer to the checker, this is correct
as the checker owns now the full console, however a cleanup should
happen in any of these two directions:

- all the calls to feedback are removed, and the checker always uses
  its own printing mechanism.

- all the calls to `Format/Printf` are removed and the checker always
  uses the `Feedback` mechanism.

Currently, I have no opinion on this.
---
 checker/checker.ml | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)

(limited to 'checker')

diff --git a/checker/checker.ml b/checker/checker.ml
index 7a69700d2..aec3e3282 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -366,10 +366,46 @@ let parse_args argv =
 (* To prevent from doing the initialization twice *)
 let initialized = ref false
 
+(* XXX: At some point we need to either port the checker to use the
+   feedback system or to remove its use completely. *)
+let init_feedback_listener () =
+  let open Format in
+  let pp_lvl fmt lvl = let open Feedback in match lvl with
+    | Error   -> fprintf fmt "Error: "
+    | Info    -> fprintf fmt "Info: "
+    | Debug   -> fprintf fmt "Debug: "
+    | Warning -> fprintf fmt "Warning: "
+    | Notice  -> fprintf fmt ""
+  in
+  let pp_loc fmt loc = let open Loc in match loc with
+    | None     -> fprintf fmt ""
+    | Some loc ->
+      fprintf fmt "File \"%s\", line %d, characters %d-%d:@\n"
+        loc.fname loc.line_nb (loc.bp-loc.bol_pos) (loc.ep-loc.bol_pos) in
+  let checker_feed (fb : Feedback.feedback) = let open Feedback in
+  match fb.contents with
+  | Processed   -> ()
+  | Incomplete  -> ()
+  | Complete    -> ()
+  | ProcessingIn _ -> ()
+  | InProgress _ -> ()
+  | WorkerStatus (_,_) -> ()
+  | AddedAxiom  -> ()
+  | GlobRef (_,_,_,_,_) -> ()
+  | GlobDef (_,_,_,_) -> ()
+  | FileDependency (_,_) -> ()
+  | FileLoaded (_,_) -> ()
+  | Custom (_,_,_) -> ()
+  (* Re-enable when we switch back to feedback-based error printing *)
+  | Message (lvl,loc,msg) ->
+    Format.eprintf "@[%a@]%a@[%a@]\n%!" pp_loc loc pp_lvl lvl Pp.pp_with msg
+  in ignore(Feedback.add_feeder checker_feed)
+
 let init_with_argv argv =
   if not !initialized then begin
     initialized := true;
     Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
+    init_feedback_listener ();
     try
       parse_args argv;
       if !Flags.debug then Printexc.record_backtrace true;
-- 
cgit v1.2.3