From 8e07227c5853de78eaed4577eefe908fb84507c0 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 28 Jun 2016 10:55:30 +0200 Subject: A new infrastructure for warnings. On the user side, coqtop and coqc take a list of warning names or categories after -w. No prefix means activate the warning, a "-" prefix means deactivate it, and "+" means turn the warning into an error. Special categories include "all", and "default" which contains the warnings enabled by default. We also provide a vernacular Set Warnings which takes the same flags as argument. Note that coqc now prints warnings. The name and category of a warning are printed with the warning itself. On the developer side, Feedback.msg_warning is still accessible, but the recommended way to print a warning is in two steps: 1) create it by: let warn_my_warning = CWarnings.create ~name:"my-warning" ~category:"my-category" (fun args -> Pp.strbrk ...) 2) print it by: warn_my_warning args --- toplevel/cerrors.ml | 7 ------- toplevel/cerrors.mli | 4 ---- toplevel/class.ml | 12 +++++++----- toplevel/command.ml | 49 +++++++++++++++++++++++++++++++---------------- toplevel/coqinit.ml | 7 ++++--- toplevel/coqloop.ml | 16 +++++++--------- toplevel/coqtop.ml | 28 +++++++++++++-------------- toplevel/indschemes.ml | 9 +++++++-- toplevel/locality.ml | 9 +++++++-- toplevel/metasyntax.ml | 30 ++++++++++++++++++++--------- toplevel/mltop.ml | 21 +++++++++++++++++--- toplevel/record.ml | 19 ++++++++++++++---- toplevel/vernac.ml | 16 ++++++++++++---- toplevel/vernacentries.ml | 39 +++++++++++++++++++++++++++++-------- toplevel/vernacinterp.ml | 7 ++++++- 15 files changed, 181 insertions(+), 92 deletions(-) (limited to 'toplevel') diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 0bb7966d7..e45ab4b4e 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -13,13 +13,6 @@ open Type_errors open Pretype_errors open Indrec -let print_loc loc = - if Loc.is_ghost loc then - (str"") - else - let loc = Loc.unloc loc in - (int (fst loc) ++ str"-" ++ int (snd loc)) - let guill s = str "\"" ++ str s ++ str "\"" (** Invariant : exceptions embedded in EvaluatedError satisfy diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli index cd6ccd565..a67c887af 100644 --- a/toplevel/cerrors.mli +++ b/toplevel/cerrors.mli @@ -9,10 +9,6 @@ (** Toplevel Exception *) exception EvaluatedError of Pp.std_ppcmds * exn option -(** Error report. *) - -val print_loc : Loc.t -> Pp.std_ppcmds - (** Pre-explain a vernac interpretation error *) val process_vernac_interp_error : ?allow_uncaught:bool -> ?with_header:bool -> Util.iexn -> Util.iexn diff --git a/toplevel/class.ml b/toplevel/class.ml index 10e9b30be..fa68a69fb 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -32,7 +32,6 @@ type coercion_error_kind = | NotAFunction | NoSource of cl_typ option | ForbiddenSourceClass of cl_typ - | NotUniform | NoTarget | WrongTarget of cl_typ * cl_typ | NotAClass of global_reference @@ -51,9 +50,6 @@ let explain_coercion_error g = function (str ": cannot find the source class of " ++ Printer.pr_global g) | ForbiddenSourceClass cl -> pr_class cl ++ str " cannot be a source class" - | NotUniform -> - (Printer.pr_global g ++ - str" does not respect the uniform inheritance condition"); | NoTarget -> (str"Cannot find the target class") | WrongTarget (clt,cl) -> @@ -247,6 +243,12 @@ booleen "coercion identite'?" lorque source est None alors target est None aussi. *) +let warn_uniform_inheritance = + CWarnings.create ~name:"uniform-inheritance" ~category:"typechecker" + (fun g -> + Printer.pr_global g ++ + strbrk" does not respect the uniform inheritance condition") + let add_new_coercion_core coef stre poly source target isid = check_source source; let t = Global.type_of_global_unsafe coef in @@ -262,7 +264,7 @@ let add_new_coercion_core coef stre poly source target isid = in check_source (Some cls); if not (uniform_cond (llp-ind) lvs) then - Feedback.msg_warning (explain_coercion_error coef NotUniform); + warn_uniform_inheritance coef; let clt = try get_target tg ind diff --git a/toplevel/command.ml b/toplevel/command.ml index 28fa8a171..ffa2484ee 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -82,6 +82,12 @@ let red_constant_entry n ce sigma = function { ce with const_entry_body = Future.chain ~greedy:true ~pure:true proof_out (fun ((body,ctx),eff) -> (under_binders env sigma redfun n body,ctx),eff) } +let warn_implicits_in_term = + CWarnings.create ~name:"implicits-in-term" ~category:"implicits" + (fun () -> + strbrk "Implicit arguments declaration relies on type." ++ spc () ++ + strbrk "The term declares more implicits than the type here.") + let interp_definition pl bl p red_option c ctypopt = let env = Global.env() in let ctx = Evd.make_evar_universe_context env pl in @@ -119,9 +125,7 @@ let interp_definition pl bl p red_option c ctypopt = impl_eq (List.assoc_f Pervasives.(=) key impsty) va (* FIXME *) in if not (try List.for_all chk imps2 with Not_found -> false) - then Feedback.msg_warning - (strbrk "Implicit arguments declaration relies on type." ++ spc () ++ - strbrk "The term declares more implicits than the type here."); + then warn_implicits_in_term (); let vars = Univ.LSet.union (Universes.universes_of_constr body) (Universes.universes_of_constr typ) in let ctx = Evd.restrict_universe_context !evdref vars in @@ -136,11 +140,15 @@ let check_definition (ce, evd, _, imps) = check_evars_are_solved (Global.env ()) evd (Evd.empty,evd); ce +let warn_local_let_definition = + CWarnings.create ~name:"local-let-definition" ~category:"scope" + (fun id -> + pr_id id ++ strbrk " is declared as a local definition") + let get_locality id = function | Discharge -> (** If a Let is defined outside a section, then we consider it as a local definition *) - let msg = pr_id id ++ strbrk " is declared as a local definition" in - let () = Feedback.msg_warning msg in + warn_local_let_definition id; true | Local -> true | Global -> false @@ -158,6 +166,12 @@ let declare_definition_hook = ref ignore let set_declare_definition_hook = (:=) declare_definition_hook let get_declare_definition_hook () = !declare_definition_hook +let warn_definition_not_visible = + CWarnings.create ~name:"definition-not-visible" ~category:"implicits" + (fun ident -> + strbrk "Section definition " ++ + pr_id ident ++ strbrk " is not visible from current goals") + let declare_definition ident (local, p, k) ce pl imps hook = let fix_exn = Future.fix_exn_of ce.const_entry_body in let () = !declare_definition_hook ce in @@ -169,9 +183,7 @@ let declare_definition ident (local, p, k) ce pl imps hook = let gr = VarRef ident in let () = maybe_declare_manual_implicits false gr imps in let () = if Pfedit.refining () then - let msg = strbrk "Section definition " ++ - pr_id ident ++ strbrk " is not visible from current goals" in - Feedback.msg_warning msg + warn_definition_not_visible ident in gr | Discharge | Local | Global -> @@ -217,7 +229,7 @@ match local with let () = assumption_message ident in let () = if is_verbose () && Pfedit.refining () then - Feedback.msg_warning (str"Variable" ++ spc () ++ pr_id ident ++ + Feedback.msg_info (str"Variable" ++ spc () ++ pr_id ident ++ strbrk " is not visible from current goals") in let r = VarRef ident in @@ -780,20 +792,25 @@ let rec partial_order cmp = function let non_full_mutual_message x xge y yge isfix rest = let reason = if Id.List.mem x yge then - pr_id y ++ str " depends on " ++ pr_id x ++ str " but not conversely" + pr_id y ++ str " depends on " ++ pr_id x ++ strbrk " but not conversely" else if Id.List.mem y xge then - pr_id x ++ str " depends on " ++ pr_id y ++ str " but not conversely" + pr_id x ++ str " depends on " ++ pr_id y ++ strbrk " but not conversely" else - pr_id y ++ str " and " ++ pr_id x ++ str " are not mutually dependent" in - let e = if List.is_empty rest then reason else str "e.g., " ++ reason in + pr_id y ++ str " and " ++ pr_id x ++ strbrk " are not mutually dependent" in + let e = if List.is_empty rest then reason else strbrk "e.g., " ++ reason in let k = if isfix then "fixpoint" else "cofixpoint" in let w = if isfix - then str "Well-foundedness check may fail unexpectedly." ++ fnl() + then strbrk "Well-foundedness check may fail unexpectedly." ++ fnl() else mt () in - str "Not a fully mutually defined " ++ str k ++ fnl () ++ + strbrk "Not a fully mutually defined " ++ str k ++ fnl () ++ str "(" ++ e ++ str ")." ++ fnl () ++ w +let warn_non_full_mutual = + CWarnings.create ~name:"non-full-mutual" ~category:"fixpoints" + (fun (x,xge,y,yge,isfix,rest) -> + non_full_mutual_message x xge y yge isfix rest) + let check_mutuality env isfix fixl = let names = List.map fst fixl in let preorder = @@ -803,7 +820,7 @@ let check_mutuality env isfix fixl = let po = partial_order Id.equal preorder in match List.filter (function (_,Inr _) -> true | _ -> false) po with | (x,Inr xge)::(y,Inr yge)::rest -> - Feedback.msg_warning (non_full_mutual_message x xge y yge isfix rest) + warn_non_full_mutual (x,xge,y,yge,isfix,rest) | _ -> () type structured_fixpoint_expr = { diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 65c5917b7..50a228050 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -135,6 +135,7 @@ let get_compat_version = function | "8.3" -> Flags.V8_3 | "8.2" -> Flags.V8_2 | ("8.1" | "8.0") as s -> - Feedback.msg_warning (str "Compatibility with version " ++ str s ++ str " not supported."); - Flags.V8_2 - | s -> Errors.errorlabstrm "get_compat_version" (str "Unknown compatibility version \"" ++ str s ++ str "\".") + Errors.errorlabstrm "get_compat_version" + (str "Compatibility with version " ++ str s ++ str " not supported.") + | s -> Errors.errorlabstrm "get_compat_version" + (str "Unknown compatibility version \"" ++ str s ++ str "\".") diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 00e0219f1..67a5472d5 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -146,9 +146,8 @@ let print_highlight_location ib loc = str sn ++ str dn) in (l1 ++ li ++ ln) in - let loc = Loc.make_loc (bp,ep) in - (str"Toplevel input, characters " ++ Cerrors.print_loc loc ++ str":" ++ fnl () ++ - highlight_lines ++ fnl ()) + let loc = Loc.make_loc (bp,ep) in + (Pp.pr_loc loc ++ highlight_lines ++ fnl ()) (* Functions to report located errors in a file. *) @@ -163,10 +162,7 @@ let print_location_in_file loc = in let open Loc in hov 0 (* No line break so as to follow emacs error message format *) - (errstrm ++ str"File " ++ str "\"" ++ str fname ++ str "\"" ++ - str", line " ++ int loc.line_nb ++ str", characters " ++ - Cerrors.print_loc (Loc.make_loc (loc.bp-loc.bol_pos,loc.ep-loc.bol_pos))) ++ str":" ++ - fnl () + (errstrm ++ Pp.pr_loc loc) let valid_buffer_loc ib loc = not (Loc.is_ghost loc) && @@ -249,7 +245,7 @@ let print_toplevel_error (e, info) = let loc = Option.default Loc.ghost (Loc.get_loc info) in let fname = loc.Loc.fname in let locmsg = - if String.equal fname "" then + if Loc.is_ghost loc || String.equal fname "" then if locate_exn e && valid_buffer_loc top_buffer loc then print_highlight_location top_buffer loc else mt () @@ -279,7 +275,9 @@ let rec discard_to_dot () = | e when Errors.noncritical e -> () let read_sentence () = - try Vernac.parse_sentence (top_buffer.tokens, None) + try + let (loc, _ as r) = Vernac.parse_sentence (top_buffer.tokens, None) in + CWarnings.set_current_loc loc; r with reraise -> let reraise = Errors.push reraise in discard_to_dot (); diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index e34f38eb3..93ed2481b 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -123,16 +123,6 @@ let engage () = let set_batch_mode () = batch_mode := true -let user_warning = ref false -(** User explicitly set warning *) - -let set_warning p = - let () = user_warning := true in - match p with - | "all" -> make_warn true - | "none" -> make_warn false - | _ -> prerr_endline ("Error: all/none expected after option w"); exit 1 - let toplevel_default_name = DirPath.make [Id.of_string "Top"] let toplevel_name = ref (Some toplevel_default_name) let set_toplevel_name dir = @@ -142,18 +132,27 @@ let unset_toplevel_name () = toplevel_name := None let remove_top_ml () = Mltop.remove () +let warn_deprecated_inputstate = + CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" + (fun () -> strbrk "The inputstate option is deprecated and discouraged.") + let inputstate = ref "" let set_inputstate s = - let () = Feedback.msg_warning (str "The inputstate option is deprecated and discouraged.") in + warn_deprecated_inputstate (); inputstate:=s let inputstate () = if not (String.is_empty !inputstate) then let fname = Loadpath.locate_file (CUnix.make_suffix !inputstate ".coq") in intern_state fname +let warn_deprecated_outputstate = + CWarnings.create ~name:"deprecated-outputstate" ~category:"deprecated" + (fun () -> + strbrk "The outputstate option is deprecated and discouraged.") + let outputstate = ref "" let set_outputstate s = - let () = Feedback.msg_warning (str "The outputstate option is deprecated and discouraged.") in + warn_deprecated_outputstate (); outputstate:=s let outputstate () = if not (String.is_empty !outputstate) then @@ -532,7 +531,7 @@ let parse_args arglist = |"-control-channel" -> Spawned.control_channel := get_host_port opt (next()) |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Vio2Vo |"-toploop" -> set_toploop (next ()) - |"-w" -> set_warning (next ()) + |"-w" | "-W" -> CWarnings.set_flags (next ()) |"-o" -> Flags.compilation_output_name := Some (next()) (* Options with zero arg *) @@ -640,7 +639,7 @@ let init_toplevel arglist = engage (); (* Be careful to set these variables after the inputstate *) Syntax_def.set_verbose_compat_notations !verb_compat_ntn; - Syntax_def.set_compat_notations (not !no_compat_ntn); +(* Syntax_def.set_compat_notations (not !no_compat_ntn); FIXME *) if (not !batch_mode || List.is_empty !compile_list) && Global.env_is_initial () then Option.iter Declaremods.start_library !toplevel_name; @@ -677,7 +676,6 @@ let start () = let () = init_toplevel (List.tl (Array.to_list Sys.argv)) in (* In batch mode, Coqtop has already exited at this point. In interactive one, dump glob is nothing but garbage ... *) - if not !user_warning then make_warn true; !toploop_run (); exit 1 diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index a48bbf89d..bbee39c3d 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -150,7 +150,7 @@ let alarm what internal msg = | UserAutomaticRequest | InternalTacticRequest -> (if debug then - Feedback.msg_warning + Feedback.msg_debug (hov 0 msg ++ fnl () ++ what ++ str " not defined.")); None | _ -> Some msg @@ -295,6 +295,11 @@ let declare_rewriting_schemes ind = (define_individual_scheme rew_l2r_forward_dep_scheme_kind UserAutomaticRequest None) ind end +let warn_cannot_build_congruence = + CWarnings.create ~name:"cannot-build-congruence" ~category:"schemes" + (fun () -> + strbrk "Cannot build congruence scheme because eq is not found") + let declare_congr_scheme ind = if Hipattern.is_equality_type (mkInd ind) then begin if @@ -303,7 +308,7 @@ let declare_congr_scheme ind = then ignore (define_individual_scheme congr_scheme_kind UserAutomaticRequest None ind) else - Feedback.msg_warning (strbrk "Cannot build congruence scheme because eq is not found") + warn_cannot_build_congruence () end let declare_sym_scheme ind = diff --git a/toplevel/locality.ml b/toplevel/locality.ml index c4c891b89..62aa85160 100644 --- a/toplevel/locality.ml +++ b/toplevel/locality.ml @@ -26,6 +26,11 @@ let check_locality locality_flag = (* Commands which supported an inlined Local flag *) +let warn_deprecated_local_syntax = + CWarnings.create ~name:"deprecated-local-syntax" ~category:"deprecated" + (fun () -> + Pp.strbrk "Deprecated syntax: use \"Local\" as a prefix.") + let enforce_locality_full locality_flag local = let local = match locality_flag with @@ -35,8 +40,8 @@ let enforce_locality_full locality_flag local = Errors.error "Use only prefix \"Local\"." | None -> if local then begin - Feedback.msg_warning (Pp.str "Obsolete syntax: use \"Local\" as a prefix."); - Some true + warn_deprecated_local_syntax (); + Some true end else None | Some b -> Some b in diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index e772ea020..aa6601a7d 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -864,16 +864,23 @@ let check_rule_productivity l = if (match l with SProdList _ :: _ -> true | _ -> false) then error "A recursive notation must start with at least one symbol." +let warn_notation_bound_to_variable = + CWarnings.create ~name:"notation-bound-to-variable" ~category:"parsing" + (fun () -> + strbrk "This notation will not be used for printing as it is bound to a single variable.") + +let warn_non_reversible_notation = + CWarnings.create ~name:"non-reversible-notation" ~category:"parsing" + (fun () -> + strbrk "This notation will not be used for printing as it is not reversible.") + let is_not_printable onlyparse noninjective = function | NVar _ -> - let () = if not onlyparse then - Feedback.msg_warning (strbrk "This notation will not be used for printing as it is bound to a single variable.") - in + if not onlyparse then warn_notation_bound_to_variable (); true | _ -> - if not onlyparse && noninjective then - let () = Feedback.msg_warning (strbrk "This notation will not be used for printing as it is not reversible.") in - true + if not onlyparse && noninjective then + (warn_non_reversible_notation (); true) else onlyparse let find_precedence lev etyps symbols = @@ -928,6 +935,10 @@ let check_curly_brackets_notation_exists () = error "Notations involving patterns of the form \"{ _ }\" are treated \n\ specially and require that the notation \"{ _ }\" is already reserved." +let warn_skip_spaces_curly = + CWarnings.create ~name:"skip-spaces-curly" ~category:"parsing" + (fun () ->strbrk "Skipping spaces inside curly brackets") + (* Remove patterns of the form "{ _ }", unless it is the "{ _ }" notation *) let remove_curly_brackets l = let rec skip_break acc = function @@ -942,9 +953,10 @@ let remove_curly_brackets l = let br',next' = skip_break [] l' in (match next' with | Terminal "}" as t2 :: l'' as l1 -> - if not (List.equal Notation.symbol_eq l l0) || not (List.equal Notation.symbol_eq l' l1) then - Feedback.msg_warning (strbrk "Skipping spaces inside curly brackets"); - if deb && List.is_empty l'' then [t1;x;t2] else begin + if not (List.equal Notation.symbol_eq l l0) || + not (List.equal Notation.symbol_eq l' l1) then + warn_skip_spaces_curly (); + if deb && List.is_empty l'' then [t1;x;t2] else begin check_curly_brackets_notation_exists (); x :: aux false l'' end diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 36c16208c..acd8026f9 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -146,7 +146,12 @@ let dir_ml_load s = let dir_ml_use s = match !load with | WithTop t -> t.use_file s - | _ -> Feedback.msg_warning (str "Cannot access the ML compiler") + | _ -> + let moreinfo = + if Dynlink.is_native then " Loading ML code works only in bytecode." + else "" + in + errorlabstrm "Mltop.dir_ml_use" (str "Could not load ML code." ++ str moreinfo) (* Adds a path to the ML paths *) let add_ml_dir s = @@ -161,12 +166,22 @@ let add_rec_ml_dir unix_path = (* Adding files to Coq and ML loadpath *) +let warn_cannot_use_directory = + CWarnings.create ~name:"cannot-use-directory" ~category:"filesystem" + (fun d -> + str "Directory " ++ str d ++ + strbrk " cannot be used as a Coq identifier (skipped)") + let convert_string d = try Names.Id.of_string d with UserError _ -> - Feedback.msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)"); + warn_cannot_use_directory d; raise Exit +let warn_cannot_open_path = + CWarnings.create ~name:"cannot-open-path" ~category:"filesystem" + (fun unix_path -> str "Cannot open " ++ str unix_path) + let add_rec_path ~unix_path ~coq_root ~implicit = if exists_dir unix_path then let dirs = all_subdirs ~unix_path in @@ -184,7 +199,7 @@ let add_rec_path ~unix_path ~coq_root ~implicit = let () = List.iter add dirs in Loadpath.add_load_path unix_path ~implicit coq_root else - Feedback.msg_warning (str "Cannot open " ++ str unix_path) + warn_cannot_open_path unix_path (* convertit un nom quelconque en nom de fichier ou de module *) let mod_of_name name = diff --git a/toplevel/record.ml b/toplevel/record.ml index fe6ed55a7..3151b1372 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -173,6 +173,13 @@ type record_error = | MissingProj of Id.t * Id.t list | BadTypedProj of Id.t * env * Type_errors.type_error +let warn_cannot_define_projection = + CWarnings.create ~name:"cannot-define-projection" ~category:"records" + (fun msg -> hov 0 msg) + +(* If a projection is not definable, we throw an error if the user +asked it to be a coercion. Otherwise, we just print an info +message. The user might still want to name the field of the record. *) let warning_or_error coe indsp err = let st = match err with | MissingProj (fi,projs) -> @@ -197,7 +204,7 @@ let warning_or_error coe indsp err = (pr_id fi ++ strbrk " cannot be defined because it is not typable.") in if coe then errorlabstrm "structure" st; - Flags.if_verbose Feedback.msg_warning (hov 0 st) + Flags.if_verbose Feedback.msg_info (hov 0 st) type field_status = | NoProjection of Name.t @@ -240,6 +247,12 @@ let instantiate_possibly_recursive_type indu paramdecls fields = let subst = List.map_i (fun i _ -> mkRel i) 1 paramdecls in Termops.substl_rel_context (subst@[mkIndU indu]) fields +let warn_non_primitive_record = + CWarnings.create ~name:"non-primitive-record" ~category:"record" + (fun (env,indsp) -> + (hov 0 (str "The record " ++ Printer.pr_inductive env indsp ++ + strbrk" could not be defined as a primitive record"))) + (* We build projections *) let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields = let env = Global.env() in @@ -263,9 +276,7 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field | Some None | None -> false in if not is_primitive then - Flags.if_verbose Feedback.msg_warning - (hov 0 (str "The record " ++ Printer.pr_inductive env indsp ++ - str" could not be defined as a primitive record")); + warn_non_primitive_record (env,indsp); is_primitive else false in diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index ac9293d5f..972d83055 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -18,14 +18,15 @@ open Vernacexpr Use the module Coqtoplevel, which catches these exceptions (the exceptions are explained only at the toplevel). *) -(* The navigation vernac commands will be handled separately *) +(* Navigation commands are allowed in a coqtop session but not in a .v file *) let rec is_navigation_vernac = function | VernacResetInitial | VernacResetName _ | VernacBacktrack _ | VernacBackTo _ - | VernacBack _ -> true + | VernacBack _ + | VernacStm _ -> true | VernacRedirect (_, (_,c)) | VernacTime (_,c) -> is_navigation_vernac c (* Time Back* is harmless *) @@ -230,6 +231,7 @@ and read_vernac_file verbosely s = * raised, which means that we raised the end of the file being loaded *) while true do let loc_ast = parse_sentence input in + CWarnings.set_current_loc (fst loc_ast); vernac_com verbosely checknav loc_ast done with any -> (* whatever the exception *) @@ -272,11 +274,17 @@ let load_vernac verb file = if !Flags.beautify_file then close_out !chan_beautify; iraise (disable_drop e, info) +let warn_file_no_extension = + CWarnings.create ~name:"file-no-extension" ~category:"filesystem" + (fun (f,ext) -> + str "File \"" ++ str f ++ + strbrk "\" has been implicitly expanded to \"" ++ + str f ++ str ext ++ str "\"") + let ensure_ext ext f = if Filename.check_suffix f ext then f else begin - Feedback.msg_warning (str "File \"" ++ str f ++ strbrk "\" has been implicitly \ - expanded to \"" ++ str f ++ str ext ++ str "\""); + warn_file_no_extension (f,ext); f ^ ext end diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 82fe9751e..65aa46bc1 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -896,7 +896,11 @@ let vernac_chdir = function | Some path -> begin try Sys.chdir (expand path) - with Sys_error err -> Feedback.msg_warning (str "Cd failed: " ++ str err) + with Sys_error err -> + (* Cd is typically used to control the output directory of + extraction. A failed Cd could lead to overwriting .ml files + so we make it an error. *) + Errors.error ("Cd failed: " ^ err) end; if_verbose Feedback.msg_info (str (Sys.getcwd())) @@ -943,6 +947,16 @@ let vernac_declare_implicits locality r l = Impargs.declare_manual_implicits local (smart_global r) ~enriching:false (List.map (List.map (fun (ex,b,f) -> ex, (b,true,f))) imps) +let warn_arguments_assert = + CWarnings.create ~name:"arguments-assert" ~category:"vernacular" + (fun sr -> + strbrk "This command is just asserting the number and names of arguments of " ++ + pr_global sr ++ strbrk". If this is what you want add " ++ + strbrk "': assert' to silence the warning. If you want " ++ + strbrk "to clear implicit arguments add ': clear implicits'. " ++ + strbrk "If you want to clear notation scopes add ': clear scopes'") + + let vernac_declare_arguments locality r l nargs flags = let extra_scope_flag = List.mem `ExtraScopes flags in let names = List.map (List.map (fun (id, _,_,_,_) -> id)) l in @@ -1071,7 +1085,7 @@ let vernac_declare_arguments locality r l nargs flags = some_scopes_specified || some_simpl_flags_specified) && no_flags then - Feedback.msg_warning (strbrk "This command is just asserting the number and names of arguments of " ++ pr_global sr ++ strbrk". If this is what you want add ': assert' to silence the warning. If you want to clear implicit arguments add ': clear implicits'. If you want to clear notation scopes add ': clear scopes'") + warn_arguments_assert sr let default_env () = { @@ -1342,6 +1356,15 @@ let _ = optread = (fun () -> !Constrintern.parsing_explicit); optwrite = (fun b -> Constrintern.parsing_explicit := b) } +let _ = + declare_string_option + { optsync = true; + optdepr = false; + optname = "warnings display"; + optkey = ["Warnings"]; + optread = CWarnings.get_flags; + optwrite = CWarnings.set_flags } + let vernac_set_strategy locality l = let local = make_locality locality in let glob_ref r = @@ -1855,12 +1878,12 @@ let interp ?proof ~loc locality poly c = | VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n") (* The STM should handle that, but LOAD bypasses the STM... *) - | VernacAbort id -> Feedback.msg_warning (str "VernacAbort not handled by Stm") - | VernacAbortAll -> Feedback.msg_warning (str "VernacAbortAll not handled by Stm") - | VernacRestart -> Feedback.msg_warning (str "VernacRestart not handled by Stm") - | VernacUndo _ -> Feedback.msg_warning (str "VernacUndo not handled by Stm") - | VernacUndoTo _ -> Feedback.msg_warning (str "VernacUndoTo not handled by Stm") - | VernacBacktrack _ -> Feedback.msg_warning (str "VernacBacktrack not handled by Stm") + | VernacAbort id -> Errors.errorlabstrm "" (str "Abort cannot be used through the Load command") + | VernacAbortAll -> Errors.errorlabstrm "" (str "AbortAll cannot be used through the Load command") + | VernacRestart -> Errors.errorlabstrm "" (str "Restart cannot be used through the Load command") + | VernacUndo _ -> Errors.errorlabstrm "" (str "Undo cannot be used through the Load command") + | VernacUndoTo _ -> Errors.errorlabstrm "" (str "UndoTo cannot be used through the Load command") + | VernacBacktrack _ -> Errors.errorlabstrm "" (str "Backtrack cannot be used through the Load command") (* Proof management *) | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t,None)] false diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index 1116a3104..0abc9e76d 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -42,6 +42,11 @@ let vinterp_map s = let vinterp_init () = Hashtbl.clear vernac_tab +let warn_deprecated_command = + let open CWarnings in + create ~name:"deprecated-command" ~category:"deprecated" + (fun pr -> str "Deprecated vernacular command: " ++ pr) + (* Interpretation of a vernac command *) let call ?locality (opn,converted_args) = @@ -55,7 +60,7 @@ let call ?locality (opn,converted_args) = | Egramml.GramNonTerminal _ -> str "_" in let pr = pr_sequence pr_gram rules in - Feedback.msg_warning (str "Deprecated vernacular command: " ++ pr) + warn_deprecated_command pr; in loc:= "Checking arguments"; let hunk = callback converted_args in -- cgit v1.2.3