diff options
82 files changed, 892 insertions, 484 deletions
diff --git a/Makefile.build b/Makefile.build index e53ebf2e6..7dff7f2fc 100644 --- a/Makefile.build +++ b/Makefile.build @@ -388,8 +388,9 @@ $(OCAMLLIBDEP): $(call bestobj, tools/ocamllibdep.cmo) # The full coqdep (unused by this build, but distributed by make install) -COQDEPCMO:=lib/clib.cma lib/errors.cmo lib/minisys.cmo lib/system.cmo \ - tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo +COQDEPCMO:=lib/clib.cma lib/errors.cmo lib/cWarnings.cmo lib/minisys.cmo \ + lib/system.cmo tools/coqdep_lexer.cmo tools/coqdep_common.cmo \ + tools/coqdep.cmo $(COQDEP): $(call bestobj, $(COQDEPCMO)) $(SHOW)'OCAMLBEST -o $@' diff --git a/checker/check.mllib b/checker/check.mllib index 2fa4d5797..1925477e0 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -35,6 +35,7 @@ Segmenttree Unicodetable Unicode Errors +CWarnings CEphemeron Future CUnix diff --git a/dev/printers.mllib b/dev/printers.mllib index e39b78072..e15855ef2 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -38,6 +38,7 @@ Segmenttree Unicodetable Unicode Errors +CWarnings Bigint CUnix Minisys diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index ac6a7ac7f..2ec6430fd 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -111,14 +111,8 @@ let declare_tactic loc s c cl = match cl with declare_str_items loc [ <:str_item< do { let obj () = Tacenv.register_ltac True False $name$ $body$ in - try do { - Tacenv.register_ml_tactic $se$ [|$tac$|]; - Mltop.declare_cache_obj obj $plugin_name$; } - with [ e when Errors.noncritical e -> - Feedback.msg_warning - (Pp.app - (Pp.str ("Exception in tactic extend " ^ $entry$ ^": ")) - (Errors.print e)) ]; } >> + Tacenv.register_ml_tactic $se$ [|$tac$|]; + Mltop.declare_cache_obj obj $plugin_name$; } >> ] | _ -> (** Otherwise we add parsing and printing rules to generate a call to a @@ -129,14 +123,8 @@ let declare_tactic loc s c cl = match cl with let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ $gl$ >> in declare_str_items loc [ <:str_item< do { - try do { Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc s cl$); - Mltop.declare_cache_obj $obj$ $plugin_name$; } - with [ e when Errors.noncritical e -> - Feedback.msg_warning - (Pp.app - (Pp.str ("Exception in tactic extend " ^ $entry$ ^": ")) - (Errors.print e)) ]; } >> + Mltop.declare_cache_obj $obj$ $plugin_name$; } >> ] open Pcaml diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index ce0431889..04b117fba 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -122,14 +122,8 @@ let declare_command loc s c nt cl = let classl = make_fun_classifiers loc s c cl in declare_str_items loc [ <:str_item< do { - try do { - CList.iteri (fun i (depr, f) -> Vernacinterp.vinterp_add depr ($se$, i) f) $funcl$; - CList.iteri (fun i f -> Vernac_classifier.declare_vernac_classifier ($se$, i) f) $classl$ } - with [ e when Errors.noncritical e -> - Feedback.msg_warning - (Pp.app - (Pp.str ("Exception in vernac extend " ^ $se$ ^": ")) - (Errors.print e)) ]; + CList.iteri (fun i (depr, f) -> Vernacinterp.vinterp_add depr ($se$, i) f) $funcl$; + CList.iteri (fun i f -> Vernac_classifier.declare_vernac_classifier ($se$, i) f) $classl$; CList.iteri (fun i r -> Egramml.extend_vernac_command_grammar ($se$, i) $nt$ r) $gl$; } >> ] diff --git a/ide/coqOps.ml b/ide/coqOps.ml index f0e767cba..18557ab6b 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -14,15 +14,17 @@ open Feedback let b2c = byte_offset_to_char_offset -type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of Loc.t * string ] -type mem_flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR ] +type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of Loc.t * string | `WARNING of Loc.t * string ] +type mem_flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR | `WARNING ] let mem_flag_of_flag : flag -> mem_flag = function | `ERROR _ -> `ERROR + | `WARNING _ -> `WARNING | (`INCOMPLETE | `UNSAFE | `PROCESSING) as mem_flag -> mem_flag let str_of_flag = function | `UNSAFE -> "U" | `PROCESSING -> "P" | `ERROR _ -> "E" + | `WARNING _ -> "W" | `INCOMPLETE -> "I" class type signals = @@ -470,6 +472,13 @@ object(self) self#attach_tooltip sentence loc msg; if not (Loc.is_ghost loc) then self#position_error_tag_at_sentence sentence (Some (Loc.unloc loc)) + | Message(Warning, loc, msg), Some (id,sentence) -> + let loc = Option.default Loc.ghost loc in + let msg = Richpp.raw_print msg in + log "WarningMsg" id; + add_flag sentence (`WARNING (loc, msg)); + self#attach_tooltip sentence loc msg; + self#position_warning_tag_at_sentence sentence loc | InProgress n, _ -> if n < 0 then processed <- processed + abs n else to_process <- to_process + n @@ -511,6 +520,18 @@ object(self) let start, _, phrase = self#get_sentence sentence in self#position_error_tag_at_iter start phrase loc + method private position_warning_tag_at_iter iter_start iter_stop phrase loc = + if Loc.is_ghost loc then + buffer#apply_tag Tags.Script.warning ~start:iter_start ~stop:iter_stop + else + buffer#apply_tag Tags.Script.warning + ~start:(iter_start#forward_chars (b2c phrase loc.Loc.bp)) + ~stop:(iter_stop#forward_chars (b2c phrase loc.Loc.ep)) + + method private position_warning_tag_at_sentence sentence loc = + let start, stop, phrase = self#get_sentence sentence in + self#position_warning_tag_at_iter start stop phrase loc + method private process_interp_error queue sentence loc msg tip id = Coq.bind (Coq.return ()) (function () -> let start, stop, phrase = self#get_sentence sentence in diff --git a/ide/sentence.ml b/ide/sentence.ml index 6897779e8..e332682dd 100644 --- a/ide/sentence.ml +++ b/ide/sentence.ml @@ -16,6 +16,7 @@ let split_slice_lax (buffer:GText.buffer) start stop = buffer#remove_tag ~start ~stop Tags.Script.sentence; buffer#remove_tag ~start ~stop Tags.Script.error; + buffer#remove_tag ~start ~stop Tags.Script.warning; buffer#remove_tag ~start ~stop Tags.Script.error_bg; let slice = buffer#get_text ~start ~stop () in let apply_tag off tag = diff --git a/ide/session.ml b/ide/session.ml index cdec392ec..e99833760 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -195,12 +195,8 @@ let set_buffer_handlers to a point indicated by coq. *) if !no_coq_action_required then begin let start, stop = get_start (), get_stop () in - buffer#remove_tag Tags.Script.error ~start ~stop; - buffer#remove_tag Tags.Script.error_bg ~start ~stop; - buffer#remove_tag Tags.Script.tooltip ~start ~stop; - buffer#remove_tag Tags.Script.processed ~start ~stop; - buffer#remove_tag Tags.Script.to_process ~start ~stop; - buffer#remove_tag Tags.Script.incomplete ~start ~stop; + List.iter (fun tag -> buffer#remove_tag tag ~start ~stop) + Tags.Script.ephemere; Sentence.tag_on_insert buffer end; end in diff --git a/ide/tags.ml b/ide/tags.ml index 9ccff9fb5..e4510e7af 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -18,6 +18,7 @@ struct let table = GText.tag_table () let comment = make_tag table ~name:"comment" [] let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE] + let warning = make_tag table ~name:"warning" [`UNDERLINE `SINGLE; `FOREGROUND "blue"] let error_bg = make_tag table ~name:"error_bg" [] let to_process = make_tag table ~name:"to_process" [] let processed = make_tag table ~name:"processed" [] @@ -29,9 +30,11 @@ struct let sentence = make_tag table ~name:"sentence" [] let tooltip = make_tag table ~name:"tooltip" [] (* debug:`BACKGROUND "blue" *) + let ephemere = + [error; warning; error_bg; tooltip; processed; to_process; incomplete; unjustified] + let all = - [comment; error; error_bg; to_process; processed; incomplete; unjustified; - found; sentence; tooltip] + comment :: found :: sentence :: ephemere let edit_zone = let t = make_tag table ~name:"edit_zone" [`UNDERLINE `SINGLE] in diff --git a/ide/tags.mli b/ide/tags.mli index 5a932f330..02e15a5ae 100644 --- a/ide/tags.mli +++ b/ide/tags.mli @@ -11,6 +11,7 @@ sig val table : GText.tag_table val comment : GText.tag val error : GText.tag + val warning : GText.tag val error_bg : GText.tag val to_process : GText.tag val processed : GText.tag @@ -20,6 +21,7 @@ sig val sentence : GText.tag val tooltip : GText.tag val edit_zone : GText.tag (* for debugging *) + val ephemere : GText.tag list val all : GText.tag list end diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 5c5a900fb..74de6f67f 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1166,10 +1166,6 @@ let alias_of als = match als.alias_ids with | [] -> Anonymous | id :: _ -> Name id -let message_redundant_alias id1 id2 = - Feedback.msg_warning - (str "Alias variable " ++ pr_id id1 ++ str " is merged with " ++ pr_id id2) - (** {6 Expanding notations } @returns a raw_case_pattern_expr : @@ -1742,7 +1738,6 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = let env_ids = List.fold_right Id.Set.add eqn_ids env.ids in List.map (fun (asubst,pl) -> let rhs = replace_vars_constr_expr asubst rhs in - Id.Map.iter message_redundant_alias asubst; let rhs' = intern {env with ids = env_ids} rhs in (loc,eqn_ids,pl,rhs')) pll diff --git a/interp/notation.ml b/interp/notation.ml index e777e5c24..b0a219200 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -190,7 +190,8 @@ let declare_delimiters scope key = | None -> scope_map := String.Map.add scope newsc !scope_map | Some oldkey when String.equal oldkey key -> () | Some oldkey -> - Feedback.msg_warning + (** FIXME: implement multikey scopes? *) + Flags.if_verbose Feedback.msg_info (str "Overwriting previous delimiting key " ++ str oldkey ++ str " in scope " ++ str scope); scope_map := String.Map.add scope newsc !scope_map end; @@ -198,7 +199,7 @@ let declare_delimiters scope key = let oldscope = String.Map.find key !delimiters_map in if String.equal oldscope scope then () else begin - Feedback.msg_warning (str "Hiding binding of key " ++ str key ++ str " to " ++ str oldscope); + Flags.if_verbose Feedback.msg_info (str "Hiding binding of key " ++ str key ++ str " to " ++ str oldscope); delimiters_map := String.Map.add key scope !delimiters_map end with Not_found -> delimiters_map := String.Map.add key scope !delimiters_map @@ -207,7 +208,7 @@ let remove_delimiters scope = let sc = find_scope scope in let newsc = { sc with delimiters = None } in match sc.delimiters with - | None -> Feedback.msg_warning (str "No bound key for scope " ++ str scope ++ str ".") + | None -> Errors.errorlabstrm "" (str "No bound key for scope " ++ str scope ++ str ".") | Some key -> scope_map := String.Map.add scope newsc !scope_map; try @@ -386,6 +387,12 @@ let level_of_notation ntn = (* The mapping between notations and their interpretation *) +let warn_notation_overridden = + CWarnings.create ~name:"notation-overridden" ~category:"parsing" + (fun (ntn,which_scope) -> + str "Notation" ++ spc () ++ str ntn ++ spc () + ++ strbrk "was already used" ++ which_scope) + let declare_notation_interpretation ntn scopt pat df ~onlyprint = let scope = match scopt with Some s -> s | None -> default_scope in let sc = find_scope scope in @@ -393,8 +400,8 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint = if String.Map.mem ntn sc.notations then let which_scope = match scopt with | None -> mt () - | Some _ -> str " in scope " ++ str scope in - Feedback.msg_warning (str "Notation " ++ str ntn ++ str " was already used" ++ which_scope) + | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in + warn_notation_overridden (ntn,which_scope) in let notdata = { not_interp = pat; diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 9a1483b10..7170fd14a 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -84,23 +84,26 @@ let declare_syntactic_definition local id onlyparse pat = let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Id.Set.empty kn) -let allow_compat_notations = ref true -let verbose_compat_notations = ref false +let verbose_compat_notations = ref true let is_verbose_compat () = - !verbose_compat_notations || not !allow_compat_notations + !verbose_compat_notations + +let pr_compat_warning (kn, def, v) = + let pp_def = match def with + | [], NRef r -> spc () ++ str "is" ++ spc () ++ pr_global_env Id.Set.empty r + | _ -> strbrk " is a compatibility notation" + in + let since = strbrk " since Coq > " ++ str (Flags.pr_version v) ++ str "." in + pr_syndef kn ++ pp_def ++ since + +let warn_compatibility_notation = + CWarnings.create ~name:"compatibility-notation" + ~category:"deprecated" pr_compat_warning let verbose_compat kn def = function | Some v when is_verbose_compat () && Flags.version_strictly_greater v -> - let act = - if !verbose_compat_notations then Feedback.msg_warning ?loc:None else errorlabstrm "" - in - let pp_def = match def with - | [], NRef r -> str " is " ++ pr_global_env Id.Set.empty r - | _ -> str " is a compatibility notation" - in - let since = str " since Coq > " ++ str (Flags.pr_version v) ++ str "." in - act (pr_syndef kn ++ pp_def ++ since) + warn_compatibility_notation (kn, def, v) | _ -> () let search_syntactic_definition kn = @@ -119,12 +122,3 @@ let set_verbose_compat_notations = optkey = ["Verbose";"Compat";"Notations"]; optread = (fun () -> !verbose_compat_notations); optwrite = ((:=) verbose_compat_notations) } - -let set_compat_notations = - declare_bool_option - { optsync = true; - optdepr = false; - optname = "accept compatibility notations"; - optkey = ["Compat"; "Notations"]; - optread = (fun () -> !allow_compat_notations); - optwrite = ((:=) allow_compat_notations) } diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index 7a1c9c5cb..aa2c9c3c1 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -18,8 +18,5 @@ val declare_syntactic_definition : bool -> Id.t -> val search_syntactic_definition : kernel_name -> syndef_interpretation -(** Options concerning verbose display of compatibility notations - or their deactivation *) - +(** Option concerning verbose display of compatibility notations *) val set_verbose_compat_notations : bool -> unit -val set_compat_notations : bool -> unit diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index a0ef5e570..8cbc3ab44 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -907,7 +907,8 @@ let compile fail_on_error ?universes:(universes=0) env c = Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ; Some (init_code,!fun_code, Array.of_list fv) with TooLargeInductive tname -> - let fn = if fail_on_error then Errors.errorlabstrm "compile" else Feedback.msg_warning ?loc:None in + let fn = if fail_on_error then Errors.errorlabstrm "compile" else + (fun x -> Feedback.msg_warning x) in (Pp.(fn (str "Cannot compile code for virtual machine as it uses inductive " ++ Id.print tname ++ str str_max_constructors)); diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index a0ff9e123..2f985e15a 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -145,11 +145,16 @@ let native_conv_gen pb sigma env univs t1 t2 = end | _ -> anomaly (Pp.str "Compilation failure") +let warn_no_native_compiler = + let open Pp in + CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler" + (fun () -> strbrk "Native compiler is disabled," ++ + strbrk " falling back to VM conversion test.") + (* Wrapper for [native_conv] above *) let native_conv cv_pb sigma env t1 t2 = if Coq_config.no_native_compiler then begin - let msg = "Native compiler is disabled, falling back to VM conversion test." in - Feedback.msg_warning (Pp.str msg); + warn_no_native_compiler (); vm_conv cv_pb env t1 t2 end else diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 5b92e9554..d4a67b399 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -55,6 +55,15 @@ let write_ml_code fn ?(header=[]) code = List.iter (pp_global fmt) (header@code); close_out ch_out +let warn_native_compiler_failed = + let print = function + | Inl (Unix.WEXITED n) -> Pp.(strbrk "Native compiler exited with status" ++ str" " ++ int n) + | Inl (Unix.WSIGNALED n) -> Pp.(strbrk "Native compiler killed by signal" ++ str" " ++ int n) + | Inl (Unix.WSTOPPED n) -> Pp.(strbrk "Native compiler stopped by signal" ++ str" " ++ int n) + | Inr e -> Pp.(strbrk "Native compiler failed with error: " ++ strbrk (Unix.error_message e)) + in + CWarnings.create ~name:"native-compiler-failed" ~category:"native-compiler" print + let call_compiler ml_filename = let load_path = !get_load_paths () in let load_path = List.map (fun dn -> dn / output_dir) load_path in @@ -78,15 +87,12 @@ let call_compiler ml_filename = let res = CUnix.sys_command (ocamlfind ()) args in let res = match res with | Unix.WEXITED 0 -> true - | Unix.WEXITED n -> - Feedback.msg_warning Pp.(str "command exited with status " ++ int n); false - | Unix.WSIGNALED n -> - Feedback.msg_warning Pp.(str "command killed by signal " ++ int n); false - | Unix.WSTOPPED n -> - Feedback.msg_warning Pp.(str "command stopped by signal " ++ int n); false in + | Unix.WEXITED n | Unix.WSIGNALED n | Unix.WSTOPPED n -> + warn_native_compiler_failed (Inl res); false + in res, link_filename with Unix.Unix_error (e,_,_) -> - Feedback.msg_warning Pp.(str (Unix.error_message e)); + warn_native_compiler_failed (Inr e); false, link_filename let compile fn code = diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 30a346c91..710bfa19b 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -676,12 +676,18 @@ let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_sta let vm_conv = ref (fun cv_pb env -> gen_conv cv_pb env ~evars:((fun _->None), universes env)) +let warn_bytecode_compiler_failed = + let open Pp in + CWarnings.create ~name:"bytecode-compiler-failed" ~category:"bytecode-compiler" + (fun () -> strbrk "Bytecode compiler failed, " ++ + strbrk "falling back to standard conversion") + let set_vm_conv (f:conv_pb -> Term.types kernel_conversion_function) = vm_conv := f let vm_conv cv_pb env t1 t2 = try !vm_conv cv_pb env t1 t2 with Not_found | Invalid_argument _ -> - Feedback.msg_warning (Pp.str "Bytecode compilation failed, falling back to standard conversion"); + warn_bytecode_compiler_failed (); gen_conv cv_pb env t1 t2 let default_conv cv_pb ?(l2r=false) env t1 t2 = diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 1b5e5e32a..389644692 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -106,3 +106,5 @@ exception NotArity val dest_arity : env -> types -> arity (* raises NotArity if not an arity *) val is_arity : env -> types -> bool + +val warn_bytecode_compiler_failed : ?loc:Loc.t -> unit -> unit diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 53db6f5be..c729a6ce2 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -185,10 +185,9 @@ let vm_conv_gen cv_pb env univs t1 t2 = let v2 = val_of_constr env t2 in fst (conv_val env cv_pb (nb_rel env) v1 v2 univs) with Not_found | Invalid_argument _ -> - (Feedback.msg_warning - (Pp.str "Bytecode compilation failed, falling back to default conversion"); - Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None) - full_transparent_state env univs t1 t2) + warn_bytecode_compiler_failed (); + Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None) + full_transparent_state env univs t1 t2 let vm_conv cv_pb env t1 t2 = let univs = Environ.universes env in diff --git a/lib/aux_file.ml b/lib/aux_file.ml index 096305b98..c6c7b4242 100644 --- a/lib/aux_file.ml +++ b/lib/aux_file.ml @@ -87,8 +87,7 @@ let load_aux_file_for vfile = | End_of_file -> !h | Sys_error s | Scanf.Scan_failure s | Failure s | Invalid_argument s -> - Flags.if_verbose - Feedback.msg_warning Pp.(str"Loading file "++str aux_fname++str": "++str s); + Flags.if_verbose Feedback.msg_info Pp.(str"Loading file "++str aux_fname++str": "++str s); empty_aux_file let set h loc k v = set h (Loc.unloc loc) k v diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml new file mode 100644 index 000000000..68442bd7c --- /dev/null +++ b/lib/cWarnings.ml @@ -0,0 +1,120 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp + +type status = + Disabled | Enabled | AsError + +type t = { + default : status; + category : string; + status : status; +} + +let warnings : (string, t) Hashtbl.t = Hashtbl.create 97 +let categories : (string, string list) Hashtbl.t = Hashtbl.create 97 + +let current_loc = ref Loc.ghost +let flags = ref "" + +let set_current_loc = (:=) current_loc + +let get_flags () = !flags + +let add_warning_in_category ~name ~category = + let ws = + try + Hashtbl.find categories category + with Not_found -> [] + in + Hashtbl.replace categories category (name::ws) + +let create ~name ~category ?(default=Enabled) pp = + Hashtbl.add warnings name { default; category; status = default }; + add_warning_in_category ~name ~category; + if default <> Disabled then + add_warning_in_category ~name ~category:"default"; + fun ?loc x -> let w = Hashtbl.find warnings name in + match w.status with + | Disabled -> () + | AsError -> + let loc = Option.default !current_loc loc in + Errors.user_err_loc (loc,"_",pp x) + | Enabled -> + let msg = + pp x ++ str " [" ++ str name ++ str "," ++ + str category ++ str "]" + in + let loc = Option.default !current_loc loc in + Feedback.msg_warning ~loc msg + +let warn_unknown_warning = + create ~name:"unknown-warning" ~category:"toplevel" + (fun name -> strbrk "Unknown warning name: " ++ str name) + +let set_warning_status ~name status = + try + let w = Hashtbl.find warnings name in + Hashtbl.replace warnings name { w with status = status } + with Not_found -> warn_unknown_warning name + +let reset_default_warnings () = + Hashtbl.iter (fun name w -> + Hashtbl.replace warnings name { w with status = w.default }) + warnings + +let set_all_warnings_status status = + Hashtbl.iter (fun name w -> + Hashtbl.replace warnings name { w with status }) + warnings + +let parse_flag s = + if String.length s > 1 then + match String.get s 0 with + | '+' -> (AsError, String.sub s 1 (String.length s - 1)) + | '-' -> (Disabled, String.sub s 1 (String.length s - 1)) + | _ -> (Enabled, s) + else Errors.error "Invalid warnings flag" + +let rec do_all_keyword = function + | [] -> [] + | (status, name as item) :: items -> + if CString.equal name "all" then + (set_all_warnings_status status; do_all_keyword items) + else item :: do_all_keyword items + +let rec do_categories = function + | [] -> [] + | (status, name as item) :: items -> + try + let names = Hashtbl.find categories name in + List.iter (fun name -> set_warning_status name status) names; + do_categories items + with Not_found -> item :: do_categories items + +let rec parse_warnings items = + List.iter (fun (status, name) -> set_warning_status ~name status) items + +(* For compatibility, we accept "none" *) +let parse_flags s = + if CString.equal s "none" then begin + Flags.make_warn false; + set_all_warnings_status Disabled + end + else begin + Flags.make_warn true; + let reg = Str.regexp "[ ,]+" in + let items = List.map parse_flag (Str.split reg s) in + let items = do_all_keyword items in + let items = do_categories items in + parse_warnings items + end + +let set_flags s = + flags := s; reset_default_warnings (); parse_flags s diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli new file mode 100644 index 000000000..351554284 --- /dev/null +++ b/lib/cWarnings.mli @@ -0,0 +1,34 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +type status = + Disabled | Enabled | AsError + +(* +type 'a repr = { + print : 'a -> Pp.std_ppcmds; + kind : string; + enabled : bool; +} + *) + +val set_current_loc : Loc.t -> unit + +val create : name:string -> category:string -> ?default:status -> + ('a -> Pp.std_ppcmds) -> ?loc:Loc.t -> 'a -> unit + +(* +val emit : 'a t -> 'a -> unit + +type any = Any : string * string * 'a repr -> any + +val dump : unit -> any list + *) + +val get_flags : unit -> string +val set_flags : string -> unit diff --git a/lib/feedback.ml b/lib/feedback.ml index bedbe226c..0ec3b2ebe 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -80,31 +80,33 @@ let info_str = mt () let warn_str = str "Warning:" ++ spc () let err_str = str "Error:" ++ spc () -let make_body quoter info s = quoter (hov 0 (info ++ s)) +let make_body quoter info ?loc s = + let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in + quoter (hov 0 (loc ++ info ++ s)) (* Generic logger *) let gen_logger dbg err ?loc level msg = match level with - | Debug -> msgnl (make_body dbg dbg_str msg) - | Info -> msgnl (make_body dbg info_str msg) + | Debug -> msgnl (make_body dbg dbg_str ?loc msg) + | Info -> msgnl (make_body dbg info_str ?loc msg) + (* XXX: What to do with loc here? *) | Notice -> msgnl msg | Warning -> Flags.if_warn (fun () -> - msgnl_with !err_ft (make_body err warn_str msg)) () - | Error -> msgnl_with !err_ft (make_body err err_str msg) + msgnl_with !err_ft (make_body err warn_str ?loc msg)) () + | Error -> msgnl_with !err_ft (make_body err err_str ?loc msg) (** Standard loggers *) let std_logger = gen_logger (fun x -> x) (fun x -> x) (* Color logger *) let color_terminal_logger ?loc level strm = - let msg = Ppstyle.color_msg in + let msg = Ppstyle.color_msg in match level with - | Debug -> msg ~header:("Debug", Ppstyle.debug_tag) !std_ft strm - | Info -> msg !std_ft strm - | Notice -> msg !std_ft strm - | Warning -> - let header = ("Warning", Ppstyle.warning_tag) in - Flags.if_warn (fun () -> msg ~header !err_ft strm) () - | Error -> msg ~header:("Error", Ppstyle.error_tag) !err_ft strm + | Debug -> msg ?loc ~header:("Debug", Ppstyle.debug_tag) !std_ft strm + | Info -> msg ?loc !std_ft strm + | Notice -> msg ?loc !std_ft strm + | Warning -> Flags.if_warn (fun () -> + msg ?loc ~header:("Warning", Ppstyle.warning_tag) !err_ft strm) () + | Error -> msg ?loc ~header:("Error", Ppstyle.error_tag) !err_ft strm (* Rules for emacs: - Debug/info: emacs_quote_info @@ -116,11 +118,11 @@ let emacs_logger = gen_logger emacs_quote_info emacs_quote_err let logger = ref std_logger let set_logger l = logger := l -let msg_info ?loc x = !logger Info x -let msg_notice ?loc x = !logger Notice x -let msg_warning ?loc x = !logger Warning x -let msg_error ?loc x = !logger Error x -let msg_debug ?loc x = !logger Debug x +let msg_info ?loc x = !logger ?loc Info x +let msg_notice ?loc x = !logger ?loc Notice x +let msg_warning ?loc x = !logger ?loc Warning x +let msg_error ?loc x = !logger ?loc Error x +let msg_debug ?loc x = !logger ?loc Debug x (** Feeders *) let feeder = ref ignore diff --git a/lib/flags.ml b/lib/flags.ml index ba19c7a63..13525165a 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -172,7 +172,7 @@ let make_polymorphic_flag b = let program_mode = ref false let is_program_mode () = !program_mode -let warn = ref false +let warn = ref true let make_warn flag = warn := flag; () let if_warn f x = if !warn then f x diff --git a/lib/lib.mllib b/lib/lib.mllib index a6c09058d..4b13156d6 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -1,4 +1,5 @@ Errors +CWarnings Bigint Segmenttree Unicodetable @@ -197,6 +197,25 @@ let strbrk s = else if p = n then [] else [str (String.sub s p (n-p))] in List.fold_left (++) Glue.empty (aux 0 0) +let pr_loc_pos loc = + if Loc.is_ghost loc then (str"<unknown>") + else + let loc = Loc.unloc loc in + int (fst loc) ++ str"-" ++ int (snd loc) + +let pr_loc loc = + if Loc.is_ghost loc then str"<unknown>" + else + let fname = loc.Loc.fname in + if CString.equal fname "" then + Loc.(str"Toplevel input, characters " ++ int loc.bp ++ + str"-" ++ int loc.ep ++ str":" ++ fnl ()) + else + Loc.(str"File " ++ str "\"" ++ str fname ++ str "\"" ++ + str", line " ++ int loc.line_nb ++ str", characters " ++ + int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++ + str":" ++ fnl()) + let ismt = is_empty (* boxing commands *) diff --git a/lib/pp.mli b/lib/pp.mli index a18744c37..3bd560812 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -166,6 +166,8 @@ val surround : std_ppcmds -> std_ppcmds val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds +val pr_loc : Loc.t -> std_ppcmds + (** {6 Low-level pretty-printing functions with and without flush} *) (** FIXME: These ignore the logging settings and call [Format] directly *) diff --git a/lib/ppstyle.ml b/lib/ppstyle.ml index b068788c9..ecfaa822c 100644 --- a/lib/ppstyle.ml +++ b/lib/ppstyle.ml @@ -124,15 +124,16 @@ let init_color_output () = Format.pp_set_formatter_tag_functions !std_ft tag_handler; Format.pp_set_formatter_tag_functions !err_ft tag_handler -let color_msg ?header ft strm = +let color_msg ?loc ?header ft strm = let pptag = tag in let open Pp in + let ploc = Option.cata Pp.pr_loc (Pp.mt ()) loc in let strm = match header with - | None -> hov 0 strm + | None -> hov 0 (ploc ++ strm) | Some (h, t) -> let tag = Pp.Tag.inj t pptag in let h = Pp.tag tag (str h ++ str ":") in - hov 0 (h ++ spc () ++ strm) + hov 0 (ploc ++ h ++ spc () ++ strm) in pp_with ~pp_tag ft strm; Format.pp_print_newline ft (); diff --git a/lib/ppstyle.mli b/lib/ppstyle.mli index 1cd701ed4..b07fcd5d4 100644 --- a/lib/ppstyle.mli +++ b/lib/ppstyle.mli @@ -48,7 +48,7 @@ val dump : unit -> (t * Terminal.style option) list val init_color_output : unit -> unit -val color_msg : ?header:string * Format.tag -> +val color_msg : ?loc:Loc.t -> ?header:string * Format.tag -> Format.formatter -> Pp.std_ppcmds -> unit (** {!color_msg ?header fmt pp} will format according to the tags defined in this file *) diff --git a/lib/system.ml b/lib/system.ml index 8b53a11d6..b27918522 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -18,6 +18,10 @@ include Minisys depth-first search, with sons ordered as on the file system; warns if [root] does not exist *) +let warn_cannot_open_dir = + CWarnings.create ~name:"cannot-open-dir" ~category:"filesystem" + (fun dir -> str ("Cannot open directory " ^ dir)) + let all_subdirs ~unix_path:root = let l = ref [] in let add f rel = l := (f, rel) :: !l in @@ -32,7 +36,7 @@ let all_subdirs ~unix_path:root = in check_unix_dir (fun s -> Feedback.msg_warning (str s)) root; if exists_dir root then traverse root [] - else Feedback.msg_warning (str ("Cannot open " ^ root)); + else warn_cannot_open_dir root; List.rev !l (* Caching directory contents for efficient syntactic equality of file @@ -85,19 +89,22 @@ let rec search paths test = | [] -> [] | lpe :: rem -> test lpe @ search rem test +let warn_ambiguous_file_name = + CWarnings.create ~name:"ambiguous-file-name" ~category:"filesystem" + (fun (filename,l,f) -> str filename ++ str " has been found in" ++ spc () ++ + hov 0 (str "[ " ++ + hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon()) + (fun (lpe,_) -> str lpe) l) + ++ str " ];") ++ fnl () ++ + str "loading " ++ str f) + + let where_in_path ?(warn=true) path filename = let check_and_warn l = match l with | [] -> raise Not_found | (lpe, f) :: l' -> let () = match l' with - | _ :: _ when warn -> - Feedback.msg_warning - (str filename ++ str " has been found in" ++ spc () ++ - hov 0 (str "[ " ++ - hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon()) - (fun (lpe,_) -> str lpe) l) - ++ str " ];") ++ fnl () ++ - str "loading " ++ str f) + | _ :: _ when warn -> warn_ambiguous_file_name (filename,l,f) | _ -> () in (lpe, f) @@ -142,12 +149,16 @@ let is_in_path lpath filename = try ignore (where_in_path ~warn:false lpath filename); true with Not_found -> false +let warn_path_not_found = + CWarnings.create ~name:"path-not-found" ~category:"filesystem" + (fun () -> str "system variable PATH not found") + let is_in_system_path filename = try let lpath = CUnix.path_to_list (Sys.getenv "PATH") in is_in_path lpath filename with Not_found -> - Feedback.msg_warning (str "system variable PATH not found"); + warn_path_not_found (); false let open_trapping_failure name = @@ -155,11 +166,14 @@ let open_trapping_failure name = with e when Errors.noncritical e -> errorlabstrm "System.open" (str "Can't open " ++ str name) +let warn_cannot_remove_file = + CWarnings.create ~name:"cannot-remove-file" ~category:"filesystem" + (fun filename -> str"Could not remove file " ++ str filename ++ str" which is corrupted!") + let try_remove filename = try Sys.remove filename with e when Errors.noncritical e -> - Feedback.msg_warning - (str"Could not remove file " ++ str filename ++ str" which is corrupted!") + warn_cannot_remove_file filename let error_corrupted file s = errorlabstrm "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.") diff --git a/library/goptions.ml b/library/goptions.ml index 4aa3a2a21..7bead0b63 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -233,6 +233,11 @@ with Not_found -> open Libobject open Lib +let warn_deprecated_option = + CWarnings.create ~name:"deprecated-option" ~category:"deprecated" + (fun key -> str "Option" ++ spc () ++ str (nickname key) ++ + strbrk " is deprecated") + let declare_option cast uncast { optsync=sync; optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } = check_key key; @@ -270,10 +275,7 @@ let declare_option cast uncast begin fun v -> add_anonymous_leaf (gdecl_obj v) end else write,write,write in - let warn () = - if depr then - Feedback.msg_warning (str "Option " ++ str (nickname key) ++ str " is deprecated") - in + let warn () = if depr then warn_deprecated_option key in let cread () = cast (read ()) in let cwrite v = warn (); write (uncast v) in let clwrite v = warn (); lwrite (uncast v) in @@ -304,19 +306,22 @@ let declare_stringopt_option = (* Setting values of options *) +let warn_unknown_option = + CWarnings.create ~name:"unknown-option" ~category:"option" + (fun key -> strbrk "There is no option " ++ + str (nickname key) ++ str ".") + let set_option_value locality check_and_cast key v = - let (name, depr, (_,read,write,lwrite,gwrite)) = - try get_option key - with Not_found -> - errorlabstrm "Goptions.set_option_value" - (str "There is no option " ++ str (nickname key) ++ str ".") - in - let write = match locality with - | None -> write - | Some true -> lwrite - | Some false -> gwrite - in - write (check_and_cast v (read ())) + let opt = try Some (get_option key) with Not_found -> None in + match opt with + | None -> warn_unknown_option key + | Some (name, depr, (_,read,write,lwrite,gwrite)) -> + let write = match locality with + | None -> write + | Some true -> lwrite + | Some false -> gwrite + in + write (check_and_cast v (read ())) let bad_type_error () = error "Bad type of value for this option." @@ -346,13 +351,11 @@ let check_unset_value v = function let set_int_option_value_gen locality = set_option_value locality check_int_value let set_bool_option_value_gen locality key v = - try set_option_value locality check_bool_value key v - with UserError (_,s) -> Feedback.msg_warning s + set_option_value locality check_bool_value key v let set_string_option_value_gen locality = set_option_value locality check_string_value let unset_option_value_gen locality key = - try set_option_value locality check_unset_value key () - with UserError (_,s) -> Feedback.msg_warning s + set_option_value locality check_unset_value key () let set_int_option_value = set_int_option_value_gen None let set_bool_option_value = set_bool_option_value_gen None diff --git a/library/libobject.ml b/library/libobject.ml index b12d2038a..3e08b38b1 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -12,18 +12,6 @@ open Util module Dyn = Dyn.Make(struct end) -(* The relax flag is used to make it possible to load files while ignoring - failures to incorporate some objects. This can be useful when one - wants to work with restricted Coq programs that have only parts of - the full capabilities, but may still be able to work correctly for - limited purposes. One example is for the graphical interface, that uses - such a limited Coq process to do only parsing. It loads .vo files, but - is only interested in loading the grammar rule definitions. *) - -let relax_flag = ref false;; - -let relax b = relax_flag := b;; - type 'a substitutivity = Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a @@ -114,31 +102,16 @@ let declare_object_full odecl = try declare_object_full odecl with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e) -let missing_tab = (Hashtbl.create 17 : (string, unit) Hashtbl.t) - (* this function describes how the cache, load, open, and export functions - are triggered. In relaxed mode, this function just return a meaningless - value instead of raising an exception when they fail. *) + are triggered. *) let apply_dyn_fun deflt f lobj = let tag = object_tag lobj in - try - let dodecl = - try - Hashtbl.find cache_tab tag - with Not_found -> - failwith "local to_apply_dyn_fun" in - f dodecl - with - Failure "local to_apply_dyn_fun" -> - if not (!relax_flag || Hashtbl.mem missing_tab tag) then - begin - Feedback.msg_warning - (Pp.str ("Cannot find library functions for an object with tag " - ^ tag ^ " (a plugin may be missing)")); - Hashtbl.add missing_tab tag () - end; - deflt + let dodecl = + try Hashtbl.find cache_tab tag + with Not_found -> assert false + in + f dodecl let cache_object ((_,lobj) as node) = apply_dyn_fun () (fun d -> d.dyn_cache_function node) lobj diff --git a/library/libobject.mli b/library/libobject.mli index dbe0de8f8..51b9af059 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -107,7 +107,6 @@ val subst_object : substitution * obj -> obj val classify_object : obj -> obj substitutivity val discharge_object : object_name * obj -> obj option val rebuild_object : obj -> obj -val relax : bool -> unit (** {6 Debug} *) diff --git a/library/library.ml b/library/library.ml index bc7723f48..cead90700 100644 --- a/library/library.ml +++ b/library/library.ml @@ -271,6 +271,12 @@ exception LibUnmappedDir exception LibNotFound type library_location = LibLoaded | LibInPath +let warn_several_object_files = + CWarnings.create ~name:"several-object-files" ~category:"require" + (fun (vi, vo) -> str"Loading" ++ spc () ++ str vi ++ + strbrk " instead of " ++ str vo ++ + strbrk " because it is more recent") + let locate_absolute_library dir = (* Search in loadpath *) let pref, base = split_dirpath dir in @@ -287,9 +293,8 @@ let locate_absolute_library dir = | [] -> raise LibNotFound | [file] -> file | [vo;vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - Feedback.msg_warning (str"Loading " ++ str vi ++ str " instead of " ++ - str vo ++ str " because it is more recent"); - vi + warn_several_object_files (vi, vo); + vi | [vo;vi] -> vo | _ -> assert false @@ -311,8 +316,7 @@ let locate_qualified_library ?root ?(warn = true) qid = | [lpath, file] -> lpath, file | [lpath_vo, vo; lpath_vi, vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - Feedback.msg_warning (str"Loading " ++ str vi ++ str " instead of " ++ - str vo ++ str " because it is more recent"); + warn_several_object_files (vi, vo); lpath_vi, vi | [lpath_vo, vo; _ ] -> lpath_vo, vo | _ -> assert false @@ -753,7 +757,7 @@ let save_library_to ?todo dir f otab = error "Could not compile the library to native code." with reraise -> let reraise = Errors.push reraise in - let () = Feedback.msg_warning (str "Removed file " ++ str f') in + let () = Feedback.msg_notice (str "Removed file " ++ str f') in let () = close_out ch in let () = Sys.remove f' in iraise reraise diff --git a/library/loadpath.ml b/library/loadpath.ml index 33c0f41e1..6f4d79430 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -50,6 +50,13 @@ let remove_load_path dir = let filter p = not (String.equal p.path_physical dir) in load_paths := List.filter filter !load_paths +let warn_overriding_logical_loadpath = + CWarnings.create ~name:"overriding-logical-loadpath" ~category:"loadpath" + (fun (phys_path, old_path, coq_path) -> + str phys_path ++ strbrk " was previously bound to " ++ + pr_dirpath old_path ++ strbrk "; it is remapped to " ++ + pr_dirpath coq_path) + let add_load_path phys_path coq_path ~implicit = let phys_path = CUnix.canonical_path_name phys_path in let filter p = String.equal p.path_physical phys_path in @@ -72,10 +79,8 @@ let add_load_path phys_path coq_path ~implicit = let () = (* Do not warn when overriding the default "-I ." path *) if not (DirPath.equal old_path Nameops.default_root_prefix) then - Feedback.msg_warning - (str phys_path ++ strbrk " was previously bound to " ++ - pr_dirpath old_path ++ strbrk "; it is remapped to " ++ - pr_dirpath coq_path) in + warn_overriding_logical_loadpath (phys_path, old_path, coq_path) + in true in if replace then begin diff --git a/library/nametab.ml b/library/nametab.ml index db902d625..f533bc791 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -82,6 +82,14 @@ module Make (U : UserName) (E : EqualityType) : NAMETREE struct type elt = E.t + (* A name became inaccessible, even with absolute qualification. + Example: + Module F (X : S). Module X. + The argument X of the functor F is masked by the inner module X. + *) + let masking_absolute n = + Flags.if_verbose Feedback.msg_info (str ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!")) + type user_name = U.t type path_status = @@ -119,9 +127,7 @@ struct | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - Feedback.msg_warning (str ("Trying to mask the absolute name \"" - ^ U.to_string n ^ "\"!")); - tree.path + masking_absolute n; tree.path | Nothing | Relative _ -> Relative (uname,o) else tree.path @@ -144,7 +150,6 @@ struct | Nothing | Relative _ -> mktree (Absolute (uname,o)) tree.map - let rec push_exactly uname o level tree = function | [] -> anomaly (Pp.str "Prefix longer than path! Impossible!") @@ -155,9 +160,7 @@ let rec push_exactly uname o level tree = function | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - Feedback.msg_warning (str ("Trying to mask the absolute name \"" - ^ U.to_string n ^ "\"!")); - tree.path + masking_absolute n; tree.path | Nothing | Relative _ -> Relative (uname,o) in diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index 517f9e3af..b5494a7cb 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -72,6 +72,11 @@ let test_bracket_ident = (* Tactics grammar rules *) +let warn_deprecated_appcontext = + CWarnings.create ~name:"deprecated-appcontext" ~category:"deprecated" + (fun () -> strbrk "appcontext is deprecated and will be removed " ++ + strbrk "in a future version") + GEXTEND Gram GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg tactic_mode constr_may_eval constr_eval selector toplevel_selector; @@ -232,7 +237,7 @@ GEXTEND Gram Subterm (mode, oid, pc) | IDENT "appcontext"; oid = OPT Constr.ident; "["; pc = Constr.lconstr_pattern; "]" -> - Feedback.msg_warning (strbrk "appcontext is deprecated"); + warn_deprecated_appcontext ~loc:!@loc (); Subterm (true,oid, pc) | pc = Constr.lconstr_pattern -> Term pc ] ] ; diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index 9081fd3e9..f332e1a0d 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -32,10 +32,14 @@ let is_new_call () = let b = !new_call in new_call := false; b profiling results will be off. *) let encountered_multi_success_backtracking = ref false +let warn_profile_backtracking = + CWarnings.create ~name:"profile-backtracking" ~category:"ltac" + (fun () -> strbrk "Ltac Profiler cannot yet handle backtracking \ + into multi-success tactics; profiling results may be wildly inaccurate.") + let warn_encountered_multi_success_backtracking () = if !encountered_multi_success_backtracking then - Feedback.msg_warning (str "Ltac Profiler cannot yet handle backtracking \ - into multi-success tactics; profiling results may be wildly inaccurate.") + warn_profile_backtracking () let encounter_multi_success_backtracking () = if not !encountered_multi_success_backtracking diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index f00adecf2..6b7ae21f3 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -417,6 +417,11 @@ type tacdef_kind = let is_defined_tac kn = try ignore (Tacenv.interp_ltac kn); true with Not_found -> false +let warn_unusable_identifier = + CWarnings.create ~name:"unusable-identifier" ~category:"parsing" + (fun id -> strbrk "The Ltac name" ++ spc () ++ pr_id id ++ spc () ++ + strbrk "may be unusable because of a conflict with a notation.") + let register_ltac local tacl = let map tactic_body = match tactic_body with @@ -427,17 +432,14 @@ let register_ltac local tacl = Errors.user_err_loc (loc, "", str "There is already an Ltac named " ++ id_pp ++ str".") in - let is_primitive = + let is_shadowed = try match Pcoq.parse_string Pcoq.Tactic.tactic (Id.to_string id) with | Tacexpr.TacArg _ -> false | _ -> true (* most probably TacAtom, i.e. a primitive tactic ident *) with e when Errors.noncritical e -> true (* prim tactics with args, e.g. "apply" *) in - let () = if is_primitive then - Feedback.msg_warning (str "The Ltac name " ++ id_pp ++ - str " may be unusable because of a conflict with a notation.") - in + let () = if is_shadowed then warn_unusable_identifier id in NewTac id, body | TacticRedefinition (ident, body) -> let loc = loc_of_reference ident in diff --git a/ltac/tacenv.ml b/ltac/tacenv.ml index 005d1f5f4..e3d5e18c9 100644 --- a/ltac/tacenv.ml +++ b/ltac/tacenv.ml @@ -53,8 +53,7 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic array) = let () = if MLTacMap.mem s !tac_tab then if overwrite then - let () = tac_tab := MLTacMap.remove s !tac_tab in - Feedback.msg_warning (str "Overwriting definition of tactic " ++ pr_tacname s) + tac_tab := MLTacMap.remove s !tac_tab else Errors.anomaly (str "Cannot redeclare tactic " ++ pr_tacname s ++ str ".") in diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index e814cc7e6..9a4beed87 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1144,6 +1144,12 @@ let rec read_match_rule lfun ist env sigma = function :: read_match_rule lfun ist env sigma tl | [] -> [] +let warn_deprecated_info = + CWarnings.create ~name:"deprecated-info-tactical" ~category:"deprecated" + (fun () -> + strbrk "The general \"info\" tactic is currently not working." ++ spc()++ + strbrk "There is an \"Info\" command to replace it." ++fnl () ++ + strbrk "Some specific verbose tactics may also exist, such as info_eauto.") (* Interprets an l-tac expression into a value *) let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftactic.t = @@ -1251,10 +1257,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac) | TacArg a -> interp_tactic ist (TacArg a) | TacInfo tac -> - Feedback.msg_warning - (strbrk "The general \"info\" tactic is currently not working." ++ spc()++ - strbrk "There is an \"Info\" command to replace it." ++fnl () ++ - strbrk "Some specific verbose tactics may also exist, such as info_eauto."); + warn_deprecated_info (); eval_tactic ist tac | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac) (* For extensions *) diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index b04c7633a..711d2240b 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -206,12 +206,16 @@ let check_keyword str = in loop_symb (Stream.of_string str) +let warn_unparsable_keyword = + CWarnings.create ~name:"unparsable-keyword" ~category:"parsing" + (fun (s,unicode) -> + strbrk (Printf.sprintf "Token '%s' contains unicode character 0x%x \ + which will not be parsable." s unicode)) + let check_keyword_to_add s = try check_keyword s with Error.E (UnsupportedUnicode unicode) -> - Flags.if_verbose Feedback.msg_warning - (strbrk (Printf.sprintf "Token '%s' contains unicode character 0x%x \ - which will not be parsable." s unicode)) + warn_unparsable_keyword (s,unicode) let check_ident str = let rec loop_id intail = parser @@ -316,6 +320,14 @@ let rec number_or_index loc bp l len = parser | ['t';'h'] when check_no_char s -> njunk 2 s; check_gt3 loc l len | _ -> true, len +let warn_comment_terminator_in_string = + CWarnings.create ~name:"comment-terminator-in-string" ~category:"parsing" + (fun () -> + (strbrk + "Not interpreting \"*)\" as the end of current \ + non-terminated comment because it occurs in a \ + non-terminated string of the comment.")) + (* If the string being lexed is in a comment, [comm_level] is Some i with i the current level of comments nesting. Otherwise, [comm_level] is None. *) let rec string loc ~comm_level bp len = parser @@ -335,11 +347,7 @@ let rec string loc ~comm_level bp len = parser | [< '')'; s >] -> let () = match comm_level with | Some 0 -> - Feedback.msg_warning - (strbrk - "Not interpreting \"*)\" as the end of current \ - non-terminated comment because it occurs in a \ - non-terminated string of the comment.") + warn_comment_terminator_in_string ~loc:!@loc () | _ -> () in let comm_level = Option.map pred comm_level in diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index d0bca9ee3..8a83bc2d1 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -211,6 +211,10 @@ let merge_occurrences loc cl = function in (Some p, ans) +let warn_deprecated_eqn_syntax = + CWarnings.create ~name:"deprecated-eqn-syntax" ~category:"deprecated" + (fun arg -> strbrk (Printf.sprintf "Syntax \"_eqn:%s\" is deprecated. Please use \"eqn:%s\" instead." arg arg)) + (* Auxiliary grammar rules *) GEXTEND Gram @@ -469,11 +473,11 @@ GEXTEND Gram eqn_ipat: [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (!@loc, pat) | IDENT "_eqn"; ":"; pat = naming_intropattern -> - let msg = "Obsolete syntax \"_eqn:H\" could be replaced by \"eqn:H\"" in - Feedback.msg_warning (strbrk msg); Some (!@loc, pat) + let loc = !@loc in + warn_deprecated_eqn_syntax ~loc "H"; Some (loc, pat) | IDENT "_eqn" -> - let msg = "Obsolete syntax \"_eqn\" could be replaced by \"eqn:?\"" in - Feedback.msg_warning (strbrk msg); Some (!@loc, IntroAnonymous) + let loc = !@loc in + warn_deprecated_eqn_syntax ~loc "?"; Some (loc, IntroAnonymous) | -> None ] ] ; as_name: diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index f0475ee25..7184136e8 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -123,16 +123,18 @@ GEXTEND Gram ; END -let test_plural_form = function +let warn_plural_command = + CWarnings.create ~name:"plural-command" ~category:"pedantic" ~default:CWarnings.Disabled + (fun kwd -> strbrk (Printf.sprintf "Command \"%s\" expects more than one assumption." kwd)) + +let test_plural_form loc kwd = function | [(_,([_],_))] -> - Flags.if_verbose Feedback.msg_warning - (strbrk "Keywords Variables/Hypotheses/Parameters expect more than one assumption") + warn_plural_command ~loc:!@loc kwd | _ -> () -let test_plural_form_types = function +let test_plural_form_types loc kwd = function | [([_],_)] -> - Flags.if_verbose Feedback.msg_warning - (strbrk "Keywords Implicit Types expect more than one type") + warn_plural_command ~loc:!@loc kwd | _ -> () let fresh_var env c = @@ -155,8 +157,8 @@ GEXTEND Gram VernacStartTheoremProof (thm, (Some id,(bl,c,None))::l, false) | stre = assumption_token; nl = inline; bl = assum_list -> VernacAssumption (stre, nl, bl) - | stre = assumptions_token; nl = inline; bl = assum_list -> - test_plural_form bl; + | (kwd,stre) = assumptions_token; nl = inline; bl = assum_list -> + test_plural_form loc kwd bl; VernacAssumption (stre, nl, bl) | d = def_token; id = pidentref; b = def_body -> VernacDefinition (d, id, b) @@ -209,11 +211,11 @@ GEXTEND Gram | IDENT "Conjecture" -> (None, Conjectural) ] ] ; assumptions_token: - [ [ IDENT "Hypotheses" -> (Some Discharge, Logical) - | IDENT "Variables" -> (Some Discharge, Definitional) - | IDENT "Axioms" -> (None, Logical) - | IDENT "Parameters" -> (None, Definitional) - | IDENT "Conjectures" -> (None, Conjectural) ] ] + [ [ kwd = IDENT "Hypotheses" -> (kwd, (Some Discharge, Logical)) + | kwd = IDENT "Variables" -> (kwd, (Some Discharge, Definitional)) + | kwd = IDENT "Axioms" -> (kwd, (None, Logical)) + | kwd = IDENT "Parameters" -> (kwd, (None, Definitional)) + | kwd = IDENT "Conjectures" -> (kwd, (None, Conjectural)) ] ] ; inline: [ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i) @@ -422,6 +424,10 @@ let starredidentreflist_to_expr l = | [] -> SsEmpty | x :: xs -> List.fold_right (fun i acc -> SsUnion(i,acc)) xs x +let warn_deprecated_include_type = + CWarnings.create ~name:"deprecated-include-type" ~category:"deprecated" + (fun () -> strbrk "Include Type is deprecated; use Include instead") + (* Modules and Sections *) GEXTEND Gram GLOBAL: gallina_ext module_expr module_type section_subset_expr; @@ -461,9 +467,8 @@ GEXTEND Gram | IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_expr -> VernacInclude(e::l) | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type -> - Flags.if_verbose - Feedback.msg_warning (strbrk "Include Type is deprecated; use Include instead"); - VernacInclude(e::l) ] ] + warn_deprecated_include_type ~loc:!@loc (); + VernacInclude(e::l) ] ] ; export_token: [ [ IDENT "Import" -> Some false @@ -567,6 +572,14 @@ GEXTEND Gram ; END +let warn_deprecated_arguments_scope = + CWarnings.create ~name:"deprecated-arguments-scope" ~category:"deprecated" + (fun () -> strbrk "Arguments Scope is deprecated; use Arguments instead") + +let warn_deprecated_implicit_arguments = + CWarnings.create ~name:"deprecated-implicit-arguments" ~category:"deprecated" + (fun () -> strbrk "Implicit Arguments is deprecated; use Arguments instead") + (* Extensions: implicits, coercions, etc. *) GEXTEND Gram GLOBAL: gallina_ext instance_name; @@ -681,22 +694,21 @@ GEXTEND Gram (* moved there so that camlp5 factors it with the previous rule *) | IDENT "Arguments"; IDENT "Scope"; qid = smart_global; "["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" -> - Feedback. msg_warning (strbrk "Arguments Scope is deprecated; use Arguments instead"); + warn_deprecated_arguments_scope ~loc:!@loc (); VernacArgumentsScope (qid,scl) (* Implicit *) | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global; pos = LIST0 [ "["; l = LIST0 implicit_name; "]" -> List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] -> - Flags.if_verbose - Feedback.msg_warning (strbrk "Implicit Arguments is deprecated; use Arguments instead"); - VernacDeclareImplicits (qid,pos) + warn_deprecated_implicit_arguments ~loc:!@loc (); + VernacDeclareImplicits (qid,pos) | IDENT "Implicit"; "Type"; bl = reserv_list -> VernacReserve bl | IDENT "Implicit"; IDENT "Types"; bl = reserv_list -> - test_plural_form_types bl; + test_plural_form_types loc "Implicit Types" bl; VernacReserve bl | IDENT "Generalizable"; diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 3fa600ac2..836f1982d 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -283,6 +283,10 @@ let register_automation_tac tac = my_automation_tac:= tac let automation_tac = Proofview.tclBIND (Proofview.tclUNIT ()) (fun () -> !my_automation_tac) +let warn_insufficient_justification = + CWarnings.create ~name:"declmode-insufficient-justification" ~category:"declmode" + (fun () -> strbrk "Insufficient justification.") + let justification tac gls= tclORELSE (tclSOLVE [tclTHEN tac (Proofview.V82.of_tactic assumption)]) @@ -291,7 +295,7 @@ let justification tac gls= error "Insufficient justification." else begin - Feedback.msg_warning (str "Insufficient justification."); + warn_insufficient_justification (); daimon_tac gls end) gls @@ -1219,6 +1223,9 @@ let hrec_for fix_id per_info gls obj_id = let hd2 = applist (mkVar fix_id,args@[obj]) in compose_lam rc (Reductionops.whd_beta gls.sigma hd2) +let warn_missing_case = + CWarnings.create ~name:"declmode-missing-case" ~category:"declmode" + (fun () -> strbrk "missing case") let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = match tree, objs with @@ -1293,8 +1300,8 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = end; match bro with None -> - Feedback.msg_warning (str "missing case"); - tacnext (mkMeta 1) + warn_missing_case (); + tacnext (mkMeta 1) | Some (sub_ids,tree) -> let br_args = List.filter diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index a03be5743..94981d0e1 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -583,8 +583,8 @@ let rec locate_ref = function | None, Some r -> let refs,mps = locate_ref l in r::refs,mps | Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps | Some mp, Some r -> - warning_both_mod_and_cst q mp r; - let refs,mps = locate_ref l in refs,mp::mps + warning_ambiguous_name (q,mp,r); + let refs,mps = locate_ref l in refs,mp::mps (*s Recursive extraction in the Coq toplevel. The vernacular command is \verb!Recursive Extraction! [qualid1] ... [qualidn]. Also used when diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 560fe5aea..81dfa603d 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -295,81 +295,94 @@ let pr_long_global ref = pr_path (Nametab.path_of_global ref) let err s = errorlabstrm "Extraction" s +let warn_extraction_axiom_to_realize = + CWarnings.create ~name:"extraction-axiom-to-realize" ~category:"extraction" + (fun axioms -> + let s = if Int.equal (List.length axioms) 1 then "axiom" else "axioms" in + strbrk ("The following "^s^" must be realized in the extracted code:") + ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global axioms) + ++ str "." ++ fnl ()) + +let warn_extraction_logical_axiom = + CWarnings.create ~name:"extraction-logical-axiom" ~category:"extraction" + (fun axioms -> + let s = + if Int.equal (List.length axioms) 1 then "axiom was" else "axioms were" + in + (strbrk ("The following logical "^s^" encountered:") ++ + hov 1 (spc () ++ prlist_with_sep spc safe_pr_global axioms ++ str ".\n") + ++ strbrk "Having invalid logical axiom in the environment when extracting" + ++ spc () ++ strbrk "may lead to incorrect or non-terminating ML terms." ++ + fnl ())) + let warning_axioms () = let info_axioms = Refset'.elements !info_axioms in - if List.is_empty info_axioms then () - else begin - let s = if Int.equal (List.length info_axioms) 1 then "axiom" else "axioms" in - Feedback.msg_warning - (str ("The following "^s^" must be realized in the extracted code:") - ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms) - ++ str "." ++ fnl ()) - end; + if not (List.is_empty info_axioms) then + warn_extraction_axiom_to_realize info_axioms; let log_axioms = Refset'.elements !log_axioms in - if List.is_empty log_axioms then () - else begin - let s = if Int.equal (List.length log_axioms) 1 then "axiom was" else "axioms were" - in - Feedback.msg_warning - (str ("The following logical "^s^" encountered:") ++ - hov 1 - (spc () ++ prlist_with_sep spc safe_pr_global log_axioms ++ str ".\n") - ++ - str "Having invalid logical axiom in the environment when extracting" ++ - spc () ++ str "may lead to incorrect or non-terminating ML terms." ++ - fnl ()) - end + if not (List.is_empty log_axioms) then + warn_extraction_logical_axiom log_axioms + +let warn_extraction_opaque_accessed = + CWarnings.create ~name:"extraction-opaque-accessed" ~category:"extraction" + (fun lst -> strbrk "The extraction is currently set to bypass opacity, " ++ + strbrk "the following opaque constant bodies have been accessed :" ++ + lst ++ str "." ++ fnl ()) + +let warn_extraction_opaque_as_axiom = + CWarnings.create ~name:"extraction-opaque-as-axiom" ~category:"extraction" + (fun lst -> strbrk "The extraction now honors the opacity constraints by default, " ++ + strbrk "the following opaque constants have been extracted as axioms :" ++ + lst ++ str "." ++ fnl () ++ + strbrk "If necessary, use \"Set Extraction AccessOpaque\" to change this." + ++ fnl ()) let warning_opaques accessed = let opaques = Refset'.elements !opaques in - if List.is_empty opaques then () - else + if not (List.is_empty opaques) then let lst = hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques) in - if accessed then - Feedback.msg_warning - (str "The extraction is currently set to bypass opacity,\n" ++ - str "the following opaque constant bodies have been accessed :" ++ - lst ++ str "." ++ fnl ()) - else - Feedback.msg_warning - (str "The extraction now honors the opacity constraints by default,\n" ++ - str "the following opaque constants have been extracted as axioms :" ++ - lst ++ str "." ++ fnl () ++ - str "If necessary, use \"Set Extraction AccessOpaque\" to change this." - ++ fnl ()) - -let warning_both_mod_and_cst q mp r = - Feedback.msg_warning - (str "The name " ++ pr_qualid q ++ str " is ambiguous, " ++ - str "do you mean module " ++ - pr_long_mp mp ++ - str " or object " ++ - pr_long_global r ++ str " ?" ++ fnl () ++ - str "First choice is assumed, for the second one please use " ++ - str "fully qualified name." ++ fnl ()) + if accessed then warn_extraction_opaque_accessed lst + else warn_extraction_opaque_as_axiom lst + +let warning_ambiguous_name = + CWarnings.create ~name:"extraction-ambiguous-name" ~category:"extraction" + (fun (q,mp,r) -> strbrk "The name " ++ pr_qualid q ++ strbrk " is ambiguous, " ++ + strbrk "do you mean module " ++ + pr_long_mp mp ++ + strbrk " or object " ++ + pr_long_global r ++ str " ?" ++ fnl () ++ + strbrk "First choice is assumed, for the second one please use " ++ + strbrk "fully qualified name." ++ fnl ()) let error_axiom_scheme r i = err (str "The type scheme axiom " ++ spc () ++ safe_pr_global r ++ spc () ++ str "needs " ++ int i ++ str " type variable(s).") +let warn_extraction_inside_module = + CWarnings.create ~name:"extraction-inside-module" ~category:"extraction" + (fun () -> strbrk "Extraction inside an opened module is experimental." ++ + strbrk "In case of problem, close it first.") + + let check_inside_module () = if Lib.is_modtype () then err (str "You can't do that within a Module Type." ++ fnl () ++ str "Close it and try again.") else if Lib.is_module () then - Feedback.msg_warning - (str "Extraction inside an opened module is experimental.\n" ++ - str "In case of problem, close it first.\n") + warn_extraction_inside_module () let check_inside_section () = if Lib.sections_are_opened () then err (str "You can't do that within a section." ++ fnl () ++ str "Close it and try again.") -let warning_id s = - Feedback.msg_warning (str ("The identifier "^s^ - " contains __ which is reserved for the extraction")) +let warn_extraction_reserved_identifier = + CWarnings.create ~name:"extraction-reserved-identifier" ~category:"extraction" + (fun s -> strbrk ("The identifier "^s^ + " contains __ which is reserved for the extraction")) + +let warning_id s = warn_extraction_reserved_identifier s let error_constant r = err (safe_pr_global r ++ str " is not a constant.") @@ -447,12 +460,15 @@ let error_remaining_implicit k = str "You might also try Unset Extraction SafeImplicits to force" ++ fnl() ++ str "the extraction of unsafe code and review it manually.") +let warn_extraction_remaining_implicit = + CWarnings.create ~name:"extraction-remaining-implicit" ~category:"extraction" + (fun s -> strbrk ("At least an implicit occurs after extraction : "^s^".") ++ fnl () ++ + strbrk "Extraction SafeImplicits is unset, extracting nonetheless," + ++ strbrk "but this code is potentially unsafe, please review it manually.") + let warning_remaining_implicit k = let s = msg_of_implicit k in - Feedback.msg_warning - (str ("At least an implicit occurs after extraction : "^s^".") ++ fnl () ++ - str "Extraction SafeImplicits is unset, extracting nonetheless," ++ fnl () - ++ str "but this code is potentially unsafe, please review it manually.") + warn_extraction_remaining_implicit s let check_loaded_modfile mp = match base_mp mp with | MPfile dp -> diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 62c20bd3a..15a08756c 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -21,8 +21,7 @@ val safe_basename_of_global : global_reference -> Id.t val warning_axioms : unit -> unit val warning_opaques : bool -> unit -val warning_both_mod_and_cst : - qualid -> module_path -> global_reference -> unit +val warning_ambiguous_name : ?loc:Loc.t -> qualid * module_path * global_reference -> unit val warning_id : string -> unit val error_axiom_scheme : global_reference -> int -> 'a val error_constant : global_reference -> 'a diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index cec3505a9..95095b09c 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -120,6 +120,11 @@ let pr_firstorder_using_raw _ _ _ l = str "using " ++ prlist_with_sep pr_comma p let pr_firstorder_using_glob _ _ _ l = str "using " ++ prlist_with_sep pr_comma (pr_or_var (fun x -> (pr_global (snd x)))) l let pr_firstorder_using_typed _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_global l +let warn_deprecated_syntax = + CWarnings.create ~name:"firstorder-deprecated-syntax" ~category:"deprecated" + (fun () -> Pp.strbrk "Deprecated syntax; use \",\" as separator") + + ARGUMENT EXTEND firstorder_using TYPED AS reference_list PRINTED BY pr_firstorder_using_typed @@ -130,8 +135,7 @@ ARGUMENT EXTEND firstorder_using | [ "using" reference(a) ] -> [ [a] ] | [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> [ a::l ] | [ "using" reference(a) reference(b) reference_list(l) ] -> [ - Flags.if_verbose - Feedback.msg_warning (Pp.str "Deprecated syntax; use \",\" as separator"); + warn_deprecated_syntax (); a::b::l ] | [ ] -> [ [] ] diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 893baad8c..93a89330e 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -198,15 +198,13 @@ let warning_error names e = let (e, _) = Cerrors.process_vernac_interp_error (e, Exninfo.null) in match e with | Building_graph e -> - Feedback.msg_warning - (str "Cannot define graph(s) for " ++ - h 1 (pr_enum Libnames.pr_reference names) ++ - if do_observe () then (spc () ++ Errors.print e) else mt ()) + let names = pr_enum Libnames.pr_reference names in + let error = if do_observe () then (spc () ++ Errors.print e) else mt () in + warn_cannot_define_graph (names,error) | Defining_principle e -> - Feedback.msg_warning - (str "Cannot define principle(s) for "++ - h 1 (pr_enum Libnames.pr_reference names) ++ - if do_observe () then Errors.print e else mt ()) + let names = pr_enum Libnames.pr_reference names in + let error = if do_observe () then Errors.print e else mt () in + warn_cannot_define_principle (names,error) | _ -> raise e diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 1c5eb1621..2ebbb34e4 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -227,6 +227,11 @@ let prepare_body ((name,_,args,types,_),_) rt = let process_vernac_interp_error e = fst (Cerrors.process_vernac_interp_error (e, Exninfo.null)) +let warn_funind_cannot_build_inversion = + CWarnings.create ~name:"funind-cannot-build-inversion" ~category:"funind" + (fun e' -> strbrk "Cannot build inversion information" ++ + if do_observe () then (fnl() ++ Errors.print e') else mt ()) + let derive_inversion fix_names = try let evd' = Evd.from_env (Global.env ()) in @@ -269,14 +274,20 @@ let derive_inversion fix_names = lind; with e when Errors.noncritical e -> let e' = process_vernac_interp_error e in - Feedback.msg_warning - (str "Cannot build inversion information" ++ - if do_observe () then (fnl() ++ Errors.print e') else mt ()) + warn_funind_cannot_build_inversion e' with e when Errors.noncritical e -> - let e' = process_vernac_interp_error e in - Feedback.msg_warning - (str "Cannot build inversion information (early)" ++ - if do_observe () then (fnl() ++ Errors.print e') else mt ()) + let e' = process_vernac_interp_error e in + warn_funind_cannot_build_inversion e' + +let warn_cannot_define_graph = + CWarnings.create ~name:"funind-cannot-define-graph" ~category:"funind" + (fun (names,error) -> strbrk "Cannot define graph(s) for " ++ + h 1 names ++ error) + +let warn_cannot_define_principle = + CWarnings.create ~name:"funind-cannot-define-principle" ~category:"funind" + (fun (names,error) -> strbrk "Cannot define induction principle(s) for "++ + h 1 names ++ error) let warning_error names e = let e = process_vernac_interp_error e in @@ -294,15 +305,11 @@ let warning_error names e = in match e with | Building_graph e -> - Feedback.msg_warning - (str "Cannot define graph(s) for " ++ - h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ - e_explain e) + let names = prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names in + warn_cannot_define_graph (names,e_explain e) | Defining_principle e -> - Feedback.msg_warning - (str "Cannot define principle(s) for "++ - h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ - e_explain e) + let names = prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names in + warn_cannot_define_principle (names,e_explain e) | _ -> raise e let error_error names e = diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index e72069140..1c27bdfac 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -1,5 +1,9 @@ open Misctypes +val warn_cannot_define_graph : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit + +val warn_cannot_define_principle : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit + val do_generate_principle : bool -> (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index 3142c8cf0..89305838b 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -26,14 +26,16 @@ open Errors let threshold = of_int 5000 +let warn_large_nat = + CWarnings.create ~name:"large-nat" ~category:"numbers" + (fun () -> strbrk "Stack overflow or segmentation fault happens when " ++ + strbrk "working with large numbers in nat (observed threshold " ++ + strbrk "may vary from 5000 to 70000 depending on your system " ++ + strbrk "limits and on the command executed).") + let nat_of_int dloc n = if is_pos_or_zero n then begin - if less_than threshold n then - Feedback.msg_warning - (strbrk "Stack overflow or segmentation fault happens when " ++ - strbrk "working with large numbers in nat (observed threshold " ++ - strbrk "may vary from 5000 to 70000 depending on your system " ++ - strbrk "limits and on the command executed)."); + if less_than threshold n then warn_large_nat (); let ref_O = GRef (dloc, glob_O, None) in let ref_S = GRef (dloc, glob_S, None) in let rec mk_nat acc n = diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 55220f44c..d3d4201f5 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -387,7 +387,7 @@ let add_coercion_in_graph (ic,source,target) = end; let is_ambig = match !ambig_paths with [] -> false | _ -> true in if is_ambig && is_verbose () then - Feedback.msg_warning (message_ambig !ambig_paths) + Feedback.msg_info (message_ambig !ambig_paths) type coercion = { coercion_type : coe_typ; diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 129725c6d..c566839e8 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -49,12 +49,12 @@ type bound_ident_map = Id.t Id.Map.t exception PatternMatchingFailure -let warn_bound_meta name = - Feedback.msg_warning (str "Collision between bound variable " ++ pr_id name ++ - str " and a metavariable of same name.") +let warn_meta_collision = + CWarnings.create ~name:"meta-collision" ~category:"ltac" + (fun name -> + strbrk "Collision between bound variable " ++ pr_id name ++ + strbrk " and a metavariable of same name.") -let warn_bound_bound name = - Feedback.msg_warning (str "Collision between bound variables of name " ++ pr_id name) let constrain n (ids, m as x) (names, terms as subst) = try @@ -62,18 +62,19 @@ let constrain n (ids, m as x) (names, terms as subst) = if List.equal Id.equal ids ids' && eq_constr m m' then subst else raise PatternMatchingFailure with Not_found -> - let () = if Id.Map.mem n names then warn_bound_meta n in + let () = if Id.Map.mem n names then warn_meta_collision n in (names, Id.Map.add n x terms) let add_binders na1 na2 binding_vars (names, terms as subst) = match na1, na2 with | Name id1, Name id2 when Id.Set.mem id1 binding_vars -> if Id.Map.mem id1 names then - let () = warn_bound_bound id1 in + let () = Glob_ops.warn_variable_collision id1 in (names, terms) else let names = Id.Map.add id1 id2 names in - let () = if Id.Map.mem id1 terms then warn_bound_meta id1 in + let () = if Id.Map.mem id1 terms then + warn_meta_collision id1 in (names, terms) | _ -> subst diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 86921c49b..cc178eb97 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -620,7 +620,7 @@ and share_names flags n l avoid env sigma c t = share_names flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c' (* If built with the f/n notation: we renounce to share names *) | _ -> - if n>0 then Feedback.msg_warning (strbrk "Detyping.detype: cannot factorize fix enough"); + if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough"); let c = detype flags avoid env sigma c in let t = detype flags avoid env sigma t in (List.rev l,c,t) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 04100c8a7..5c8060996 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -334,10 +334,14 @@ let glob_visible_short_qualid c = fold_glob_constr aux acc c in aux [] c +let warn_variable_collision = + let open Pp in + CWarnings.create ~name:"variable-collision" ~category:"ltac" + (fun name -> + strbrk "Collision between bound variables of name " ++ pr_id name) + let add_and_check_ident id set = - if Id.Set.mem id set then - Feedback.msg_warning - Pp.(str "Collision between bound variables of name " ++ Id.print id); + if Id.Set.mem id set then warn_variable_collision id; Id.Set.add id set let bound_glob_vars = diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index e0a2de032..c2b27ca6a 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -34,6 +34,8 @@ val map_glob_constr : val map_glob_constr_left_to_right : (glob_constr -> glob_constr) -> glob_constr -> glob_constr +val warn_variable_collision : ?loc:Loc.t -> Id.t -> unit + val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit val occur_glob_constr : Id.t -> glob_constr -> bool diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 5d36fc78e..fc38e98c6 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -183,9 +183,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = | ra::rest -> (match dest_recarg ra with | Mrec (_,j) when is_rec -> (depPvect.(j),rest) - | Imbr _ -> - Feedback.msg_warning (strbrk "Ignoring recursive call"); - (None,rest) + | Imbr _ -> (None,rest) | _ -> (None, rest)) in (match optionpos with diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index d6305d81a..7eb3d633d 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -317,6 +317,10 @@ let rev_it_mkPLambda = List.fold_right mkPLambda let err loc pp = user_err_loc (loc,"pattern_of_glob_constr", pp) +let warn_cast_in_pattern = + CWarnings.create ~name:"cast-in-pattern" ~category:"automation" + (fun () -> Pp.strbrk "Casts are ignored in patterns") + let rec pat_of_raw metas vars = function | GVar (_,id) -> (try PRel (List.index Name.equal (Name id) vars) @@ -348,7 +352,7 @@ let rec pat_of_raw metas vars = function | GHole _ -> PMeta None | GCast (_,c,_) -> - Feedback.msg_warning (strbrk "Cast not taken into account in constr pattern"); + warn_cast_in_pattern (); pat_of_raw metas vars c | GIf (_,c,(_,None),b1,b2) -> PIf (pat_of_raw metas vars c, diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index bbb6a9266..2959bd7c8 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -187,6 +187,13 @@ let cs_pattern_of_constr t = with e when Errors.noncritical e -> raise Not_found end +let warn_projection_no_head_constant = + CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker" + (fun (t,con_pp,proji_sp_pp) -> + strbrk "Projection value has no head constant: " + ++ Termops.print_constr t ++ strbrk " in canonical instance " + ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.") + (* Intended to always succeed *) let compute_canonical_projections (con,ind) = let env = Global.env () in @@ -213,13 +220,10 @@ let compute_canonical_projections (con,ind) = let patt, n , args = cs_pattern_of_constr t in ((ConstRef proji_sp, patt, t, n, args) :: l) with Not_found -> - if Flags.is_verbose () then - (let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) + let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) and proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in - Feedback.msg_warning (strbrk "No global reference exists for projection value" - ++ Termops.print_constr t ++ strbrk " in instance " - ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")); - l + warn_projection_no_head_constant (t,con_pp,proji_sp_pp); + l end | _ -> l) [] lps in @@ -235,6 +239,13 @@ let pr_cs_pattern = function | Default_cs -> str "_" | Sort_cs s -> Termops.pr_sort_family s +let warn_redundant_canonical_projection = + CWarnings.create ~name:"redundant-canonical-projection" ~category:"typechecker" + (fun (hd_val,prj,new_can_s,old_can_s) -> + strbrk "Ignoring canonical projection to " ++ hd_val + ++ strbrk " by " ++ prj ++ strbrk " in " + ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s) + let open_canonical_structure i (_,o) = if Int.equal i 1 then let lo = compute_canonical_projections o in @@ -245,14 +256,12 @@ let open_canonical_structure i (_,o) = in match ocs with | None -> object_table := Refmap.add proj ((pat,s)::l) !object_table; | Some (c, cs) -> - if Flags.is_verbose () then let old_can_s = (Termops.print_constr cs.o_DEF) and new_can_s = (Termops.print_constr s.o_DEF) in let prj = (Nametab.pr_global_env Id.Set.empty proj) and hd_val = (pr_cs_pattern cs_pat) in - Feedback.msg_warning (strbrk "Ignoring canonical projection to " ++ hd_val - ++ strbrk " by " ++ prj ++ strbrk " in " - ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s)) lo + warn_redundant_canonical_projection (hd_val,prj,new_can_s,old_can_s)) + lo let cache_canonical_structure o = open_canonical_structure 1 o diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 13b5848a3..ee5591521 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -29,10 +29,15 @@ let cbv_vm env sigma c = error "vm_compute does not support existential variables."; Vnorm.cbv_vm env c ctyp +let warn_native_compute_disabled = + CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler" + (fun () -> + strbrk "native_compute disabled at configure time; falling back to vm_compute.") + let cbv_native env sigma c = if Coq_config.no_native_compiler then - let () = Feedback.msg_warning (str "native_compute disabled at configure time; falling back to vm_compute.") in - cbv_vm env sigma c + (warn_native_compute_disabled (); + cbv_vm env sigma c) else let ctyp = Retyping.get_type_of env sigma c in Nativenorm.native_norm env sigma c ctyp @@ -209,6 +214,11 @@ let contextualize f g = function e_red (contextually b (l,c) (fun _ -> h)) | None -> e_red g +let warn_simpl_unfolding_modifiers = + CWarnings.create ~name:"simpl-unfolding-modifiers" ~category:"tactics" + (fun () -> + Pp.strbrk "The legacy simpl ignores constant unfolding modifiers.") + let reduction_of_red_expr env = let make_flag = make_flag env in let rec reduction_of_red_expr = function @@ -221,7 +231,7 @@ let reduction_of_red_expr env = let am = if !simplIsCbn then strong_cbn (make_flag f) else simpl in let () = if not (!simplIsCbn || List.is_empty f.rConst) then - Feedback.msg_warning (Pp.strbrk "The legacy simpl does not deal with delta flags.") in + warn_simpl_unfolding_modifiers () in (contextualize (if head_style then whd_am else am) am o,DEFAULTcast) | Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast) | Cbn f -> diff --git a/stm/lemmas.ml b/stm/lemmas.ml index a2e8fac05..50dceb8e6 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -301,13 +301,16 @@ let save_anonymous_with_strength ?export_seff proof kind save_ident = (* Admitted *) +let warn_let_as_axiom = + CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" + (fun id -> strbrk "Let definition" ++ spc () ++ pr_id id ++ + spc () ++ strbrk "declared as an axiom.") + let admit (id,k,e) pl hook () = let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in let () = match k with | Global, _, _ -> () - | Local, _, _ | Discharge, _, _ -> - Feedback.msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++ - str "declared as an axiom.") + | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id in let () = assumption_message id in Option.iter (Universes.register_universe_binders (ConstRef kn)) pl; diff --git a/stm/stm.ml b/stm/stm.ml index d460cea94..928a0dd6f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -989,8 +989,6 @@ end = struct (* {{{ *) | VernacResetInitial -> VtStm (VtBack Stateid.initial, true), VtNow | VernacResetName (_,name) -> - msg_warning - (str"Reset not implemented for automatically generated constants"); let id = VCS.get_branch_pos (VCS.current_branch ()) in (try let oid = @@ -1040,8 +1038,8 @@ end = struct (* {{{ *) | _ -> VtUnknown, VtNow with | Not_found -> - msg_warning(str"undo_vernac_classifier: going back to the initial state."); - VtStm (VtBack Stateid.initial, true), VtNow + Errors.errorlabstrm "undo_vernac_classifier" + (str "Cannot undo") end (* }}} *) @@ -1368,7 +1366,7 @@ end = struct (* {{{ *) when is_tac expr && State.same_env o n -> (* A pure tactic *) Some (id, `Proof (prev, State.proof_part_of_frozen n)) | Some _, Some s -> - msg_warning (str "STM: sending back a fat state"); + msg_debug (str "STM: sending back a fat state"); Some (id, `Full s) | _, Some s -> Some (id, `Full s) in let rec aux seen = function @@ -1898,6 +1896,12 @@ let delegate name = || !Flags.compilation_mode = Flags.BuildVio || !Flags.async_proofs_full +let warn_deprecated_nested_proofs = + CWarnings.create ~name:"deprecated-nested-proofs" ~category:"deprecated" + (fun () -> + strbrk ("Nested proofs are deprecated and will "^ + "stop working in a future Coq version")) + let collect_proof keep cur hd brkind id = prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id); let no_name = "" in @@ -1962,8 +1966,7 @@ let collect_proof keep cur hd brkind id = let name = name ids in `MaybeASync (parent last, None, accn, name, delegate name) | `Sideff _ -> - Pp.(msg_warning (strbrk ("Nested proofs are deprecated and will "^ - "stop working in the next Coq version"))); + warn_deprecated_nested_proofs (); `Sync (no_name,None,`NestedProof) | _ -> `Sync (no_name,None,`Unknown) in let make_sync why = function @@ -2410,10 +2413,7 @@ let reset_task_queue = Slaves.reset_task_queue (* Document building *) let process_transaction ?(newtip=Stateid.fresh ()) ~tty - ({ verbose; loc; expr } as x) c - = - let warn_if_pos a b = - if b then msg_warning(pr_ast a ++ str" should not be part of a script") in + ({ verbose; loc; expr } as x) c = prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x)); let vcs = VCS.backup () in try @@ -2427,12 +2427,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty | VtStm(VtPG,false), VtNow -> vernac_interp Stateid.dummy x; `Ok | VtStm(VtPG,_), _ -> anomaly(str "PG command in script or VtLater") (* Joining various parts of the document *) - | VtStm (VtJoinDocument, b), VtNow -> warn_if_pos x b; join (); `Ok - | VtStm (VtFinish, b), VtNow -> warn_if_pos x b; finish (); `Ok - | VtStm (VtWait, b), VtNow -> warn_if_pos x b; finish (); wait (); `Ok + | VtStm (VtJoinDocument, b), VtNow -> join (); `Ok + | VtStm (VtFinish, b), VtNow -> finish (); `Ok + | VtStm (VtWait, b), VtNow -> finish (); wait (); `Ok | VtStm (VtPrintDag, b), VtNow -> - warn_if_pos x b; VCS.print ~now:true (); `Ok - | VtStm (VtObserve id, b), VtNow -> warn_if_pos x b; observe id; `Ok + VCS.print ~now:true (); `Ok + | VtStm (VtObserve id, b), VtNow -> observe id; `Ok | VtStm ((VtObserve _ | VtFinish | VtJoinDocument |VtPrintDag |VtWait),_), VtLater -> anomaly(str"classifier: join actions cannot be classified as VtLater") @@ -2642,6 +2642,7 @@ let add ~ontop ?newtip ?(check=ignore) verb eid s = anomaly(str"Not yet implemented, the GUI should not try this"); let indentation, strlen, loc, ast = vernac_parse ~indlen_prev:(fun () -> ind_len_of ontop) ?newtip eid s in + CWarnings.set_current_loc loc; check(loc,ast); let clas = classify_vernac ast in let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in @@ -2663,6 +2664,7 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) s = else Reach.known_state ~cache:`Yes at; let newtip, route = report_with in let indentation, strlen, loc, ast = vernac_parse ~newtip ~route 0 s in + CWarnings.set_current_loc loc; let clas = classify_vernac ast in let aast = { verbose = true; indentation; strlen; loc; expr = ast } in match clas with diff --git a/tactics/hints.ml b/tactics/hints.ml index 952719129..2c2b76412 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -708,7 +708,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, else begin if not eapply then failwith "make_apply_entry"; if verbose then - Feedback.msg_warning (str "the hint: eapply " ++ pr_lconstr c ++ + Feedback.msg_info (str "the hint: eapply " ++ pr_lconstr c ++ str " will only be used by eauto"); (Some hd, { pri = (match pri with None -> nb_hyp cty + nmiss | Some p -> p); @@ -743,6 +743,12 @@ let input_context_set : Univ.ContextSet.t -> Libobject.obj = discharge_function = (fun (_,a) -> Some a); classify_function = (fun a -> Keep a) } +let warn_polymorphic_hint = + CWarnings.create ~name:"polymorphic-hint" ~category:"automation" + (fun hint -> strbrk"Using polymorphic hint " ++ hint ++ + str" monomorphically" ++ + strbrk" use Polymorphic Hint to use it polymorphically.") + let fresh_global_or_constr env sigma poly cr = let isgr, (c, ctx) = match cr with @@ -754,9 +760,7 @@ let fresh_global_or_constr env sigma poly cr = else if Univ.ContextSet.is_empty ctx then (c, ctx) else begin if isgr then - Feedback.msg_warning (str"Using polymorphic hint " ++ - pr_hint_term env sigma ctx cr ++ str" monomorphically" ++ - str" use Polymorphic Hint to use it polymorphically."); + warn_polymorphic_hint (pr_hint_term env sigma ctx cr); Lib.add_anonymous_leaf (input_context_set ctx); (c, Univ.ContextSet.empty) end @@ -1389,10 +1393,15 @@ let print_mp mp = let is_imported h = try KNmap.find h.uid !statustable with Not_found -> true +let warn_non_imported_hint = + CWarnings.create ~name:"non-imported-hint" ~category:"automation" + (fun (hint,mp) -> + strbrk "Hint used but not imported: " ++ hint ++ print_mp mp) + let warn h x = let hint = pr_hint h in let (mp, _, _) = KerName.repr h.uid in - let () = Feedback.msg_warning (str "Hint used but not imported: " ++ hint ++ print_mp mp) in + warn_non_imported_hint (hint,mp); Proofview.tclUNIT x let run_hint tac k = match !warn_hint with diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f3e117f8c..cf842d6f1 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2976,13 +2976,17 @@ let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id] *) +let warn_unused_intro_pattern = + CWarnings.create ~name:"unused-intro-pattern" ~category:"tactics" + (fun names -> + strbrk"Unused introduction " ++ str (String.plural (List.length names) "pattern") + ++ str": " ++ prlist_with_sep spc + (Miscprint.pr_intro_pattern + (fun c -> Printer.pr_constr (fst (run_delayed (Global.env()) Evd.empty c)))) names) + let check_unused_names names = if not (List.is_empty names) && Flags.is_verbose () then - Feedback.msg_warning - (str"Unused introduction " ++ str (String.plural (List.length names) "pattern") - ++ str": " ++ prlist_with_sep spc - (Miscprint.pr_intro_pattern - (fun c -> Printer.pr_constr (fst (run_delayed (Global.env()) Evd.empty c)))) names) + warn_unused_intro_pattern names let intropattern_of_name gl avoid = function | Anonymous -> IntroNaming IntroAnonymous 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"<unknown>") - 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 |