From bd458575ba7f767e3b939fad5d628a9cb24e6bb2 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 22 Mar 2017 18:23:41 +0100 Subject: [pp] Add anomaly header to anomaly error messages. This patch restores the proper printing of anomalies in coqtop / coqc / coqide. Currently, they are printed with an `Error` header, whereas they should be printed with an `Anomaly" header. This reopens an unfinished debate started in #390 , about how to properly do "message" headers. Prior to #390, headers were handled inconsistently, sometimes, `Error` or `Anomaly` were added in `CErrors`, which lives below of the tagging system, thus some times we got no coloring (c.f. https://coq.inria.fr/bugs/show_bug.cgi?id=4789), but some other times the headers were added by the message handlers in Feedback. PR #390 takes the position of identifying the messages with the `Feedback.level` tag, and letting the backends to the tagging. This makes sense as the backends may want to interpret the "headers" in any way they'd like. For instance, instead of printing: `Error: foo` they may want to insert an image. Note that this implies that CoqIDE doesn't currently insert an error header on the first error case. This could be easily solved, but for anomalies we could do in any of the ways explained below. There are thus two natural ways to handle anomalies here: One is to tag them as errors, but add a text header, this is done now, with the small optimization in the case the handled has access to the exception itself. The second way is to add a new `Feedback.level` category and tag the anomalies appropriately. We would need also to modify Fail in this case, or to completely remove it from the protocol. I guess feedback from the rest of developers is needed before committing to a strategy, for now this patch should be good. --- vernac/topfmt.ml | 1 + vernac/topfmt.mli | 1 + 2 files changed, 2 insertions(+) (limited to 'vernac') diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index f843484f7e..e3c0a1709a 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -136,6 +136,7 @@ let dbg_hdr = tag Tag.debug (str "Debug:") ++ spc () let info_hdr = mt () let warn_hdr = tag Tag.warning (str "Warning:") ++ spc () let err_hdr = tag Tag.error (str "Error:") ++ spc () +let ann_hdr = tag Tag.error (str "Anomaly:") ++ spc () let make_body quoter info ?loc s = let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 1555f80a9f..0e122f46e3 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -38,6 +38,7 @@ val get_margin : unit -> int option (** Headers for tagging *) val err_hdr : Pp.std_ppcmds +val ann_hdr : Pp.std_ppcmds (** Console display of feedback *) val std_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit -- cgit v1.2.3 From 8cfe40dbc02156228a529c01190c50d825495013 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 22 Mar 2017 19:06:54 +0100 Subject: Ensuring static invariants about handling of pending evars in Pretyping. All functions where actually called with the second argument of the pending problem being the current evar map. We simply remove this useless and error-prone second component. --- vernac/command.ml | 8 ++++---- vernac/lemmas.ml | 2 +- vernac/record.ml | 2 +- 3 files changed, 6 insertions(+), 6 deletions(-) (limited to 'vernac') diff --git a/vernac/command.ml b/vernac/command.ml index 4b4f4d2711..849596f07b 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -139,7 +139,7 @@ let interp_definition pl bl p red_option c ctypopt = red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, pl, imps let check_definition (ce, evd, _, imps) = - check_evars_are_solved (Global.env ()) evd (Evd.empty,evd); + check_evars_are_solved (Global.env ()) evd Evd.empty; ce let warn_local_declaration = @@ -299,7 +299,7 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = ((env,ienv),((is_coe,idl),t,imps))) (env,empty_internalization_env) l in - let evd = solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref) in + let evd = solve_remaining_evars all_and_fail_flags env !evdref Evd.empty in (* The universe constraints come from the whole telescope. *) let evd = Evd.nf_constraints evd in let ctx = Evd.universe_context_set evd in @@ -604,7 +604,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = () in (* Try further to solve evars, and instantiate them *) - let sigma = solve_remaining_evars all_and_fail_flags env_params !evdref (Evd.empty,!evdref) in + let sigma = solve_remaining_evars all_and_fail_flags env_params !evdref Evd.empty in evdref := sigma; (* Compute renewed arities *) let nf,_ = e_nf_evars_and_universes evdref in @@ -1142,7 +1142,7 @@ let interp_recursive isfix fixl notations = (env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxnames fiximps fixannots let check_recursive isfix env evd (fixnames,fixdefs,_) = - check_evars_are_solved env evd (Evd.empty,evd); + check_evars_are_solved env evd Evd.empty; if List.for_all Option.has_some fixdefs then begin let fixdefs = List.map Option.get fixdefs in check_mutuality env isfix (List.combine fixnames fixdefs) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 798a238c74..409676276a 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -463,7 +463,7 @@ let start_proof_com ?inference_hook kind thms hook = let t', imps' = interp_type_evars_impls ~impls env evdref t in let flags = all_and_fail_flags in let flags = { flags with use_hook = inference_hook } in - evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref); + evdref := solve_remaining_evars flags env !evdref Evd.empty; let ids = List.map RelDecl.get_name ctx in (compute_proof_name (pi1 kind) sopt, (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), diff --git a/vernac/record.ml b/vernac/record.ml index b494430c28..07cfd9ebb7 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -141,7 +141,7 @@ let typecheck_params_and_fields def id pl t ps nots fs = interp_fields_evars env_ar evars impls_env nots (binders_of_decls fs) in let sigma = - Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar !evars (Evd.empty,!evars) in + Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar !evars Evd.empty in let evars, nf = Evarutil.nf_evars_and_universes sigma in let arity = nf t' in let arity, evars = -- cgit v1.2.3 From 63cfc77ddf3586262d905dc351b58669d185a55e Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 31 Mar 2017 20:38:52 +0200 Subject: [toplevel] Remove exception error printer in favor of feedback printer. We solve https://coq.inria.fr/bugs/show_bug.cgi?id=4789 by printing all the errors from the feedback handler, even in the case of coqtop. All error display is handled by a single, uniform path. There may be some minor discrepancies with 8.6 as we are uniform now whereas 8.6 tended to print errors in several ways, but our behavior is a subset of the 8.6 behavior. We had to make a choice for `-emacs` error output, which used to vary too. We have chosen to display error messages as: ``` (location info) option \n (program caret) option \n MARKER[254]Error: msgMARKER[255] ``` This commit also fixes: - https://coq.inria.fr/bugs/show_bug.cgi?id=5418 - https://coq.inria.fr/bugs/show_bug.cgi?id=5429 --- vernac/topfmt.ml | 24 +++++++++++------------- vernac/topfmt.mli | 7 +++---- 2 files changed, 14 insertions(+), 17 deletions(-) (limited to 'vernac') diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index e3c0a1709a..ee55366927 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -108,7 +108,7 @@ end type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit -let msgnl_with fmt strm = +let msgnl_with ?pre_hdr fmt strm = pp_with fmt (strm ++ fnl ()); Format.pp_print_flush fmt () @@ -138,19 +138,17 @@ let warn_hdr = tag Tag.warning (str "Warning:") ++ spc () let err_hdr = tag Tag.error (str "Error:") ++ spc () let ann_hdr = tag Tag.error (str "Anomaly:") ++ spc () -let make_body quoter info ?loc s = - let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in - quoter (hov 0 (loc ++ info ++ s)) +let make_body quoter info ?pre_hdr s = + pr_opt_no_spc (fun x -> x ++ fnl ()) pre_hdr ++ quoter (hov 0 (info ++ s)) (* Generic logger *) -let gen_logger dbg err ?loc level msg = match level with - | Debug -> msgnl_with !std_ft (make_body dbg dbg_hdr ?loc msg) - | Info -> msgnl_with !std_ft (make_body dbg info_hdr ?loc msg) - (* XXX: What to do with loc here? *) - | Notice -> msgnl_with !std_ft msg +let gen_logger dbg err ?pre_hdr level msg = match level with + | Debug -> msgnl_with !std_ft (make_body dbg dbg_hdr ?pre_hdr msg) + | Info -> msgnl_with !std_ft (make_body dbg info_hdr ?pre_hdr msg) + | Notice -> msgnl_with !std_ft (make_body dbg info_hdr ?pre_hdr msg) | Warning -> Flags.if_warn (fun () -> - msgnl_with !err_ft (make_body err warn_hdr ?loc msg)) () - | Error -> msgnl_with !err_ft (make_body err err_hdr ?loc msg) + msgnl_with !err_ft (make_body err warn_hdr ?pre_hdr msg)) () + | Error -> msgnl_with !err_ft (make_body err err_hdr ?pre_hdr msg) (** Standard loggers *) @@ -159,8 +157,8 @@ let gen_logger dbg err ?loc level msg = match level with *) let std_logger_cleanup = ref (fun () -> ()) -let std_logger ?loc level msg = - gen_logger (fun x -> x) (fun x -> x) ?loc level msg; +let std_logger ?pre_hdr level msg = + gen_logger (fun x -> x) (fun x -> x) ?pre_hdr level msg; !std_logger_cleanup () (** Color logging. Moved from Ppstyle, it may need some more refactoring *) diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 0e122f46e3..909dd70775 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -40,10 +40,9 @@ val get_margin : unit -> int option val err_hdr : Pp.std_ppcmds val ann_hdr : Pp.std_ppcmds -(** Console display of feedback *) -val std_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit - -val emacs_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit +(** Console display of feedback, we may add some location information *) +val std_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit +val emacs_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit val init_color_output : unit -> unit val clear_styles : unit -> unit -- cgit v1.2.3