Merge PR #10612: Fix feedback levels

Ack-by: ejgallego
Reviewed-by: gares

19 files changed, 65 insertions, 75 deletions

diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index e3a5676942..3c383b2e00 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -107,7 +107,7 @@ struct
       Util.iraise (Exception e, info)
 
   (** Use the current logger. The buffer is also flushed. *)
-  let print_debug   s = make (fun _ -> Feedback.msg_info s)
+  let print_debug   s = make (fun _ -> Feedback.msg_debug s)
   let print_info    s = make (fun _ -> Feedback.msg_info s)
   let print_warning s = make (fun _ -> Feedback.msg_warning s)
   let print_notice  s = make (fun _ -> Feedback.msg_notice s)
diff --git a/lib/feedback.mli b/lib/feedback.mli
index dc8449ed71..5375d97d57 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -74,13 +74,8 @@ val feedback : ?did:doc_id -> ?id:Stateid.t -> ?route:route_id -> feedback_conte
 (** [set_id_for_feedback route id] Set the defaults for feedback *)
 val set_id_for_feedback : ?route:route_id -> doc_id -> Stateid.t -> unit
 
-(** {6 output functions}
+(** {6 output functions} *)
 
-[msg_notice] do not put any decoration on output by default. If
-possible don't mix it with goal output (prefer msg_info or
-msg_warning) so that interfaces can dispatch outputs easily. Once all
-interfaces use the xml-like protocol this constraint can be
-relaxed. *)
 (* Should we advertise these functions more? Should they be the ONLY
    allowed way to output something? *)
 
diff --git a/lib/system.ml b/lib/system.ml
index b1a9efccfc..8c333ec267 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -300,13 +300,13 @@ let with_time ~batch ~header f x =
     let y = f x in
     let tend = get_time() in
     let msg2 = if batch then "" else " (successful)" in
-    Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2);
+    Feedback.msg_notice (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2);
     y
   with e ->
     let tend = get_time() in
     let msg = if batch then "" else "Finished failing transaction in " in
     let msg2 = if batch then "" else " (failure)" in
-    Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2);
+    Feedback.msg_notice (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2);
     raise e
 
 (* We use argv.[0] as we don't want to resolve symlinks *)
diff --git a/library/goptions.ml b/library/goptions.ml
index c7024ca81d..0973944fb5 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -398,9 +398,9 @@ let print_option_value key =
   let s = read () in
   match s with
     | BoolValue b ->
-	Feedback.msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off"))
+        Feedback.msg_notice (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off"))
     | _ ->
-	Feedback.msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s))
+        Feedback.msg_notice (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s))
 
 let get_tables () =
   let tables = !value_tab in
diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index de23f05a9e..7f0d768d3f 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -436,7 +436,7 @@ let comment_stop ep =
     let bp = match !comment_begin with
         Some bp -> bp
       | None ->
-          Feedback.msg_notice
+          Feedback.msg_debug
             (str "No begin location for comment '"
              ++ str current_s ++str"' ending at  "
              ++ int ep);
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 3ed843649e..b5be1cdd89 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -437,30 +437,25 @@ let cc_tactic depth additionnal_terms =
 	    let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
 	    discriminate_tac cstr p
 	| Incomplete ->
