From 18250a35127ed8913dd05f31f109b308a0f11826 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias 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 From 1a14ec90521fdeed7db52a59e0a049bf578da487 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 21 Sep 2017 17:37:10 +0200 Subject: Adapt checker to change in locations. --- checker/checker.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'checker') diff --git a/checker/checker.ml b/checker/checker.ml index aec3e3282..a23ca8f4f 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -380,8 +380,10 @@ let init_feedback_listener () = 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 where = + match loc.fname with InFile f -> f | ToplevelInput -> "Toplevel input" in + fprintf fmt "\"%s\", line %d, characters %d-%d:@\n" + where 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 -> () -- cgit v1.2.3 From 7000496b6d95b67968ea49537ef9120b764cf9f4 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 21 Sep 2017 17:37:26 +0200 Subject: Fix -silent flag of coqchk after ff918e4. --- checker/mod_checking.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'checker') diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 3c9e1cac5..63e28448f 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -25,7 +25,7 @@ let refresh_arity ar = | _ -> ar, Univ.ContextSet.empty let check_constant_declaration env kn cb = - Feedback.msg_notice (str " checking cst:" ++ prcon kn); + Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ prcon kn); (** [env'] contains De Bruijn universe variables *) let env' = match cb.const_universes with -- cgit v1.2.3