diff options
52 files changed, 475 insertions, 302 deletions
diff --git a/checker/check.ml b/checker/check.ml index 1ff1425dea..587bb90d43 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -149,7 +149,7 @@ let remove_load_path dir = load_paths := List.filter2 (fun p d -> p <> dir) physical logical let add_load_path (phys_path,coq_path) = - if !Flags.debug then + if CDebug.(get_flag misc) then Feedback.msg_notice (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++ str phys_path); let phys_path = CUnix.canonical_path_name phys_path in diff --git a/checker/checker.ml b/checker/checker.ml index bdfc5f07be..588ce14336 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -132,8 +132,6 @@ let init_load_path () = includes := [] -let set_debug () = Flags.debug := true - let impredicative_set = ref Declarations.PredicativeSet let set_impredicative_set () = impredicative_set := Declarations.ImpredicativeSet @@ -222,7 +220,7 @@ let guill s = str "\"" ++ str s ++ str "\"" let where = function | None -> mt () | Some s -> - if !Flags.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) + if CDebug.(get_flag misc) then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) let explain_exn = function | Stream.Failure -> @@ -251,7 +249,7 @@ let explain_exn = function hov 0 (fnl () ++ str "User interrupt.") | Univ.UniverseInconsistency i -> let msg = - if !Flags.debug then + if CDebug.(get_flag misc) then str "." ++ spc() ++ Univ.explain_universe_inconsistency Univ.Level.pr i else @@ -339,7 +337,7 @@ let parse_args argv = | ("-Q"|"-R") :: d :: p :: rem -> set_include d p;parse rem | ("-Q"|"-R") :: ([] | [_]) -> usage () - | "-debug" :: rem -> set_debug (); parse rem + | "-debug" :: rem -> CDebug.set_debug_all true; parse rem | "-where" :: _ -> Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); @@ -377,7 +375,7 @@ let init_with_argv argv = try parse_args argv; CWarnings.set_flags ("+"^Typeops.warn_bad_relevance_name); - if !Flags.debug then Printexc.record_backtrace true; + if CDebug.(get_flag misc) then Printexc.record_backtrace true; Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); Flags.if_verbose print_header (); init_load_path (); @@ -392,7 +390,7 @@ let run senv = let senv = compile_files senv in flush_all(); senv with e -> - if !Flags.debug then Printexc.print_backtrace stderr; + if CDebug.(get_flag misc) then Printexc.print_backtrace stderr; fatal_error (explain_exn e) (is_anomaly e) let start () = diff --git a/doc/changelog/07-vernac-commands-and-options/13202-debug-infra.rst b/doc/changelog/07-vernac-commands-and-options/13202-debug-infra.rst new file mode 100644 index 0000000000..cd1ac3a35a --- /dev/null +++ b/doc/changelog/07-vernac-commands-and-options/13202-debug-infra.rst @@ -0,0 +1,19 @@ +- **Added:** + :opt:`Debug` to control debug messages, functioning similarly to the warning system + (`#13202 <https://github.com/coq/coq/pull/13202>`_, + by Maxime Dénès and Gaëtan Gilbert). + The following flags have been converted (such that ``Set Flag`` becomes ``Set Debug "flag"``): + + - ``Debug Unification`` to ``unification`` + + - ``Debug HO Unification`` to ``ho-unification`` + + - ``Debug Tactic Unification`` to ``tactic-unification`` + + - ``Congruence Verbose`` to ``congruence`` + + - ``Debug Cbv`` to ``cbv`` + + - ``Debug RAKAM`` to ``RAKAM`` + + - ``Debug Ssreflect`` to ``ssreflect`` diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 665bae7077..071fcbee11 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -675,10 +675,10 @@ Applying theorems :tacn:`notypeclasses refine`: it performs type checking without resolution of typeclasses, does not perform beta reductions or shelve the subgoals. - .. flag:: Debug Unification - - Enables printing traces of unification steps used during - elaboration/typechecking and the :tacn:`refine` tactic. + :opt:`Debug` ``"unification"`` enables printing traces of + unification steps used during elaboration/typechecking and the + :tacn:`refine` tactic. ``"ho-unification"`` prints information + about higher order heuristics. .. tacn:: apply @term :name: apply @@ -1040,10 +1040,9 @@ Applying theorems when the instantiation of a variable cannot be found (cf. :tacn:`eapply` and :tacn:`apply`). -.. flag:: Debug Tactic Unification - - Enables printing traces of unification steps in tactic unification. - Tactic unification is used in tactics such as :tacn:`apply` and :tacn:`rewrite`. +:opt:`Debug` ``"tactic-unification"`` enables printing traces of +unification steps in tactic unification. Tactic unification is used in +tactics such as :tacn:`apply` and :tacn:`rewrite`. .. _managingthelocalcontext: diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 8db16fff69..37d605360d 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -865,6 +865,14 @@ Controlling display interpreted from left to right, so in case of an overlap, the flags on the right have higher priority, meaning that `A,-A` is equivalent to `-A`. +.. opt:: Debug "{+, {? - } @ident }" + + Configures the display of debug messages. Each :n:`@ident` enables debug messages + for that component, while :n:`-@ident` disables messages for the component. + ``all`` activates or deactivates all other components. ``backtrace`` controls printing of + error backtraces. + + :cmd:`Test` `Debug` displays the list of components and their enabled/disabled state. .. opt:: Printing Width @natural This command sets which left-aligned part of the width of the screen is used diff --git a/doc/sphinx/proofs/automatic-tactics/logic.rst b/doc/sphinx/proofs/automatic-tactics/logic.rst index 5aaded2726..3f1f5d46c5 100644 --- a/doc/sphinx/proofs/automatic-tactics/logic.rst +++ b/doc/sphinx/proofs/automatic-tactics/logic.rst @@ -194,9 +194,7 @@ Solvers for logic and equality additional arguments can be given to congruence by filling in the holes in the terms given in the error message, using the `with` clause. - .. flag:: Congruence Verbose - - Makes :tacn:`congruence` print debug information. + :opt:`Debug` ``"congruence"`` makes :tacn:`congruence` print debug information. .. tacn:: btauto diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index f286533d78..8c000a4aa7 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -559,9 +559,7 @@ the conversion in hypotheses :n:`{+ @ident}`. on the profile file to see the results. Consult the ``perf`` documentation for more details. -.. flag:: Debug Cbv - - This flag makes :tacn:`cbv` (and its derivative :tacn:`compute`) print + :opt:`Debug` ``"Cbv"`` makes :tacn:`cbv` (and its derivative :tacn:`compute`) print information about the constants it encounters and the unfolding decisions it makes. @@ -662,10 +660,8 @@ the conversion in hypotheses :n:`{+ @ident}`. This applies :tacn:`simpl` only to the :n:`{+ @natural}` applicative subterms whose head occurrence is :n:`@qualid` (or :n:`@string`). -.. flag:: Debug RAKAM - - This flag makes :tacn:`cbn` print various debugging information. - ``RAKAM`` is the Refolding Algebraic Krivine Abstract Machine. +:opt:`Debug` ``"RAKAM"`` makes :tacn:`cbn` print various debugging information. +``RAKAM`` is the Refolding Algebraic Krivine Abstract Machine. .. tacn:: unfold @qualid :name: unfold diff --git a/ide/coqide/coqide.ml b/ide/coqide/coqide.ml index e066fc6292..3fbfbd66d3 100644 --- a/ide/coqide/coqide.ml +++ b/ide/coqide/coqide.ml @@ -1374,8 +1374,7 @@ let main files = let read_coqide_args argv = let set_debug () = Minilib.debug := true; - Flags.debug := true; - Exninfo.record_backtrace true + CDebug.set_debug_all true in let rec filter_coqtop coqtop project_files bindings_files out = function |"-unicode-bindings" :: sfilenames :: args -> diff --git a/ide/coqide/coqide_main.ml b/ide/coqide/coqide_main.ml index 0812e00960..a178e72806 100644 --- a/ide/coqide/coqide_main.ml +++ b/ide/coqide/coqide_main.ml @@ -35,7 +35,7 @@ let catch_gtk_messages () = let () = GToolbox.message_box ~title:"Error" (header ^ msg) in Coqide.crash_save 1 |`ERROR -> - if !Flags.debug then GToolbox.message_box ~title:"Error" (header ^ msg) + if CDebug.(get_flag misc) then GToolbox.message_box ~title:"Error" (header ^ msg) else Printf.eprintf "%s\n" (header ^ msg) |`DEBUG -> Minilib.log msg |level when Sys.os_type = "Win32" -> Minilib.log ~level msg diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index b42c705add..4b069b09ba 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -35,11 +35,11 @@ let pr_with_pid s = Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s let pr_error s = pr_with_pid s let pr_debug s = - if !Flags.debug then pr_with_pid s + if CDebug.(get_flag misc) then pr_with_pid s let pr_debug_call q = - if !Flags.debug then pr_with_pid ("<-- " ^ Xmlprotocol.pr_call q) + if CDebug.(get_flag misc) then pr_with_pid ("<-- " ^ Xmlprotocol.pr_call q) let pr_debug_answer q r = - if !Flags.debug then pr_with_pid ("--> " ^ Xmlprotocol.pr_full_value q r) + if CDebug.(get_flag misc) then pr_with_pid ("--> " ^ Xmlprotocol.pr_full_value q r) (** Categories of commands *) diff --git a/ide/coqide/microPG.ml b/ide/coqide/microPG.ml index 5a4871b70a..9908703cea 100644 --- a/ide/coqide/microPG.ml +++ b/ide/coqide/microPG.ml @@ -15,7 +15,7 @@ open GdkKeysyms open Printf let eprintf x = - if !Flags.debug then Printf.eprintf x else Printf.ifprintf stderr x + if CDebug.(get_flag misc) then Printf.eprintf x else Printf.ifprintf stderr x type gui = { notebook : session Wg_Notebook.typed_notebook; diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index c19b883e3d..d517d215ed 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -24,6 +24,11 @@ open Environ compiler. mllambda represents a fragment of ML, and can easily be printed to OCaml code. *) +let debug_native_flag, debug_native_compiler = CDebug.create_full ~name:"native-compiler" () + +let keep_debug_files () = + CDebug.get_flag debug_native_flag + (** Local names **) (* The first component is there for debugging purposes only *) @@ -1939,7 +1944,7 @@ let compile_constant env sigma con cb = | Def t -> let t = Mod_subst.force_constr t in let code = lambda_of_constr env sigma t in - if !Flags.debug then Feedback.msg_debug (Pp.str "Generated lambda code"); + debug_native_compiler (fun () -> Pp.str "Generated lambda code"); let is_lazy = is_lazy t in let code = if is_lazy then mk_lazy code else code in let l = Constant.label con in @@ -1950,11 +1955,11 @@ let compile_constant env sigma con cb = let (auxdefs,code) = compile_with_fv env sigma (Some univ) [] (Some l) code in (auxdefs,mkMLlam [|univ|] code) in - if !Flags.debug then Feedback.msg_debug (Pp.str "Generated mllambda code"); + debug_native_compiler (fun () -> Pp.str "Generated mllambda code"); let code = optimize_stk (Glet(Gconstant ("", con),code)::auxdefs) in - if !Flags.debug then Feedback.msg_debug (Pp.str "Optimized mllambda code"); + debug_native_compiler (fun () -> Pp.str "Optimized mllambda code"); code | _ -> let i = push_symbol (SymbConst con) in diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index aab6e1d4a0..1b14801fec 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -21,6 +21,10 @@ to OCaml code. *) type mllambda type global +val debug_native_compiler : CDebug.t + +val keep_debug_files : unit -> bool + val pp_global : Format.formatter -> global -> unit val mk_open : string -> global diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index d77ee759c6..7e73725c6c 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -159,12 +159,12 @@ let native_conv_gen pb sigma env univs t1 t2 = let ml_filename, prefix = get_ml_filename () in let code, upds = mk_conv_code env sigma prefix t1 t2 in let fn = compile ml_filename code ~profile:false in - if !Flags.debug then Feedback.msg_debug (Pp.str "Running test..."); + debug_native_compiler (fun () -> Pp.str "Running test..."); let t0 = Sys.time () in call_linker ~fatal:true ~prefix fn (Some upds); let t1 = Sys.time () in let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in - if !Flags.debug then Feedback.msg_debug (Pp.str time_info); + debug_native_compiler (fun () -> Pp.str time_info); (* TODO change 0 when we can have de Bruijn *) fst (conv_val env pb 0 !rt1 !rt2 univs) diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 1e1085d5ff..3eb3c949bc 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -38,7 +38,7 @@ let ( / ) = Filename.concat let my_temp_dir = lazy (CUnix.mktemp_dir "Coq_native" "") let () = at_exit (fun () -> - if not !Flags.debug && Lazy.is_val my_temp_dir then + if not (keep_debug_files ()) && Lazy.is_val my_temp_dir then try let d = Lazy.force my_temp_dir in Array.iter (fun f -> Sys.remove (Filename.concat d f)) (Sys.readdir d); @@ -129,7 +129,7 @@ let call_compiler ?profile:(profile=false) ml_filename = ::"-w"::"a" ::include_dirs) @ ["-impl"; ml_filename] in - if !Flags.debug then Feedback.msg_debug (Pp.str (Envars.ocamlfind () ^ " " ^ (String.concat " " args))); + debug_native_compiler (fun () -> Pp.str (Envars.ocamlfind () ^ " " ^ (String.concat " " args))); try let res = CUnix.sys_command (Envars.ocamlfind ()) args in match res with @@ -142,7 +142,7 @@ let call_compiler ?profile:(profile=false) ml_filename = let compile fn code ~profile:profile = write_ml_code fn code; let r = call_compiler ~profile fn in - if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn; + if (not (keep_debug_files ())) && Sys.file_exists fn then Sys.remove fn; r type native_library = Nativecode.global list * Nativevalues.symbols @@ -160,7 +160,7 @@ let compile_library (code, symb) fn = let fn = dirname / basename in write_ml_code fn ~header code; let _ = call_compiler fn in - if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn + if (not (keep_debug_files ())) && Sys.file_exists fn then Sys.remove fn (* call_linker links dynamically the code for constants in environment or a *) (* conversion test. *) @@ -171,7 +171,7 @@ let call_linker ?(fatal=true) ~prefix f upds = begin let msg = "Cannot find native compiler file " ^ f in if fatal then CErrors.user_err Pp.(str msg) - else if !Flags.debug then Feedback.msg_debug (Pp.str msg) + else debug_native_compiler (fun () -> Pp.str msg) end else (try @@ -180,7 +180,7 @@ let call_linker ?(fatal=true) ~prefix f upds = with Dynlink.Error _ as exn -> let exn = Exninfo.capture exn in if fatal then Exninfo.iraise exn - else if !Flags.debug then Feedback.msg_debug CErrors.(iprint exn)); + else debug_native_compiler (fun () -> CErrors.(iprint exn))); match upds with Some upds -> update_locations upds | _ -> () let link_library ~prefix ~dirname ~basename = diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index c95880dc36..2e27fe071e 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -28,35 +28,35 @@ and translate_field prefix mp env acc (l,x) = match x with | SFBconst cb -> let con = Constant.make2 mp l in - (if !Flags.debug then + (debug_native_compiler (fun () -> let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in - Feedback.msg_debug (Pp.str msg)); + Pp.str msg)); compile_constant_field env prefix con acc cb | SFBmind mb -> - (if !Flags.debug then + (debug_native_compiler (fun () -> let id = mb.mind_packets.(0).mind_typename in let msg = Printf.sprintf "Compiling inductive %s..." (Id.to_string id) in - Feedback.msg_debug (Pp.str msg)); + Pp.str msg)); compile_mind_field mp l acc mb | SFBmodule md -> let mp = md.mod_mp in - (if !Flags.debug then + (debug_native_compiler (fun () -> let msg = Printf.sprintf "Compiling module %s..." (ModPath.to_string mp) in - Feedback.msg_debug (Pp.str msg)); + Pp.str msg)); translate_mod prefix mp env md.mod_type acc | SFBmodtype mdtyp -> let mp = mdtyp.mod_mp in - (if !Flags.debug then + (debug_native_compiler (fun () -> let msg = Printf.sprintf "Compiling module type %s..." (ModPath.to_string mp) in - Feedback.msg_debug (Pp.str msg)); + Pp.str msg)); translate_mod prefix mp env mdtyp.mod_type acc let dump_library mp dp env mod_expr = - if !Flags.debug then Feedback.msg_debug (Pp.str "Compiling library..."); + debug_native_compiler (fun () -> Pp.str "Compiling library..."); match mod_expr with | NoFunctor struc -> let env = add_structure mp struc empty_delta_resolver env in diff --git a/lib/cDebug.ml b/lib/cDebug.ml new file mode 100644 index 0000000000..efa7365b91 --- /dev/null +++ b/lib/cDebug.ml @@ -0,0 +1,92 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +type flag = bool ref + +type t = (unit -> Pp.t) -> unit + +let debug = ref CString.Map.empty + +(* Used to remember level of Set Debug "all" for debugs created by + plugins dynlinked after the Set *) +let all_flag = ref false + +let set_debug_backtrace b = + Exninfo.record_backtrace b + +let set_debug_all b = + set_debug_backtrace b; + CString.Map.iter (fun _ flag -> flag := b) !debug; + all_flag := b + +let create_full ~name () = + let anomaly pp = CErrors.anomaly ~label:"CDebug.create" pp in + let () = match name with + | "all"|"backtrace" -> anomaly Pp.(str"The debug name \""++str name++str"\" is reserved.") + | _ -> + if CString.Map.mem name !debug then + anomaly Pp.(str "The debug name \"" ++ str name ++ str "\" is already used.") + in + let pp x = + Feedback.msg_debug Pp.(str "[" ++ str name ++ str "] " ++ x) + in + let flag = ref !all_flag in + debug := CString.Map.add name flag !debug; + let pp x = + if !flag + then pp (x ()) + in + flag, pp + +let create ~name () = + snd (create_full ~name ()) + +let get_flag flag = !flag + +let warn_unknown_debug = CWarnings.create ~name:"unknown-debug-flag" ~category:"option" + Pp.(fun name -> str "There is no debug flag \"" ++ str name ++ str "\".") + +let get_flags () = + let pp_flag name flag = if flag then name else "-"^name in + let flags = + CString.Map.fold + (fun name v acc -> pp_flag name !v :: acc) + !debug [] + in + let all = pp_flag "all" !all_flag in + let bt = pp_flag "backtrace" (Printexc.backtrace_status()) in + String.concat "," (all::bt::flags) + +exception Error + +let parse_flags s = + let parse_flag s = + if CString.is_empty s then raise Error + else if s.[0] = '-' + then String.sub s 1 (String.length s - 1), false + else s, true + in + try + Some (CList.map parse_flag @@ String.split_on_char ',' s) + with Error -> None + +let set_flags s = match parse_flags s with + | None -> CErrors.user_err Pp.(str "Syntax error in debug flags.") + | Some flags -> + let set_one_flag (name,b) = match name with + | "all" -> set_debug_all b + | "backtrace" -> set_debug_backtrace b + | _ -> match CString.Map.find_opt name !debug with + | None -> warn_unknown_debug name + | Some flag -> flag := b + in + List.iter set_one_flag flags + +let misc, pp_misc = create_full ~name:"misc" () diff --git a/lib/cDebug.mli b/lib/cDebug.mli new file mode 100644 index 0000000000..846c4b493b --- /dev/null +++ b/lib/cDebug.mli @@ -0,0 +1,50 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +type flag + +type t = (unit -> Pp.t) -> unit + +(** Creates a debug component, which may be used to print debug + messages. + + A debug component is named by the string [name]. It is either + active or inactive. + + The special component ["all"] may be used to control all components. + + There is also a special component ["backtrace"] to control + backtrace recording. +*) +val create : name:string -> unit -> t + +(** Useful when interacting with a component from code, typically when + doing something more complicated than printing. + + Note that the printer function prints some metadata compared to + [ fun pp -> if get_flag flag then Feedback.msg_debug (pp ()) ] + *) +val create_full : name:string -> unit -> flag * t + +val get_flag : flag -> bool + +(** [get_flags] and [set_flags] use the user syntax: a comma separated + list of activated "component" and "-component"s. [get_flags] starts + with "all" or "-all" and lists all components after it (even if redundant). *) +val get_flags : unit -> string + +(** Components not mentioned are not affected (use the "all" component + at the start if you want to reset everything). *) +val set_flags : string -> unit + +val set_debug_all : bool -> unit + +val misc : flag +val pp_misc : t diff --git a/lib/flags.ml b/lib/flags.ml index 83733cf00d..57e879add7 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -46,7 +46,6 @@ let async_proofs_is_worker () = !async_proofs_worker_id <> "master" let load_vos_libraries = ref false -let debug = ref false let xml_debug = ref false let in_debugger = ref false diff --git a/lib/flags.mli b/lib/flags.mli index ebd23a4d20..e10e2c8cb8 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -40,7 +40,6 @@ val async_proofs_is_worker : unit -> bool val load_vos_libraries : bool ref (** Debug flags *) -val debug : bool ref val xml_debug : bool ref val in_debugger : bool ref val in_toplevel : bool ref diff --git a/lib/lib.mllib b/lib/lib.mllib index 4e08e87084..bbc9966498 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -10,6 +10,7 @@ Loc Feedback CErrors CWarnings +CDebug AcyclicGraph Rtree diff --git a/lib/spawn.ml b/lib/spawn.ml index 2fe7b31d04..27b4387b61 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -13,7 +13,7 @@ let prefer_sock = Sys.os_type = "Win32" let accept_timeout = 10.0 let pr_err s = Printf.eprintf "(Spawn ,%d) %s\n%!" (Unix.getpid ()) s -let prerr_endline s = if !Flags.debug then begin pr_err s end else () +let prerr_endline s = if CDebug.(get_flag misc) then begin pr_err s end else () type req = ReqDie | Hello of int * int diff --git a/library/nametab.ml b/library/nametab.ml index e94b696b60..bd96446f1c 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -574,7 +574,7 @@ let pr_global_env env ref = try pr_qualid (shortest_qualid_of_global env ref) with Not_found as exn -> let exn, info = Exninfo.capture exn in - if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); + if CDebug.(get_flag misc) then Feedback.msg_debug (Pp.str "pr_global_env not found"); Exninfo.iraise (exn, info) let global_inductive qid = diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 129b220680..6617f4726e 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -19,20 +19,12 @@ open Sorts open Constr open Context open Vars -open Goptions open Tacmach open Util let init_size=5 -let cc_verbose= - declare_bool_option_and_ref - ~depr:false - ~key:["Congruence";"Verbose"] - ~value:false - -let debug x = - if cc_verbose () then Feedback.msg_debug (x ()) +let debug_congruence = CDebug.create ~name:"congruence" () (* Signature table *) @@ -576,7 +568,7 @@ let add_inst state (inst,int_subst) = Control.check_for_interrupt (); if state.rew_depth > 0 then if is_redundant state inst.qe_hyp_id int_subst then - debug (fun () -> str "discarding redundant (dis)equality") + debug_congruence (fun () -> str "discarding redundant (dis)equality") else begin Identhash.add state.q_history inst.qe_hyp_id int_subst; @@ -591,7 +583,7 @@ let add_inst state (inst,int_subst) = state.rew_depth<-pred state.rew_depth; if inst.qe_pol then begin - debug (fun () -> + debug_congruence (fun () -> (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++ (str " [" ++ Printer.pr_econstr_env state.env state.sigma (EConstr.of_constr prf) ++ str " : " ++ pr_term state.env state.sigma s ++ str " == " ++ pr_term state.env state.sigma t ++ str "]")); @@ -599,7 +591,7 @@ let add_inst state (inst,int_subst) = end else begin - debug (fun () -> + debug_congruence (fun () -> (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++ (str " [" ++ Printer.pr_econstr_env state.env state.sigma (EConstr.of_constr prf) ++ str " : " ++ pr_term state.env state.sigma s ++ str " <> " ++ pr_term state.env state.sigma t ++ str "]")); @@ -630,7 +622,7 @@ let join_path uf i j= min_path (down_path uf i [],down_path uf j []) let union state i1 i2 eq= - debug (fun () -> str "Linking " ++ pr_idx_term state.env state.sigma state.uf i1 ++ + debug_congruence (fun () -> str "Linking " ++ pr_idx_term state.env state.sigma state.uf i1 ++ str " and " ++ pr_idx_term state.env state.sigma state.uf i2 ++ str "."); let r1= get_representative state.uf i1 and r2= get_representative state.uf i2 in @@ -670,7 +662,7 @@ let union state i1 i2 eq= | _,_ -> () let merge eq state = (* merge and no-merge *) - debug + debug_congruence (fun () -> str "Merging " ++ pr_idx_term state.env state.sigma state.uf eq.lhs ++ str " and " ++ pr_idx_term state.env state.sigma state.uf eq.rhs ++ str "."); let uf=state.uf in @@ -683,7 +675,7 @@ let merge eq state = (* merge and no-merge *) union state j i (swap eq) let update t state = (* update 1 and 2 *) - debug + debug_congruence (fun () -> str "Updating term " ++ pr_idx_term state.env state.sigma state.uf t ++ str "."); let (i,j) as sign = signature state.uf t in let (u,v) = subterms state.uf t in @@ -745,7 +737,7 @@ let process_constructor_mark t i rep pac state = end let process_mark t m state = - debug + debug_congruence (fun () -> str "Processing mark for term " ++ pr_idx_term state.env state.sigma state.uf t ++ str "."); let i=find state.uf t in let rep=get_representative state.uf i in @@ -766,7 +758,7 @@ let check_disequalities state = if Int.equal (find uf dis.lhs) (find uf dis.rhs) then (str "Yes", Some dis) else (str "No", check_aux q) in - let _ = debug + let _ = debug_congruence (fun () -> str "Checking if " ++ pr_idx_term state.env state.sigma state.uf dis.lhs ++ str " = " ++ pr_idx_term state.env state.sigma state.uf dis.rhs ++ str " ... " ++ info) in ans @@ -953,7 +945,7 @@ let find_instances state = let pb_stack= init_pb_stack state in let res =ref [] in let _ = - debug (fun () -> str "Running E-matching algorithm ... "); + debug_congruence (fun () -> str "Running E-matching algorithm ... "); try while true do Control.check_for_interrupt (); @@ -964,7 +956,7 @@ let find_instances state = !res let rec execute first_run state = - debug (fun () -> str "Executing ... "); + debug_congruence (fun () -> str "Executing ... "); try while Control.check_for_interrupt (); @@ -974,7 +966,7 @@ let rec execute first_run state = None -> if not(Int.Set.is_empty state.pa_classes) then begin - debug (fun () -> str "First run was incomplete, completing ... "); + debug_congruence (fun () -> str "First run was incomplete, completing ... "); complete state; execute false state end @@ -989,12 +981,12 @@ let rec execute first_run state = end else begin - debug (fun () -> str "Out of instances ... "); + debug_congruence (fun () -> str "Out of instances ... "); None end else begin - debug (fun () -> str "Out of depth ... "); + debug_congruence (fun () -> str "Out of depth ... "); None end | Some dis -> Some diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index 3270f74479..047756deef 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -121,7 +121,7 @@ val term_equal : term -> term -> bool val constr_of_term : term -> constr -val debug : (unit -> Pp.t) -> unit +val debug_congruence : CDebug.t val forest : state -> forest diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index 53d8c5bdd9..e7e0822916 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -95,13 +95,13 @@ let pinject p c n a = p_rule=Inject(p,c,n,a)} let rec equal_proof env sigma uf i j= - debug (fun () -> str "equal_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); + debug_congruence (fun () -> str "equal_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); if i=j then prefl (term uf i) else let (li,lj)=join_path uf i j in ptrans (path_proof env sigma uf i li) (psym (path_proof env sigma uf j lj)) and edge_proof env sigma uf ((i,j),eq)= - debug (fun () -> str "edge_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); + debug_congruence (fun () -> str "edge_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); let pi=equal_proof env sigma uf i eq.lhs in let pj=psym (equal_proof env sigma uf j eq.rhs) in let pij= @@ -117,7 +117,7 @@ and edge_proof env sigma uf ((i,j),eq)= ptrans (ptrans pi pij) pj and constr_proof env sigma uf i ipac= - debug (fun () -> str "constr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20)); + debug_congruence (fun () -> str "constr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20)); let t=find_oldest_pac uf i ipac in let eq_it=equal_proof env sigma uf i t in if ipac.args=[] then @@ -130,20 +130,20 @@ and constr_proof env sigma uf i ipac= ptrans eq_it (pcongr p (prefl targ)) and path_proof env sigma uf i l= - debug (fun () -> str "path_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ str "{" ++ + debug_congruence (fun () -> str "path_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ str "{" ++ (prlist_with_sep (fun () -> str ",") (fun ((_,j),_) -> int j) l) ++ str "}"); match l with | [] -> prefl (term uf i) | x::q->ptrans (path_proof env sigma uf (snd (fst x)) q) (edge_proof env sigma uf x) and congr_proof env sigma uf i j= - debug (fun () -> str "congr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); + debug_congruence (fun () -> str "congr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); let (i1,i2) = subterms uf i and (j1,j2) = subterms uf j in pcongr (equal_proof env sigma uf i1 j1) (equal_proof env sigma uf i2 j2) and ind_proof env sigma uf i ipac j jpac= - debug (fun () -> str "ind_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); + debug_congruence (fun () -> str "ind_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); let p=equal_proof env sigma uf i j and p1=constr_proof env sigma uf i ipac and p2=constr_proof env sigma uf j jpac in diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 72f77508d8..341fde7b77 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -420,16 +420,16 @@ let cc_tactic depth additionnal_terms = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in Coqlib.(check_required_library logic_module_name); - let _ = debug (fun () -> Pp.str "Reading goal ...") in + let _ = debug_congruence (fun () -> Pp.str "Reading goal ...") in let state = make_prb gl depth additionnal_terms in - let _ = debug (fun () -> Pp.str "Problem built, solving ...") in + let _ = debug_congruence (fun () -> Pp.str "Problem built, solving ...") in let sol = execute true state in - let _ = debug (fun () -> Pp.str "Computation completed.") in + let _ = debug_congruence (fun () -> Pp.str "Computation completed.") in let uf=forest state in match sol with None -> Tacticals.New.tclFAIL 0 (str "congruence failed") | Some reason -> - debug (fun () -> Pp.str "Goal solved, generating proof ..."); + debug_congruence (fun () -> Pp.str "Goal solved, generating proof ..."); match reason with Discrimination (i,ipac,j,jpac) -> let p=build_proof (Tacmach.New.pf_env gl) sigma uf (`Discr (i,ipac,j,jpac)) in diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index d1403558ad..61966b60c0 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -14,7 +14,7 @@ open Pp open Lazy module NamedDecl = Context.Named.Declaration -let debug = false +let debug_zify = CDebug.create ~name:"zify" () (* The following [constr] are necessary for constructing the proof terms *) @@ -805,12 +805,11 @@ let pp_prf prf = let interp_prf evd inj source prf = let t, prf' = interp_prf evd inj source prf in - if debug then - Feedback.msg_debug + debug_zify (fun () -> Pp.( str "interp_prf " ++ gl_pr_constr inj.EInjT.inj ++ str " " ++ gl_pr_constr source ++ str " = " ++ gl_pr_constr t ++ str " by " - ++ gl_pr_constr prf' ++ str " from " ++ pp_prf prf ++ fnl ()); + ++ gl_pr_constr prf' ++ str " from " ++ pp_prf prf ++ fnl ())); (t, prf') let mkvar evd inj e = @@ -888,13 +887,12 @@ let app_unop evd src unop arg prf = let app_unop evd src unop arg prf = let res = app_unop evd src unop arg prf in - if debug then - Feedback.msg_debug + debug_zify (fun () -> Pp.( str "\napp_unop " ++ pp_prf evd unop.EUnOpT.inj1_t arg prf ++ str " => " - ++ pp_prf evd unop.EUnOpT.inj2_t src res); + ++ pp_prf evd unop.EUnOpT.inj2_t src res)); res let app_binop evd src binop arg1 prf1 arg2 prf2 = @@ -1066,8 +1064,7 @@ let match_operator env evd hd args (t, d) = let pp_trans_expr env evd e res = let {deriv = inj} = get_injection env evd e.typ in - if debug then - Feedback.msg_debug Pp.(str "\ntrans_expr " ++ pp_prf evd inj e.constr res); + debug_zify (fun () -> Pp.(str "\ntrans_expr " ++ pp_prf evd inj e.constr res)); res let declared_term env evd hd args = @@ -1187,7 +1184,7 @@ let trans_binrel evd src rop a1 prf1 a2 prf2 = let trans_binrel evd src rop a1 prf1 a2 prf2 = let res = trans_binrel evd src rop a1 prf1 a2 prf2 in - if debug then Feedback.msg_debug Pp.(str "\ntrans_binrel " ++ pp_prfp res); + debug_zify (fun () -> Pp.(str "\ntrans_binrel " ++ pp_prfp res)); res let mkprf t p = @@ -1199,11 +1196,10 @@ let mkprf t p = let mkprf t p = let t', p = mkprf t p in - if debug then - Feedback.msg_debug + debug_zify (fun () -> Pp.( str "mkprf " ++ gl_pr_constr t ++ str " <-> " ++ gl_pr_constr t' - ++ str " by " ++ gl_pr_constr p); + ++ str " by " ++ gl_pr_constr p)); (t', p) let trans_bin_prop op_constr op_iff t1 p1 t2 p2 = @@ -1221,7 +1217,7 @@ let trans_bin_prop op_constr op_iff t1 p1 t2 p2 = let trans_bin_prop op_constr op_iff t1 p1 t2 p2 = let prf = trans_bin_prop op_constr op_iff t1 p1 t2 p2 in - if debug then Feedback.msg_debug (pp_prfp prf); + debug_zify (fun () -> pp_prfp prf); prf let trans_un_prop op_constr op_iff p1 prf1 = @@ -1285,8 +1281,7 @@ let trans_hyps env evd l = [] l let trans_hyp h t0 prfp = - if debug then - Feedback.msg_debug Pp.(str "trans_hyp: " ++ pp_prfp prfp ++ fnl ()); + debug_zify (fun () -> Pp.(str "trans_hyp: " ++ pp_prfp prfp ++ fnl ())); match prfp with | IProof -> Tacticals.New.tclIDTAC (* Should detect before *) | CProof t' -> @@ -1313,8 +1308,7 @@ let trans_hyp h t0 prfp = (tclTHEN (Tactics.clear [h]) (Tactics.rename_hyp [(h', h)]))))) let trans_concl prfp = - if debug then - Feedback.msg_debug Pp.(str "trans_concl: " ++ pp_prfp prfp ++ fnl ()); + debug_zify (fun () -> Pp.(str "trans_concl: " ++ pp_prfp prfp ++ fnl ())); match prfp with | IProof -> Tacticals.New.tclIDTAC | CProof t -> diff --git a/plugins/nsatz/utile.ml b/plugins/nsatz/utile.ml index 1caa042db6..19bdcbac58 100644 --- a/plugins/nsatz/utile.ml +++ b/plugins/nsatz/utile.ml @@ -1,9 +1,9 @@ (* Printing *) let pr x = - if !Flags.debug then (Format.printf "@[%s@]" x; flush(stdout);)else () + if CDebug.(get_flag misc) then (Format.printf "@[%s@]" x; flush(stdout);)else () let prt0 s = () (* print_string s;flush(stdout)*) -let sinfo s = if !Flags.debug then Feedback.msg_debug (Pp.str s) -let info s = if !Flags.debug then Feedback.msg_debug (Pp.str (s ())) +let sinfo s = if CDebug.(get_flag misc) then Feedback.msg_debug (Pp.str s) +let info s = if CDebug.(get_flag misc) then Feedback.msg_debug (Pp.str (s ())) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 4d57abb465..41fd96ccb5 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -252,7 +252,7 @@ let interp_refine ist gl rc = in let sigma, c = Pretyping.understand_ltac flags (pf_env gl) (project gl) vars kind rc in (* ppdebug(lazy(str"sigma@interp_refine=" ++ pr_evar_map None sigma)); *) - ppdebug(lazy(str"c@interp_refine=" ++ Printer.pr_econstr_env (pf_env gl) sigma c)); + debug_ssr (fun () -> str"c@interp_refine=" ++ Printer.pr_econstr_env (pf_env gl) sigma c); (sigma, (sigma, c)) @@ -1207,7 +1207,7 @@ let gentac gen = Proofview.V82.tactic begin fun gl -> (* ppdebug(lazy(str"sigma@gentac=" ++ pr_evar_map None (project gl))); *) let conv, _, cl, c, clr, ucst,gl = pf_interp_gen_aux gl false gen in - ppdebug(lazy(str"c@gentac=" ++ pr_econstr_env (pf_env gl) (project gl) c)); + debug_ssr (fun () -> str"c@gentac=" ++ pr_econstr_env (pf_env gl) (project gl) c); let gl = pf_merge_uc ucst gl in if conv then tclTHEN (Proofview.V82.of_tactic (convert_concl ~check:true cl)) (old_cleartac clr) gl diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 582c45cde1..78a59abda9 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -126,17 +126,17 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = fun (oc, orig_clr, occ, c_gen) -> pfLIFT begin fun gl -> let orig_gl, concl, env = gl, pf_concl gl, pf_env gl in - ppdebug(lazy(Pp.str(if is_case then "==CASE==" else "==ELIM=="))); + debug_ssr (fun () -> (Pp.str(if is_case then "==CASE==" else "==ELIM=="))); let fire_subst gl t = Reductionops.nf_evar (project gl) t in let is_undef_pat = function | sigma, T t -> EConstr.isEvar sigma (EConstr.of_constr t) | _ -> false in let match_pat env p occ h cl = let sigma0 = project orig_gl in - ppdebug(lazy Pp.(str"matching: " ++ pr_occ occ ++ pp_pattern env p)); + debug_ssr (fun () -> Pp.(str"matching: " ++ pr_occ occ ++ pp_pattern env p)); let (c,ucst), cl = fill_occ_pattern ~raise_NoMatch:true env sigma0 (EConstr.Unsafe.to_constr cl) p occ h in - ppdebug(lazy Pp.(str" got: " ++ pr_constr_env env sigma0 c)); + debug_ssr (fun () -> Pp.(str" got: " ++ pr_constr_env env sigma0 c)); c, EConstr.of_constr cl, ucst in let mkTpat gl t = (* takes a term, refreshes it and makes a T pattern *) let n, t, _, ucst = pf_abs_evars orig_gl (project gl, fire_subst gl t) in @@ -212,10 +212,10 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let renamed_tys = Array.mapi (fun j (ctx, cty) -> let t = Term.it_mkProd_or_LetIn cty ctx in - ppdebug(lazy Pp.(str "Search" ++ Printer.pr_constr_env env (project gl) t)); + debug_ssr (fun () -> Pp.(str "Search" ++ Printer.pr_constr_env env (project gl) t)); let t = Arguments_renaming.rename_type t (GlobRef.ConstructRef((kn,i),j+1)) in - ppdebug(lazy Pp.(str"Done Search " ++ Printer.pr_constr_env env (project gl) t)); + debug_ssr (fun () -> Pp.(str"Done Search " ++ Printer.pr_constr_env env (project gl) t)); t) tys in @@ -241,8 +241,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = in let () = let sigma = project gl in - ppdebug(lazy Pp.(str"elim= "++ pr_econstr_pat env sigma elim)); - ppdebug(lazy Pp.(str"elimty= "++ pr_econstr_pat env sigma elimty)) in + debug_ssr (fun () -> Pp.(str"elim= "++ pr_econstr_pat env sigma elim)); + debug_ssr (fun () -> Pp.(str"elimty= "++ pr_econstr_pat env sigma elimty)) in let open EConstr in let inf_deps_r = match kind_of_type (project gl) elimty with | AtomicType (_, args) -> List.rev (Array.to_list args) @@ -301,7 +301,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = | Some (c, _, _,gl) -> Some(true, gl) | None -> None in first [try_c_last_arg;try_c_last_pattern] in - ppdebug(lazy Pp.(str"c_is_head_p= " ++ bool c_is_head_p)); + debug_ssr (fun () -> Pp.(str"c_is_head_p= " ++ bool c_is_head_p)); let gl, predty = pfe_type_of gl pred in (* Patterns for the inductive types indexes to be bound in pred are computed * looking at the ones provided by the user and the inferred ones looking at @@ -321,7 +321,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = loop (patterns @ [i, p, inf_t, occ]) (clr_t @ clr) (i+1) (deps, inf_deps) | [], c :: inf_deps -> - ppdebug(lazy Pp.(str"adding inf pattern " ++ pr_econstr_pat env (project gl) c)); + debug_ssr (fun () -> Pp.(str"adding inf pattern " ++ pr_econstr_pat env (project gl) c)); loop (patterns @ [i, mkTpat gl c, c, allocc]) clr (i+1) ([], inf_deps) | _::_, [] -> errorstrm Pp.(str "Too many dependent abstractions") in @@ -337,8 +337,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = loop [] orig_clr (List.length head_p+1) (List.rev deps, inf_deps_r) in head_p @ patterns, Util.List.uniquize clr, gl in - ppdebug(lazy Pp.(pp_concat (str"patterns=") (List.map pp_pat patterns))); - ppdebug(lazy Pp.(pp_concat (str"inf. patterns=") (List.map (pp_inf_pat gl) patterns))); + debug_ssr (fun () -> Pp.(pp_concat (str"patterns=") (List.map pp_pat patterns))); + debug_ssr (fun () -> Pp.(pp_concat (str"inf. patterns=") (List.map (pp_inf_pat gl) patterns))); (* Predicate generation, and (if necessary) tactic to generalize the * equation asked by the user *) let elim_pred, gen_eq_tac, clr, gl = @@ -348,7 +348,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let match_or_postpone (cl, gl, post) (h, p, inf_t, occ) = let p = unif_redex gl p inf_t in if is_undef_pat p then - let () = ppdebug(lazy Pp.(str"postponing " ++ pp_pattern env p)) in + let () = debug_ssr (fun () -> Pp.(str"postponing " ++ pp_pattern env p)) in cl, gl, post @ [h, p, inf_t, occ] else try let c, cl, ucst = match_pat env p occ h cl in @@ -420,8 +420,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = else gl, concl in concl, gen_eq_tac, clr, gl in let gl, pty = pf_e_type_of gl elim_pred in - ppdebug(lazy Pp.(str"elim_pred=" ++ pp_term gl elim_pred)); - ppdebug(lazy Pp.(str"elim_pred_ty=" ++ pp_term gl pty)); + debug_ssr (fun () -> Pp.(str"elim_pred=" ++ pp_term gl elim_pred)); + debug_ssr (fun () -> Pp.(str"elim_pred_ty=" ++ pp_term gl pty)); let gl = pf_unify_HO gl pred elim_pred in let elim = fire_subst gl elim in let gl = pf_resolve_typeclasses ~where:elim ~fail:false gl in diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 0008d31ffd..92a481dd18 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -76,7 +76,7 @@ let simpltac s = Proofview.Goal.enter (fun _ -> simpltac s) (** The "congr" tactic *) let interp_congrarg_at ist gl n rf ty m = - ppdebug(lazy Pp.(str"===interp_congrarg_at===")); + debug_ssr (fun () -> Pp.(str"===interp_congrarg_at===")); let congrn, _ = mkSsrRRef "nary_congruence" in let args1 = mkRnat n :: mkRHoles n @ [ty] in let args2 = mkRHoles (3 * n) in @@ -84,7 +84,7 @@ let interp_congrarg_at ist gl n rf ty m = if i + n > m then None else try let rt = mkRApp congrn (args1 @ mkRApp rf (mkRHoles i) :: args2) in - ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr_env (pf_env gl) (project gl) rt)); + debug_ssr (fun () -> Pp.(str"rt=" ++ Printer.pr_glob_constr_env (pf_env gl) (project gl) rt)); Some (interp_refine ist gl rt) with _ -> loop (i + 1) in loop 0 @@ -92,8 +92,8 @@ let interp_congrarg_at ist gl n rf ty m = let pattern_id = mk_internal_id "pattern value" let congrtac ((n, t), ty) ist gl = - ppdebug(lazy (Pp.str"===congr===")); - ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (Tacmach.pf_concl gl))); + debug_ssr (fun () -> (Pp.str"===congr===")); + debug_ssr (fun () -> Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (Tacmach.pf_concl gl))); let sigma, _ as it = interp_term (pf_env gl) (project gl) ist t in let gl = pf_merge_uc_of sigma gl in let _, f, _, _ucst = pf_abs_evars gl it in @@ -124,8 +124,8 @@ let newssrcongrtac arg ist = Proofview.Goal.enter_one ~__LOC__ begin fun _g -> (Ssrcommon.tacMK_SSR_CONST "ssr_congr_arrow") end >>= fun arr -> Proofview.V82.tactic begin fun gl -> - ppdebug(lazy Pp.(str"===newcongr===")); - ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (pf_concl gl))); + debug_ssr (fun () -> Pp.(str"===newcongr===")); + debug_ssr (fun () -> Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (pf_concl gl))); (* utils *) let fs gl t = Reductionops.nf_evar (project gl) t in let tclMATCH_GOAL (c, gl_c) proj t_ok t_fail gl = @@ -385,8 +385,8 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_ | Pretype_errors.PretypeError (env, sigma, te) -> raise (PRtype_error (Some (env, sigma, te))) | e when CErrors.noncritical e -> raise (PRtype_error None) in - ppdebug(lazy Pp.(str"pirrel_rewrite: proof term: " ++ pr_econstr_env env sigma proof)); - ppdebug(lazy Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty)); + debug_ssr (fun () -> Pp.(str"pirrel_rewrite: proof term: " ++ pr_econstr_env env sigma proof)); + debug_ssr (fun () -> Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty)); try Proofview.V82.of_tactic (refine_with ~first_goes_last:(not !ssroldreworder || under) ~with_evars:under (sigma, proof)) gl with e when CErrors.noncritical e -> @@ -435,12 +435,12 @@ let rwcltac ?under ?map_redex cl rdx dir sr = let sigma0 = Evd.set_universe_context sigma0 ucst in let rdxt = Retyping.get_type_of env (fst sr) rdx in (* ppdebug(lazy(str"sigma@rwcltac=" ++ pr_evar_map None (fst sr))); *) - ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr_env env sigma0 (snd sr))); + debug_ssr (fun () -> Pp.(str"r@rwcltac=" ++ pr_econstr_env env sigma0 (snd sr))); let cvtac, rwtac, sigma0 = if EConstr.Vars.closed0 sigma0 r' then let sigma, c, c_eq = fst sr, snd sr, Coqlib.(lib_ref "core.eq.type") in let sigma, c_ty = Typing.type_of env sigma c in - ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty)); + debug_ssr (fun () -> Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty)); let open EConstr in match kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with | AtomicType(e, a) when Ssrcommon.is_ind_ref sigma e c_eq -> @@ -521,7 +521,7 @@ let rwprocess_rule env dir rule = let t = if red = 1 then Tacred.hnf_constr env sigma t0 else Reductionops.whd_betaiotazeta env sigma t0 in - ppdebug(lazy Pp.(str"rewrule="++pr_econstr_pat env sigma t)); + debug_ssr (fun () -> Pp.(str"rewrule="++pr_econstr_pat env sigma t)); match EConstr.kind sigma t with | Prod (_, xt, at) -> let sigma = Evd.create_evar_defs sigma in diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index f2c7f495b3..bc46c23761 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -296,8 +296,8 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave = | Some id -> if pats = [] then Tacticals.New.tclIDTAC else let args = Array.of_list args in - ppdebug(lazy(str"specialized="++ pr_econstr_env (pf_env gl) (project gl) EConstr.(mkApp (mkVar id,args)))); - ppdebug(lazy(str"specialized_ty="++ pr_econstr_env (pf_env gl) (project gl) ct)); + debug_ssr (fun () -> str"specialized="++ pr_econstr_env (pf_env gl) (project gl) EConstr.(mkApp (mkVar id,args))); + debug_ssr (fun () -> str"specialized_ty="++ pr_econstr_env (pf_env gl) (project gl) ct); Tacticals.New.tclTHENS (basecuttac "ssr_have" ct) [Tactics.apply EConstr.(mkApp (mkVar id,args)); Tacticals.New.tclIDTAC] in "ssr_have", @@ -395,7 +395,7 @@ let intro_lock ipats = Array.length args = 3 && is_app_evar sigma args.(2) -> protect_subgoal env sigma hd args | _ -> - ppdebug(lazy Pp.(str"under: stop:" ++ pr_econstr_env env sigma t)); + debug_ssr (fun () -> Pp.(str"under: stop:" ++ pr_econstr_env env sigma t)); Proofview.tclUNIT () end) @@ -468,13 +468,13 @@ let undertac ?(pad_intro = false) ist ipats ((dir,_),_ as rule) hint = | Some l -> [IPatCase(Regular [l;[]])] in let map_redex env evar_map ~before:_ ~after:t = - ppdebug(lazy Pp.(str"under vars: " ++ prlist Names.Name.print varnames)); + debug_ssr (fun () -> Pp.(str"under vars: " ++ prlist Names.Name.print varnames)); let evar_map, ty = Typing.type_of env evar_map t in let new_t = (* pretty-rename the bound variables *) try begin match EConstr.destApp evar_map t with (f, ar) -> let lam = Array.last ar in - ppdebug(lazy Pp.(str"under: mapping:" ++ + debug_ssr(fun () -> Pp.(str"under: mapping:" ++ pr_econstr_env env evar_map lam)); let new_lam = pretty_rename evar_map lam varnames in let new_ar, len1 = Array.copy ar, pred (Array.length ar) in @@ -482,10 +482,10 @@ let undertac ?(pad_intro = false) ist ipats ((dir,_),_ as rule) hint = EConstr.mkApp (f, new_ar) end with | DestKO -> - ppdebug(lazy Pp.(str"under: cannot pretty-rename bound variables with destApp")); + debug_ssr (fun () -> Pp.(str"under: cannot pretty-rename bound variables with destApp")); t in - ppdebug(lazy Pp.(str"under: to:" ++ pr_econstr_env env evar_map new_t)); + debug_ssr (fun () -> Pp.(str"under: to:" ++ pr_econstr_env env evar_map new_t)); evar_map, new_t in let undertacs = diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 1e940b5ad3..f8abed5482 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -324,7 +324,7 @@ end `tac`, where k is the size of `seeds` *) let tclSEED_SUBGOALS seeds tac = tclTHENin tac (fun i n -> - Ssrprinters.ppdebug (lazy Pp.(str"seeding")); + Ssrprinters.debug_ssr (fun () -> Pp.(str"seeding")); (* eg [case: (H _ : nat)] generates 3 goals: - 1 for _ - 2 for the nat constructors *) @@ -416,11 +416,11 @@ let tclMK_ABSTRACT_VARS ids = (* Debugging *) let tclLOG p t = tclUNIT () >>= begin fun () -> - Ssrprinters.ppdebug (lazy Pp.(str "exec: " ++ pr_ipatop p)); + Ssrprinters.debug_ssr (fun () -> Pp.(str "exec: " ++ pr_ipatop p)); tclUNIT () end <*> Goal.enter begin fun g -> - Ssrprinters.ppdebug (lazy Pp.(str" on state:" ++ spc () ++ + Ssrprinters.debug_ssr (fun () -> Pp.(str" on state:" ++ spc () ++ isPRINT g ++ str" goal:" ++ spc () ++ Printer.pr_goal (Goal.print g))); tclUNIT () @@ -429,7 +429,7 @@ let tclLOG p t = t p >>= fun ret -> Goal.enter begin fun g -> - Ssrprinters.ppdebug (lazy Pp.(str "done: " ++ isPRINT g)); + Ssrprinters.debug_ssr (fun () -> Pp.(str "done: " ++ isPRINT g)); tclUNIT () end >>= fun () -> tclUNIT ret @@ -579,10 +579,10 @@ let tclCompileIPats l = elab l ;; let tclCompileIPats l = - Ssrprinters.ppdebug (lazy Pp.(str "tclCompileIPats input: " ++ + Ssrprinters.debug_ssr (fun () -> Pp.(str "tclCompileIPats input: " ++ prlist_with_sep spc Ssrprinters.pr_ipat l)); let ops = tclCompileIPats l in - Ssrprinters.ppdebug (lazy Pp.(str "tclCompileIPats output: " ++ + Ssrprinters.debug_ssr (fun () -> Pp.(str "tclCompileIPats output: " ++ prlist_with_sep spc pr_ipatop ops)); ops @@ -597,11 +597,11 @@ let main ?eqtac ~first_case_is_dispatch iops = end (* }}} *) let tclIPAT_EQ eqtac ip = - Ssrprinters.ppdebug (lazy Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip)); + Ssrprinters.debug_ssr (fun () -> Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip)); IpatMachine.(main ~eqtac ~first_case_is_dispatch:true (tclCompileIPats ip)) let tclIPATssr ip = - Ssrprinters.ppdebug (lazy Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip)); + Ssrprinters.debug_ssr (fun () -> Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip)); IpatMachine.(main ~first_case_is_dispatch:true (tclCompileIPats ip)) let tclCompileIPats = IpatMachine.tclCompileIPats diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index 6ed68094dc..434568b554 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -15,7 +15,6 @@ open Names open Printer open Tacmach -open Ssrmatching_plugin open Ssrast let pr_spc () = str " " @@ -121,15 +120,4 @@ and pr_block = function (Prefix id) -> str"^" ++ Id.print id | (SuffixId id) -> str"^~" ++ Id.print id | (SuffixNum n) -> str"^~" ++ int n -(* 0 cost pp function. Active only if Debug Ssreflect is Set *) -let ppdebug_ref = ref (fun _ -> ()) -let ssr_pp s = Feedback.msg_debug (str"SSR: "++Lazy.force s) -let () = - Goptions.(declare_bool_option - { optkey = ["Debug";"Ssreflect"]; - optdepr = false; - optread = (fun _ -> !ppdebug_ref == ssr_pp); - optwrite = (fun b -> - Ssrmatching.debug b; - if b then ppdebug_ref := ssr_pp else ppdebug_ref := fun _ -> ()) }) -let ppdebug s = !ppdebug_ref s +let debug_ssr = CDebug.create ~name:"ssreflect" () diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli index 21fb28038a..994577a0c9 100644 --- a/plugins/ssr/ssrprinters.mli +++ b/plugins/ssr/ssrprinters.mli @@ -51,5 +51,4 @@ val pr_guarded : val pr_occ : ssrocc -> Pp.t -val ppdebug : Pp.t Lazy.t -> unit - +val debug_ssr : CDebug.t diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 97926753f5..b3a9e71a3f 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -194,17 +194,17 @@ let mkGApp f args = let interp_glob ist glob = Goal.enter_one ~__LOC__ begin fun goal -> let env = Goal.env goal in let sigma = Goal.sigma goal in - Ssrprinters.ppdebug (lazy + Ssrprinters.debug_ssr (fun () -> Pp.(str"interp-in: " ++ Printer.pr_glob_constr_env env sigma glob)); try let sigma,term = Tacinterp.interp_open_constr ist env sigma (glob,None) in - Ssrprinters.ppdebug (lazy + Ssrprinters.debug_ssr (fun () -> Pp.(str"interp-out: " ++ Printer.pr_econstr_env env sigma term)); tclUNIT (env,sigma,term) with e -> (* XXX this is another catch all! *) let e, info = Exninfo.capture e in - Ssrprinters.ppdebug (lazy + Ssrprinters.debug_ssr (fun () -> Pp.(str"interp-err: " ++ Printer.pr_glob_constr_env env sigma glob)); tclZERO ~info e end @@ -217,7 +217,7 @@ end let tclKeepOpenConstr (_env, sigma, t) = Unsafe.tclEVARS sigma <*> tclUNIT t let tclADD_CLEAR_IF_ID (env, ist, t) x = - Ssrprinters.ppdebug (lazy + Ssrprinters.debug_ssr (fun () -> Pp.(str"tclADD_CLEAR_IF_ID: " ++ Printer.pr_econstr_env env ist t)); let hd, args = EConstr.decompose_app ist t in match EConstr.kind ist hd with @@ -269,11 +269,11 @@ let interp_view ~clear_if_id ist v p = let p_id = DAst.make p_id in match DAst.get v with | Glob_term.GApp (hd, rargs) when is_specialize hd -> - Ssrprinters.ppdebug (lazy Pp.(str "specialize")); + Ssrprinters.debug_ssr (fun () -> Pp.(str "specialize")); interp_glob ist (mkGApp p_id rargs) >>= tclKeepOpenConstr >>= tclPAIR [] | _ -> - Ssrprinters.ppdebug (lazy Pp.(str "view")); + Ssrprinters.debug_ssr (fun () -> Pp.(str "view")); (* We find out how to build (v p) eventually using an adaptor *) let adaptors = AdaptorDb.(get Forward) in Proofview.tclORELSE @@ -324,7 +324,7 @@ Goal.enter_one ~__LOC__ begin fun g -> let rigid = rigid_of und0 in let n, p, to_prune, _ucst = pf_abs_evars2 s0 rigid (sigma, p) in let p = if simple_types then pf_abs_cterm s0 n p else p in - Ssrprinters.ppdebug (lazy Pp.(str"view@finalized: " ++ + Ssrprinters.debug_ssr (fun () -> Pp.(str"view@finalized: " ++ Printer.pr_econstr_env env sigma p)); let sigma = List.fold_left Evd.remove sigma to_prune in Unsafe.tclEVARS sigma <*> @@ -349,26 +349,26 @@ let rec apply_all_views_aux ~clear_if_id vs finalization conclusion s0 = pose_proof name p <*> conclusion ~to_clear:name) <*> tclUNIT false) | v :: vs -> - Ssrprinters.ppdebug (lazy Pp.(str"piling...")); + Ssrprinters.debug_ssr (fun () -> Pp.(str"piling...")); is_tac_in_term ~extra_scope:"ssripat" v >>= function | `Term v -> - Ssrprinters.ppdebug (lazy Pp.(str"..a term")); + Ssrprinters.debug_ssr (fun () -> Pp.(str"..a term")); pile_up_view ~clear_if_id v <*> apply_all_views_aux ~clear_if_id vs finalization conclusion s0 | `Tac tac -> - Ssrprinters.ppdebug (lazy Pp.(str"..a tactic")); + Ssrprinters.debug_ssr (fun () -> Pp.(str"..a tactic")); finalization s0 (fun name p -> (match p with | None -> tclUNIT () | Some p -> pose_proof name p) <*> Tacinterp.eval_tactic tac <*> if vs = [] then begin - Ssrprinters.ppdebug (lazy Pp.(str"..was the last view")); + Ssrprinters.debug_ssr (fun () -> Pp.(str"..was the last view")); conclusion ~to_clear:name <*> tclUNIT true end else Tactics.clear name <*> tclINDEPENDENTL begin - Ssrprinters.ppdebug (lazy Pp.(str"..was NOT the last view")); + Ssrprinters.debug_ssr (fun () -> Pp.(str"..was NOT the last view")); Ssrcommon.tacSIGMA >>= apply_all_views_aux ~clear_if_id vs finalization conclusion end >>= reduce_or) diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 7930c3d634..02fb347d08 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -201,10 +201,7 @@ let cofixp_reducible flgs _ stk = else false -let get_debug_cbv = Goptions.declare_bool_option_and_ref - ~depr:false - ~value:false - ~key:["Debug";"Cbv"] +let debug_cbv = CDebug.create ~name:"Cbv" () (* Reduction of primitives *) @@ -525,7 +522,7 @@ and norm_head_ref k info env stack normt t = if red_set_ref info.reds normt then match cbv_value_cache info normt with | Declarations.Def body -> - if get_debug_cbv () then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt); + debug_cbv (fun () -> Pp.(str "Unfolding " ++ debug_pr_key normt)); strip_appl (shift_value k body) stack | Declarations.Primitive op -> let c = match normt with @@ -534,11 +531,11 @@ and norm_head_ref k info env stack normt t = in (PRIMITIVE(op,c,[||]),stack) | Declarations.OpaqueDef _ | Declarations.Undef _ -> - if get_debug_cbv () then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); + debug_cbv (fun () -> Pp.(str "Not unfolding " ++ debug_pr_key normt)); (VAL(0,make_constr_ref k normt t),stack) else begin - if get_debug_cbv () then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); + debug_cbv (fun () -> Pp.(str "Not unfolding " ++ debug_pr_key normt)); (VAL(0,make_constr_ref k normt t),stack) end diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 990e84e5a7..e1d6fff3e4 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -47,17 +47,9 @@ let default_flags env = let ts = default_transparent_state env in default_flags_of ts -let debug_unification = - Goptions.declare_bool_option_and_ref - ~depr:false - ~key:["Debug";"Unification"] - ~value:false - -let debug_ho_unification = - Goptions.declare_bool_option_and_ref - ~depr:false - ~key:["Debug";"HO";"Unification"] - ~value:false +let debug_unification = CDebug.create ~name:"unification" () + +let debug_ho_unification = CDebug.create ~name:"ho-unification" () (*******************************************) (* Functions to deal with impossible cases *) @@ -808,9 +800,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty in let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in (* Evar must be undefined since we have flushed evars *) - let () = if debug_unification () then - let open Pp in - Feedback.msg_debug (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in + let () = debug_unification (fun () -> Pp.(v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ()))) in match (flex_kind_of_term flags env evd term1 sk1, flex_kind_of_term flags env evd term2 sk2) with | Flexible (sp1,al1), Flexible (sp2,al2) -> @@ -1288,17 +1278,17 @@ let apply_on_subterm env evd fixed f test c t = (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) applyrec acc t else - (if debug_ho_unification () then - Feedback.msg_debug Pp.(str"Testing " ++ prc env !evdref c ++ str" against " ++ prc env !evdref t); + (debug_ho_unification (fun () -> + Pp.(str"Testing " ++ prc env !evdref c ++ str" against " ++ prc env !evdref t)); let b, evd = try test env !evdref k c t with e when CErrors.noncritical e -> assert false in - if b then (if debug_ho_unification () then Feedback.msg_debug (Pp.str "succeeded"); + if b then (debug_ho_unification (fun () -> Pp.str "succeeded"); let evd', fixed, t' = f !evdref !fixedref k t in fixedref := fixed; evdref := evd'; t') else ( - if debug_ho_unification () then Feedback.msg_debug (Pp.str "failed"); + debug_ho_unification (fun () -> Pp.str "failed"); map_constr_with_binders_left_to_right env !evdref (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) applyrec acc t)) @@ -1404,9 +1394,9 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = let env_evar = evar_filtered_env env_rhs evi in let sign = named_context_val env_evar in let ctxt = evar_filtered_context evi in - if debug_ho_unification () then - (Feedback.msg_debug Pp.(str"env rhs: " ++ Termops.Internal.print_env env_rhs); - Feedback.msg_debug Pp.(str"env evars: " ++ Termops.Internal.print_env env_evar)); + debug_ho_unification (fun () -> + Pp.(str"env rhs: " ++ Termops.Internal.print_env env_rhs ++ fnl () ++ + str"env evars: " ++ Termops.Internal.print_env env_evar)); let args = List.map (nf_evar evd) args in let argsubst = List.map2 (fun decl c -> (NamedDecl.get_id decl, c)) ctxt args in let instance = evar_identity_subst evi in @@ -1439,17 +1429,17 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = let rec set_holes env_rhs evd fixed rhs = function | (id,idty,c,cty,evsref,filter,occs)::subst -> let c = nf_evar evd c in - if debug_ho_unification () then - Feedback.msg_debug Pp.(str"set holes for: " ++ + debug_ho_unification (fun () -> + Pp.(str"set holes for: " ++ prc env_rhs evd (mkVar id.binder_name) ++ spc () ++ prc env_rhs evd c ++ str" in " ++ - prc env_rhs evd rhs); + prc env_rhs evd rhs)); let occ = ref 1 in let set_var evd fixed k inst = let oc = !occ in - if debug_ho_unification () then - (Feedback.msg_debug Pp.(str"Found one occurrence"); - Feedback.msg_debug Pp.(str"cty: " ++ prc env_rhs evd c)); + debug_ho_unification (fun () -> + Pp.(str"Found one occurrence" ++ fnl () ++ + str"cty: " ++ prc env_rhs evd c)); incr occ; match occs with | AtOccurrences occs -> @@ -1458,10 +1448,10 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = | Unspecified prefer_abstraction -> let evd, fixed, evty = set_holes env_rhs evd fixed cty subst in let evty = nf_evar evd evty in - if debug_ho_unification () then - Feedback.msg_debug Pp.(str"abstracting one occurrence " ++ prc env_rhs evd inst ++ - str" of type: " ++ prc env_evar evd evty ++ - str " for " ++ prc env_rhs evd c); + debug_ho_unification (fun () -> + Pp.(str"abstracting one occurrence " ++ prc env_rhs evd inst ++ + str" of type: " ++ prc env_evar evd evty ++ + str " for " ++ prc env_rhs evd c)); let instance = Filter.filter_list filter instance in (* Allow any type lower than the variable's type as the abstracted subterm might have a smaller type, which could be @@ -1477,8 +1467,8 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = evd, fixed, mkEvar (evk, instance) in let evd, fixed, rhs' = apply_on_subterm env_rhs evd fixed set_var test c rhs in - if debug_ho_unification () then - Feedback.msg_debug Pp.(str"abstracted: " ++ prc env_rhs evd rhs'); + debug_ho_unification (fun () -> + Pp.(str"abstracted: " ++ prc env_rhs evd rhs')); let () = check_selected_occs env_rhs evd c !occ occs in let env_rhs' = push_named (NamedDecl.LocalAssum (id,idty)) env_rhs in set_holes env_rhs' evd fixed rhs' subst @@ -1491,9 +1481,9 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = (* Thin evars making the term typable in env_evar *) let evd, rhs' = thin_evars env_evar evd ctxt rhs' in (* We instantiate the evars of which the value is forced by typing *) - if debug_ho_unification () then - (Feedback.msg_debug Pp.(str"solve_evars on: " ++ prc env_evar evd rhs'); - Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd)); + debug_ho_unification (fun () -> + Pp.(str"solve_evars on: " ++ prc env_evar evd rhs' ++ fnl () ++ + str"evars: " ++ pr_evar_map (Some 0) env_evar evd)); let evd,rhs' = try !solve_evars env_evar evd rhs' with e when Pretype_errors.precatchable_exception e -> @@ -1501,18 +1491,18 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = raise (TypingFailed evd) in let rhs' = nf_evar evd rhs' in (* We instantiate the evars of which the value is forced by typing *) - if debug_ho_unification () then - (Feedback.msg_debug Pp.(str"after solve_evars: " ++ prc env_evar evd rhs'); - Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd)); + debug_ho_unification (fun () -> + Pp.(str"after solve_evars: " ++ prc env_evar evd rhs' ++ fnl () ++ + str"evars: " ++ pr_evar_map (Some 0) env_evar evd)); let rec abstract_free_holes evd = function | (id,idty,c,cty,evsref,_,_)::l -> let id = id.binder_name in let c = nf_evar evd c in - if debug_ho_unification () then - Feedback.msg_debug Pp.(str"abstracting: " ++ - prc env_rhs evd (mkVar id) ++ spc () ++ - prc env_rhs evd c); + debug_ho_unification (fun () -> + Pp.(str"abstracting: " ++ + prc env_rhs evd (mkVar id) ++ spc () ++ + prc env_rhs evd c)); let rec force_instantiation evd = function | (evk,evty,inst,abstract)::evs -> let evk = Option.default evk (Evarutil.advance evd evk) in @@ -1541,14 +1531,14 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = with IllTypedInstance _ (* from instantiate_evar *) | TypingFailed _ -> user_err (Pp.str "Cannot find an instance.") else - ((if debug_ho_unification () then + ((debug_ho_unification (fun () -> let evi = Evd.find evd evk in let env = Evd.evar_env env_rhs evi in - Feedback.msg_debug Pp.(str"evar is defined: " ++ + Pp.(str"evar is defined: " ++ int (Evar.repr evk) ++ spc () ++ prc env evd (match evar_body evi with Evar_defined c -> c | Evar_empty -> assert false))); - evd) + evd)) in force_instantiation evd evs | [] -> abstract_free_holes evd l in force_instantiation evd !evsref @@ -1556,27 +1546,27 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = if Evd.is_defined evd evk then (* Can happen due to dependencies: instantiating evars in the arguments of evk might instantiate evk itself. *) - (if debug_ho_unification () then + (debug_ho_unification (fun () -> begin let evi = Evd.find evd evk in let evenv = evar_env env_rhs evi in let body = match evar_body evi with Evar_empty -> assert false | Evar_defined c -> c in - Feedback.msg_debug Pp.(str"evar was defined already as: " ++ prc evenv evd body) - end; + Pp.(str"evar was defined already as: " ++ prc evenv evd body) + end); evd) else try let evi = Evd.find_undefined evd evk in let evenv = evar_env env_rhs evi in let rhs' = nf_evar evd rhs' in - if debug_ho_unification () then - Feedback.msg_debug Pp.(str"abstracted type before second solve_evars: " ++ - prc evenv evd rhs'); + debug_ho_unification (fun () -> + Pp.(str"abstracted type before second solve_evars: " ++ + prc evenv evd rhs')); (* solve_evars is not commuting with nf_evar, because restricting an evar might provide a more specific type. *) let evd, _ = !solve_evars evenv evd rhs' in - if debug_ho_unification () then - Feedback.msg_debug Pp.(str"abstracted type: " ++ prc evenv evd (nf_evar evd rhs')); + debug_ho_unification (fun () -> + Pp.(str"abstracted type: " ++ prc evenv evd (nf_evar evd rhs'))); let flags = default_flags_of TransparentState.full in Evarsolve.instantiate_evar evar_unify flags env_rhs evd evk rhs' with IllTypedInstance _ -> raise (TypingFailed evd) @@ -1629,11 +1619,10 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = let t2 = apprec_nohdbeta flags env evd (whd_head_evar evd t2) in let (term1,l1 as appr1) = try destApp evd t1 with DestKO -> (t1, [||]) in let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in - let () = if debug_unification () then - let open Pp in - Feedback.msg_debug (v 0 (str "Heuristic:" ++ spc () ++ + let () = debug_unification (fun () -> + Pp.(v 0 (str "Heuristic:" ++ spc () ++ Termops.Internal.print_constr_env env evd t1 ++ cut () ++ - Termops.Internal.print_constr_env env evd t2 ++ cut ())) in + Termops.Internal.print_constr_env env evd t2 ++ cut ()))) in let app_empty = Array.is_empty l1 && Array.is_empty l2 in match EConstr.kind evd term1, EConstr.kind evd term2 with | Evar (evk1,args1), (Rel _|Var _) when app_empty diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 92e412a537..28621aa92e 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -469,15 +469,15 @@ let start_profiler_linux profile_fn = Unix.stdin dev_null dev_null in (* doesn't seem to be a way to test whether process creation succeeded *) - if !Flags.debug then - Feedback.msg_debug (Pp.str (Format.sprintf "Native compute profiler started, pid = %d, output to: %s" profiler_pid profile_fn)); + debug_native_compiler (fun () -> + Pp.str (Format.sprintf "Native compute profiler started, pid = %d, output to: %s" profiler_pid profile_fn)); Some profiler_pid (* kill profiler via SIGINT *) let stop_profiler_linux m_pid = match m_pid with | Some pid -> ( - let _ = if !Flags.debug then Feedback.msg_debug (Pp.str "Stopping native code profiler") in + let _ = debug_native_compiler (fun () -> Pp.str "Stopping native code profiler") in try Unix.kill pid Sys.sigint; let _ = Unix.waitpid [] pid in () diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 54a47a252d..4083d3bc23 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -686,11 +686,7 @@ module CredNative = RedNative(CNativeEntries) contract_* in any case . *) -let debug_RAKAM = - Goptions.declare_bool_option_and_ref - ~depr:false - ~key:["Debug";"RAKAM"] - ~value:false +let debug_RAKAM = CDebug.create ~name:"RAKAM" () let apply_branch env sigma (ind, i) args (ci, u, pms, iv, r, lf) = let args = Stack.tail ci.ci_npar args in @@ -709,18 +705,18 @@ let apply_branch env sigma (ind, i) args (ci, u, pms, iv, r, lf) = let rec whd_state_gen flags env sigma = let open Context.Named.Declaration in let rec whrec (x, stack) : state = - let () = if debug_RAKAM () then + let () = let open Pp in let pr c = Termops.Internal.print_constr_env env sigma c in - Feedback.msg_debug + debug_RAKAM (fun () -> (h (str "<<" ++ pr x ++ str "|" ++ cut () ++ Stack.pr pr stack ++ - str ">>")) + str ">>"))) in let c0 = EConstr.kind sigma x in let fold () = - let () = if debug_RAKAM () then - let open Pp in Feedback.msg_debug (str "<><><><><>") in + let () = debug_RAKAM (fun () -> + let open Pp in str "<><><><><>") in ((EConstr.of_kind c0, stack)) in match c0 with diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 41d16f1c3c..09bcc860d0 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -19,7 +19,7 @@ open Environ exception Elimconst -val debug_RAKAM : unit -> bool +val debug_RAKAM : CDebug.t module CredNative : Primred.RedNative with type elem = EConstr.t and type args = EConstr.t array and type evd = Evd.evar_map diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 83e46e3295..df0f49a033 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -49,11 +49,7 @@ let is_keyed_unification = ~key:["Keyed";"Unification"] ~value:false -let debug_unification = - Goptions.declare_bool_option_and_ref - ~depr:false - ~key:["Debug";"Tactic";"Unification"] - ~value:false +let debug_tactic_unification = CDebug.create ~name:"tactic-unification" () (** Making this unification algorithm correct w.r.t. the evar-map abstraction breaks too much stuff. So we redefine incorrect functions here. *) @@ -713,8 +709,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e let cM = Evarutil.whd_head_evar sigma curm and cN = Evarutil.whd_head_evar sigma curn in let () = - if debug_unification () then - Feedback.msg_debug ( + debug_tactic_unification (fun () -> Termops.Internal.print_constr_env curenv sigma cM ++ str" ~= " ++ Termops.Internal.print_constr_env curenv sigma cN) in @@ -1138,7 +1133,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e else error_cannot_unify (fst curenvnb) sigma (cM,cN) in - if debug_unification () then Feedback.msg_debug (str "Starting unification"); + debug_tactic_unification (fun () -> str "Starting unification"); let opt = { at_top = conv_at_top; with_types = false; with_cs = true } in try let res = @@ -1165,11 +1160,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e let a = match res with | Some sigma -> sigma, ms, es | None -> unirec_rec (env,0) cv_pb opt subst (fst m) (fst n) in - if debug_unification () then Feedback.msg_debug (str "Leaving unification with success"); + debug_tactic_unification (fun () -> str "Leaving unification with success"); a with e -> let e = Exninfo.capture e in - if debug_unification () then Feedback.msg_debug (str "Leaving unification with failure"); + debug_tactic_unification (fun () -> str "Leaving unification with failure"); Exninfo.iraise e let unify_0 env sigma pb flags c1 c2 = diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 4c4c26f47e..dd80ff21aa 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -13,7 +13,7 @@ open Pp open Util let stm_pr_err pp = Format.eprintf "%s] @[%a@]\n%!" (Spawned.process_id ()) Pp.pp_with pp -let stm_prerr_endline s = if !Flags.debug then begin stm_pr_err (str s) end else () +let stm_prerr_endline s = if CDebug.(get_flag misc) then begin stm_pr_err (str s) end else () type cancel_switch = bool ref let async_proofs_flags_for_workers = ref [] diff --git a/stm/spawned.ml b/stm/spawned.ml index 5cc8be78f5..ee9c8e9942 100644 --- a/stm/spawned.ml +++ b/stm/spawned.ml @@ -11,7 +11,7 @@ open Spawn let pr_err s = Printf.eprintf "(Spawned,%d) %s\n%!" (Unix.getpid ()) s -let prerr_endline s = if !Flags.debug then begin pr_err s end else () +let prerr_endline s = if CDebug.(get_flag misc) then begin pr_err s end else () type chandescr = AnonPipe | Socket of string * int * int diff --git a/stm/stm.ml b/stm/stm.ml index 7de109e596..5ed6adbd63 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -9,7 +9,7 @@ (************************************************************************) (* enable in case of stm problems *) -(* let stm_debug () = !Flags.debug *) +(* let stm_debug () = CDebug.(get_flag misc) *) let stm_debug = ref false let stm_pr_err s = Format.eprintf "%s] %s\n%!" (Spawned.process_id ()) s @@ -18,7 +18,7 @@ let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n%!" (Spawned.process_id ()) Pp.p let stm_prerr_endline s = if !stm_debug then begin stm_pr_err (s ()) end else () let stm_pperr_endline s = if !stm_debug then begin stm_pp_err (s ()) end else () -let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else () +let stm_prerr_debug s = if CDebug.(get_flag misc) then begin stm_pr_err (s ()) end else () open Pp open CErrors @@ -785,7 +785,7 @@ end = struct (* {{{ *) end let print ?(now=false) () = - if !Flags.debug then NB.command ~now (print_dag !vcs) + if CDebug.(get_flag misc) then NB.command ~now (print_dag !vcs) let backup () = !vcs let restore v = vcs := v @@ -1533,7 +1533,7 @@ end = struct (* {{{ *) when is_tac expr && Vernacstate.Stm.same_env o n -> (* A pure tactic *) Some (id, `ProofOnly (prev, Vernacstate.Stm.pstate n)) | Some _, Some s -> - if !Flags.debug then msg_debug (Pp.str "STM: sending back a fat state"); + if CDebug.(get_flag misc) then msg_debug (Pp.str "STM: sending back a fat state"); Some (id, `Full s) | _, Some s -> Some (id, `Full s) in let rec aux seen = function diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml index 56d88e6bd6..8be73ca028 100644 --- a/sysinit/coqargs.ml +++ b/sysinit/coqargs.ml @@ -22,14 +22,6 @@ let error_missing_arg s = exit 1 (******************************************************************************) -(* Imperative effects! This must be fixed at some point. *) -(******************************************************************************) - -let set_debug () = - let () = Exninfo.record_backtrace true in - Flags.debug := true - -(******************************************************************************) type native_compiler = Coq_config.native_compiler = NativeOff | NativeOn of { ondemand : bool } @@ -168,6 +160,9 @@ let add_load_vernacular opts verb s = let add_set_option opts opt_name value = { opts with pre = { opts.pre with injections = OptionInjection (opt_name, value) :: opts.pre.injections }} +let add_set_debug opts flags = + add_set_option opts ["Debug"] (OptionAppend flags) + (** Options for proof general *) let set_emacs opts = let opts = add_set_option opts Printer.print_goal_tag_opt_name (OptionSet None) in @@ -382,10 +377,15 @@ let parse_args ~usage ~init arglist : t * string list = (* Options with zero arg *) |"-test-mode" -> Vernacinterp.test_mode := true; oval |"-beautify" -> Flags.beautify := true; oval - |"-bt" -> Exninfo.record_backtrace true; oval + |"-bt" -> add_set_debug oval "backtrace" |"-config"|"--config" -> set_query oval PrintConfig - |"-debug" -> set_debug (); oval - |"-xml-debug" -> Flags.xml_debug := true; set_debug (); oval + + |"-debug" -> add_set_debug oval "all" + |"-d" | "-D" -> add_set_debug oval (next()) + + (* -xml-debug implies -debug. TODO don't be imperative here. *) + |"-xml-debug" -> Flags.xml_debug := true; add_set_debug oval "all" + |"-diffs" -> add_set_option oval Proof_diffs.opt_name @@ OptionSet (Some (next ())) |"-emacs" -> set_emacs oval diff --git a/tactics/cbn.ml b/tactics/cbn.ml index 6fb6cff04f..167f7d4026 100644 --- a/tactics/cbn.ml +++ b/tactics/cbn.ml @@ -562,19 +562,18 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = let open Context.Named.Declaration in let open ReductionBehaviour in let rec whrec cst_l (x, stack) = - let () = if debug_RAKAM () then + let () = debug_RAKAM (fun () -> let open Pp in let pr c = Termops.Internal.print_constr_env env sigma c in - Feedback.msg_debug (h (str "<<" ++ pr x ++ str "|" ++ cut () ++ Cst_stack.pr env sigma cst_l ++ str "|" ++ cut () ++ Stack.pr pr stack ++ - str ">>")) + str ">>"))) in let c0 = EConstr.kind sigma x in let fold () = - let () = if debug_RAKAM () then - let open Pp in Feedback.msg_debug (str "<><><><><>") in + let () = debug_RAKAM (fun () -> + Pp.(str "<><><><><>")) in ((EConstr.of_kind c0, stack),cst_l) in match c0 with diff --git a/test-suite/output/DebugFlags.out b/test-suite/output/DebugFlags.out new file mode 100644 index 0000000000..0385413937 --- /dev/null +++ b/test-suite/output/DebugFlags.out @@ -0,0 +1,44 @@ +File "stdin", line 1, characters 0-16: +Warning: There is no debug flag "cbn". [unknown-debug-flag,option] +Debug: [RAKAM] <<forall A : Type, A -> A -> Prop|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<forall A : Type, A -> A -> Prop|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<?A -> ?A -> Prop|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<?A -> ?A -> Prop|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> Prop|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> Prop|>> +Debug: [RAKAM] <><><><><> +2 + 3 = 0 + : Prop diff --git a/test-suite/output/DebugFlags.v b/test-suite/output/DebugFlags.v new file mode 100644 index 0000000000..32c0f2d24b --- /dev/null +++ b/test-suite/output/DebugFlags.v @@ -0,0 +1,5 @@ +Set Debug "cbn". + +Set Debug "RAKAM". + +Check 2 + 3 = 0. diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index bdb0cabacf..d859fcafe2 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -91,13 +91,14 @@ let remove_ids_and_lets env s ids = let record_proof_using expr = Aux_file.record_in_aux "suggest_proof_using" expr +let debug_proof_using = CDebug.create ~name:"proof-using" () + (* Variables in [skip] come from after the definition, so don't count for "All". Used in the variable case since the env contains the variable itself. *) let suggest_common env ppid used ids_typ skip = let module S = Id.Set in let open Pp in - let print x = Feedback.msg_debug x in let pr_set parens s = let wrap ppcmds = if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")" @@ -111,13 +112,13 @@ let suggest_common env ppid used ids_typ skip = in let all = S.diff all skip in let fwd_typ = close_fwd env (Evd.from_env env) ids_typ in - if !Flags.debug then begin - print (str "All " ++ pr_set false all); - print (str "Type " ++ pr_set false ids_typ); - print (str "needed " ++ pr_set false needed); - print (str "all_needed " ++ pr_set false all_needed); - print (str "Type* " ++ pr_set false fwd_typ); - end; + let () = debug_proof_using (fun () -> + str "All " ++ pr_set false all ++ fnl() ++ + str "Type " ++ pr_set false ids_typ ++ fnl() ++ + str "needed " ++ pr_set false needed ++ fnl() ++ + str "all_needed " ++ pr_set false all_needed ++ fnl() ++ + str "Type* " ++ pr_set false fwd_typ) + in let valid_exprs = ref [] in let valid e = valid_exprs := e :: !valid_exprs in if S.is_empty needed then valid (str "Type"); diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 42ba63903d..c38cfbadc2 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1645,6 +1645,13 @@ let () = optwrite = CWarnings.set_flags } let () = + declare_string_option + { optdepr = false; + optkey = ["Debug"]; + optread = CDebug.get_flags; + optwrite = CDebug.set_flags } + +let () = declare_bool_option { optdepr = false; optkey = ["Guard"; "Checking"]; @@ -1710,9 +1717,9 @@ let vernac_set_append_option ~locality key s = let vernac_set_option ~locality table v = match v with | OptionSetString s -> - (* We make a special case for warnings because appending is their - natural semantics *) - if CString.List.equal table ["Warnings"] then + (* We make a special case for warnings and debug flags because appending is + their natural semantics *) + if CString.List.equal table ["Warnings"] || CString.List.equal table ["Debug"] then vernac_set_append_option ~locality table s else let (last, prefix) = List.sep_last table in |