-            let open Glob_term in
-            let env = Proofview.Goal.env gl in
-            let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in
-            let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) in
-            let pr_missing (c, missing) =
-              let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in
-              let holes = List.init missing (fun _ -> hole) in
-              Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes))
-            in
-	    Feedback.msg_info
-	      (Pp.str "Goal is solvable by congruence but some arguments are missing.");
-	    Feedback.msg_info
-	      (Pp.str "  Try " ++
-		 hov 8
-		 begin
-		   str "\"congruence with (" ++
-		     prlist_with_sep
-		     (fun () -> str ")" ++ spc () ++ str "(")
-		     pr_missing
-		     terms_to_complete ++
-		     str ")\","
-		 end ++
-		 Pp.str "  replacing metavariables by arbitrary terms.");
-	    Tacticals.New.tclFAIL 0 (str "Incomplete")
+      let open Glob_term in
+      let env = Proofview.Goal.env gl in
+      let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in
+      let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) in
+      let pr_missing (c, missing) =
+        let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in
+        let holes = List.init missing (fun _ -> hole) in
+        Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes))
+      in
+            let msg = Pp.(str "Goal is solvable by congruence but some arguments are missing."
+                    ++ fnl () ++
+                    str "  Try " ++
+                    hov 8
+                    begin
+                      str "\"congruence with (" ++ prlist_with_sep (fun () -> str ")" ++ spc () ++ str "(")
+                      pr_missing terms_to_complete ++ str ")\","
+                    end ++
+                    str "  replacing metavariables by arbitrary terms.") in
+      Tacticals.New.tclFAIL 0 msg
 	| Contradiction dis ->
       let env = Proofview.Goal.env gl in
             let p=build_proof env sigma uf (`Prove (dis.lhs,dis.rhs)) in
diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg
index e222fbc808..4f077b08b6 100644
--- a/plugins/extraction/g_extraction.mlg
+++ b/plugins/extraction/g_extraction.mlg
@@ -128,7 +128,7 @@ END
 
 VERNAC COMMAND EXTEND PrintExtractionInline CLASSIFIED AS QUERY
 | [ "Print" "Extraction" "Inline" ]
-  -> {Feedback. msg_info (print_extraction_inline ()) }
+  -> {Feedback.msg_notice (print_extraction_inline ()) }
 END
 
 VERNAC COMMAND EXTEND ResetExtractionInline CLASSIFIED AS SIDEFF
@@ -150,7 +150,7 @@ END
 
 VERNAC COMMAND EXTEND PrintExtractionBlacklist CLASSIFIED AS QUERY
 | [ "Print" "Extraction" "Blacklist" ]
-  -> { Feedback.msg_info (print_extraction_blacklist ()) }
+  -> { Feedback.msg_notice (print_extraction_blacklist ()) }
 END
 
 VERNAC COMMAND EXTEND ResetExtractionBlacklist CLASSIFIED AS SIDEFF
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index 8a5c32b8b5..35cd10a1ff 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -83,7 +83,7 @@ END
 
 VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY
 | [ "Print" "Firstorder" "Solver" ] -> {
-    Feedback.msg_info
+    Feedback.msg_notice
       (Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) }
 END
 
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 21d61d1f97..f7215a9d13 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -1100,7 +1100,7 @@ VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF
 END
 
 VERNAC COMMAND EXTEND Print_keys CLASSIFIED AS QUERY
-| [ "Print" "Equivalent" "Keys" ] -> { Feedback.msg_info (Keys.pr_keys Printer.pr_global) }
+| [ "Print" "Equivalent" "Keys" ] -> { Feedback.msg_notice (Keys.pr_keys Printer.pr_global) }
 END
 
 
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index 455c8ab003..61cc77c42a 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -145,7 +145,7 @@ open Pp
 
 VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY
 | [ "Show" "Obligation" "Tactic" ] -> {
-    Feedback.msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) }
+    Feedback.msg_notice (str"Program obligation tactic is " ++ print_default_tactic ()) }
 END
 
 VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY
@@ -154,8 +154,8 @@ VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY
 END
 
 VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY
-| [ "Preterm" "of" ident(name) ] -> { Feedback.msg_info (show_term (Some name)) }
-| [ "Preterm" ] -> { Feedback.msg_info (show_term None) }
+| [ "Preterm" "of" ident(name) ] -> { Feedback.msg_notice (show_term (Some name)) }
+| [ "Preterm" ] -> { Feedback.msg_notice (show_term None) }
 END
 
 {
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 9d46bbc74e..fe5ebf1172 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -417,7 +417,7 @@ let get_timer name =
 let finish_timing ~prefix name =
   let tend = System.get_time () in
   let tstart = get_timer name in
-  Feedback.msg_info(str prefix ++ pr_opt str name ++ str " ran for " ++
+  Feedback.msg_notice(str prefix ++ pr_opt str name ++ str " ran for " ++
                     System.fmt_time_difference tstart tend)
 
 (* ******************** *)
@@ -431,7 +431,7 @@ let print_results_filter ~cutoff ~filter =
   let results =
     SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in
   let results = merge_roots results Local.(CList.last !stack) in
-  Feedback.msg_info (to_string ~cutoff ~filter results)
+  Feedback.msg_notice (to_string ~cutoff ~filter results)
 ;;
 
 let print_results ~cutoff =
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index f3f1d713e9..064ea0a3e3 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -279,7 +279,7 @@ let interp_search_notation ?loc tag okey =
       Feedback.msg_warning (hov 4 (qtag "In" ++ str "also occurs in " ++ pr_ntns'))
     end; ntn
   | [ntn] ->
-    Feedback.msg_info (hov 4 (qtag "In" ++ str "is part of notation " ++ pr_ntn ntn)); ntn
+    Feedback.msg_notice (hov 4 (qtag "In" ++ str "is part of notation " ++ pr_ntn ntn)); ntn
   | ntns' ->
     let e = str "occurs in" ++ spc() ++ pr_and_list pr_ntn ntns' in
     err (hov 4 (str "ambiguous: " ++ qtag "in" ++ e)) in
@@ -297,7 +297,7 @@ let interp_search_notation ?loc tag okey =
     let rbody = glob_constr_of_notation_constr ?loc body in
     let m_body = hov 0 (Constrextern.without_symbols prl_glob_constr rbody) in
     let m = m_sc ++ pr_ntn ntn_pat ++ spc () ++ str "denotes " ++ m_body in
-    Feedback.msg_info (hov 0 m) in
+    Feedback.msg_notice (hov 0 m) in
   if List.length !scs > 1 then
     let scs' = List.remove (=) sc !scs in
     let w = pr_ntn ntn ++ str " is also defined " ++ pr_scs scs' in
@@ -464,7 +464,7 @@ let interp_modloc mr =
 
 let ssrdisplaysearch gr env t =
   let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env Evd.empty t in
-  Feedback.msg_info (hov 2 pr_res ++ fnl ())
+  Feedback.msg_notice (hov 2 pr_res ++ fnl ())
 
 }
 
@@ -559,7 +559,7 @@ END
 let print_view_hints env sigma kind l =
   let pp_viewname = str "Hint View" ++ pr_viewpos (Some kind) ++ str " " in
   let pp_hints = pr_list spc (pr_rawhintref env sigma) l in
-  Feedback.msg_info  (pp_viewname ++ hov 0 pp_hints ++ Pp.cut ())
+  Feedback.msg_notice  (pp_viewname ++ hov 0 pp_hints ++ Pp.cut ())
 
 }
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index be21a3a60d..288a349b8b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -773,7 +773,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
   (* Evar must be undefined since we have flushed evars *)
   let () = if !debug_unification then
 	     let open Pp in
-             Feedback.msg_notice (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in
+             Feedback.msg_debug (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) ->
@@ -1569,7 +1569,7 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
   let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in
   let () = if !debug_unification then
 	     let open Pp in
-             Feedback.msg_notice (v 0 (str "Heuristic:" ++ spc () ++
+             Feedback.msg_debug (v 0 (str "Heuristic:" ++ spc () ++
                                 Termops.Internal.print_constr_env env evd t1 ++ cut () ++
                                 Termops.Internal.print_constr_env env evd t2 ++ cut ())) in
   let app_empty = Array.is_empty l1 && Array.is_empty l2 in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 7362955eb7..df161b747a 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -918,7 +918,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
     let () = if !debug_RAKAM then
 	let open Pp in
         let pr c = Termops.Internal.print_constr_env env sigma c in
-	Feedback.msg_notice
+        Feedback.msg_debug
              (h 0 (str "<<" ++ pr x ++
                    str "|" ++ cut () ++ Cst_stack.pr env sigma cst_l ++
 		   str "|" ++ cut () ++ Stack.pr pr stack ++
@@ -927,7 +927,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
     let c0 = EConstr.kind sigma x in
     let fold () =
       let () = if !debug_RAKAM then
-	  let open Pp in Feedback.msg_notice (str "<><><><><>") in
+          let open Pp in Feedback.msg_debug (str "<><><><><>") in
       ((EConstr.of_kind c0, stack),cst_l)
     in
     match c0 with
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 67f49f0074..0b465418f2 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -220,13 +220,13 @@ let tclLOG (dbg,_,depth,trace) pp tac =
           tac >>= fun v ->
           tclENV >>= fun env ->
           tclEVARMAP >>= fun sigma ->
-          Feedback.msg_debug (str s ++ spc () ++ pp env sigma ++ str ". (*success*)");
+          Feedback.msg_notice (str s ++ spc () ++ pp env sigma ++ str ". (*success*)");
           tclUNIT v
         ) tclUNIT
           (fun (exn, info) ->
              tclENV >>= fun env ->
              tclEVARMAP >>= fun sigma ->
-             Feedback.msg_debug (str s ++ spc () ++ pp env sigma ++ str ". (*fail*)");
+             Feedback.msg_notice (str s ++ spc () ++ pp env sigma ++ str ". (*fail*)");
              tclZERO ~info exn))
     | Info ->
       (* For "info (trivial/auto)", we store a log trace *)
@@ -260,19 +260,19 @@ let pr_info_atom env sigma (d,pp) =
 
 let pr_info_trace env sigma = function
   | (Info,_,_,{contents=(d,Some pp)::l}) ->
-    Feedback.msg_info (prlist_with_sep fnl (pr_info_atom env sigma) (cleanup_info_trace d [(d,pp)] l))
+    Feedback.msg_notice (prlist_with_sep fnl (pr_info_atom env sigma) (cleanup_info_trace d [(d,pp)] l))
   | _ -> ()
 
 let pr_info_nop = function
-  | (Info,_,_,_) -> Feedback.msg_info (str "idtac.")
+  | (Info,_,_,_) -> Feedback.msg_notice (str "idtac.")
   | _ -> ()
 
 let pr_dbg_header = function
   | (Off,_,_,_) -> ()
-  | (Debug,ReportForTrivial,_,_) -> Feedback.msg_debug (str "(* debug trivial: *)")
-  | (Debug,ReportForAuto,_,_) -> Feedback.msg_debug (str "(* debug auto: *)")
-  | (Info,ReportForTrivial,_,_) -> Feedback.msg_info (str "(* info trivial: *)")
-  | (Info,ReportForAuto,_,_) -> Feedback.msg_info (str "(* info auto: *)")
+  | (Debug,ReportForTrivial,_,_) -> Feedback.msg_notice (str "(* debug trivial: *)")
+  | (Debug,ReportForAuto,_,_) -> Feedback.msg_notice (str "(* debug auto: *)")
+  | (Info,ReportForTrivial,_,_) -> Feedback.msg_notice (str "(* info trivial: *)")
+  | (Info,ReportForAuto,_,_) -> Feedback.msg_notice (str "(* info auto: *)")
 
 let tclTRY_dbg d tac =
   let delay f = Proofview.tclUNIT () >>= fun () -> f () in
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index d4e4322bef..2ce32b309a 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -351,13 +351,13 @@ let mk_eauto_dbg d =
   else Off
 
 let pr_info_nop = function
-  | Info -> Feedback.msg_info (str "idtac.")
+  | Info -> Feedback.msg_notice (str "idtac.")
   | _ -> ()
 
 let pr_dbg_header = function
   | Off -> ()
-  | Debug -> Feedback.msg_debug (str "(* debug eauto: *)")
-  | Info  -> Feedback.msg_info (str "(* info eauto: *)")
+  | Debug -> Feedback.msg_notice (str "(* debug eauto: *)")
+  | Info  -> Feedback.msg_notice (str "(* info eauto: *)")
 
 let pr_info dbg s =
   if dbg != Info then ()
@@ -368,7 +368,7 @@ let pr_info dbg s =
 	| State sp ->
 	  let mindepth = loop sp in
 	  let indent = String.make (mindepth - sp.depth) ' ' in
-	  Feedback.msg_info (str indent ++ Lazy.force s.last_tactic ++ str ".");
+          Feedback.msg_notice (str indent ++ Lazy.force s.last_tactic ++ str ".");
 	  mindepth
     in
     ignore (loop s)
diff --git a/test-suite/output/auto.out b/test-suite/output/auto.out
index 2761b87b02..5e81b43504 100644
--- a/test-suite/output/auto.out
+++ b/test-suite/output/auto.out
@@ -2,18 +2,18 @@
 simple apply or_intror (in core).
  intro.
  assumption.
-Debug: (* debug auto: *)
-Debug: * assumption. (*fail*)
-Debug: * intro. (*fail*)
-Debug: * simple apply or_intror (in core). (*success*)
-Debug: ** assumption. (*fail*)
-Debug: ** intro. (*success*)
-Debug: ** assumption. (*success*)
+(* debug auto: *)
+* assumption. (*fail*)
+* intro. (*fail*)
+* simple apply or_intror (in core). (*success*)
+** assumption. (*fail*)
+** intro. (*success*)
+** assumption. (*success*)
 (* info eauto: *)
 simple apply or_intror.
  intro.
  exact H.
-Debug: (* debug eauto: *)
+(* debug eauto: *)
 Debug: 1 depth=5 
 Debug: 1.1 depth=4 simple apply or_intror
 Debug: 1.1.1 depth=4 intro
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 33a95e7b30..eded9f4bcd 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -30,7 +30,7 @@ let get_version_date () =
 
 let print_header () =
   let (ver,rev) = get_version_date () in
-  Feedback.msg_notice (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")");
+  Feedback.msg_info (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")");
   flush_all ()
 
 let print_memory_stat () =
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 90b7610750..3d14e8d510 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2285,7 +2285,7 @@ let with_fail ~st f =
     user_err ~hdr:"Fail" (str "The command has not failed!")
   | Ok msg ->
     if not !Flags.quiet || !test_mode
-    then Feedback.msg_info (str "The command has indeed failed with message:" ++ fnl () ++ msg)
+    then Feedback.msg_notice (str "The command has indeed failed with message:" ++ fnl () ++ msg)
 
 let locate_if_not_already ?loc (e, info) =
   match Loc.get_loc info with