[glob/aux files] Remove undocumented Stdout dump, cleanup flags.

Fixes #10640

We remove the `StdOut` dump target, so now dump will only happen if a
file is specified. Indeed, we make the default no to dump, and enable
dump only in coqc, moving the option to the `Coqcargs` module.

No need for a changes entry as this feature was undocumented, and no
use case was given when introduced.

Output to feedback must be explicitly enabled by clients / coqidetop,
and we have thus also removed the undocumented option `-feedback-glob`.

7 files changed, 18 insertions, 27 deletions

diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index d8a3dbb4bb..fe5361c156 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -108,8 +108,6 @@ let compile opts copts ~echo ~f_in ~f_out =
   in
   match copts.compilation_mode with
   | BuildVo ->
-      Flags.record_aux_file := true;
-
       let long_f_dot_v, long_f_dot_vo =
         ensure_exists_with_prefix f_in f_out ".v" ".vo" in
 
@@ -124,8 +122,11 @@ let compile opts copts ~echo ~f_in ~f_out =
       Aux_file.(start_aux_file
         ~aux_file:(aux_file_name_for long_f_dot_vo)
         ~v_file:long_f_dot_v);
+
+      Dumpglob.set_glob_output copts.glob_out;
       Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo;
       Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
+
       let wall_clock1 = Unix.gettimeofday () in
       let check = Stm.AsyncOpts.(stm_options.async_proofs_mode = APoff) in
       let state = Vernac.load_vernac ~echo ~check ~interactive:false ~state long_f_dot_v in
@@ -139,9 +140,6 @@ let compile opts copts ~echo ~f_in ~f_out =
       Dumpglob.end_dump_glob ()
 
   | BuildVio ->
-      Flags.record_aux_file := false;
-      Dumpglob.noglob ();
-
       let long_f_dot_v, long_f_dot_vio =
         ensure_exists_with_prefix f_in f_out ".v" ".vio" in
 
@@ -174,9 +172,6 @@ let compile opts copts ~echo ~f_in ~f_out =
       Stm.reset_task_queue ()
 
   | Vio2Vo ->
-
-      Flags.record_aux_file := false;
-      Dumpglob.noglob ();
       let long_f_dot_vio, long_f_dot_vo =
         ensure_exists_with_prefix f_in f_out ".vio" ".vo" in
       let sum, lib, univs, tasks, proofs =
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 67d70416c8..64c1da20b6 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -59,7 +59,6 @@ type coqargs_config = {
   debug       : bool;
   diffs_set   : bool;
   time        : bool;
-  glob_opt    : bool;
   print_emacs : bool;
   set_options : (Goptions.option_name * option_command) list;
 }
@@ -125,7 +124,6 @@ let default_config = {
   debug        = false;
   diffs_set    = false;
   time         = false;
-  glob_opt     = false;
   print_emacs  = false;
   set_options  = [];
 
@@ -380,13 +378,6 @@ let parse_args ~help ~init arglist : t * string list =
       Flags.compat_version := v;
       add_compat_require oval v
 
-    |"-dump-glob" ->
-      Dumpglob.dump_into_file (next ());
-      { oval with config = { oval.config with glob_opt = true }}
-
-    |"-feedback-glob" ->
-      Dumpglob.feedback_glob (); oval
-
     |"-exclude-dir" ->
       System.exclude_directory (next ()); oval
 
@@ -524,7 +515,6 @@ let parse_args ~help ~init arglist : t * string list =
     |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval
     |"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }}
     |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }}
-    |"-no-glob"|"-noglob" -> Dumpglob.noglob (); { oval with config = { oval.config with glob_opt = true }}
     |"-output-context" -> { oval with post = { oval.post with output_context = true }}
     |"-profile-ltac" -> Flags.profile_ltac := true; oval
     |"-q" -> { oval with pre = { oval.pre with load_rcfile = false; }}
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index e414888861..26f22386a0 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -35,7 +35,6 @@ type coqargs_config = {
   debug       : bool;
   diffs_set   : bool;
   time        : bool;
-  glob_opt    : bool;
   print_emacs : bool;
   set_options : (Goptions.option_name * option_command) list;
 }
diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml
index 5678acb2b1..019577ac85 100644
--- a/toplevel/coqc.ml
+++ b/toplevel/coqc.ml
@@ -16,8 +16,7 @@ let outputstate opts =
 let coqc_init _copts ~opts =
   Flags.quiet := true;
   System.trust_file_cache := true;
-  Coqtop.init_color opts.Coqargs.config;
-  if not opts.Coqargs.config.Coqargs.glob_opt then Dumpglob.dump_to_dotglob ()
+  Coqtop.init_color opts.Coqargs.config
 
 let coqc_specific_usage = Usage.{
   executable_name = "coqc";
diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml
index 5cced2baac..0b5481fe72 100644
--- a/toplevel/coqcargs.ml
+++ b/toplevel/coqcargs.ml
@@ -23,7 +23,8 @@ type t =
 
   ; echo : bool
 
-  ; outputstate : string option;
+  ; outputstate : string option
+  ; glob_out    : Dumpglob.glob_output
   }
 
 let default =
@@ -40,6 +41,7 @@ let default =
   ; echo = false
 
   ; outputstate = None
+  ; glob_out = Dumpglob.MultFiles
   }
 
 let depr opt =
@@ -187,6 +189,15 @@ let parse arglist : t =
         | "-outputstate" ->
           set_outputstate oval (next ())
 
+        (* Glob options *)
+        |"-no-glob" | "-noglob" ->
+          { oval with glob_out = Dumpglob.NoGlob }
+
+        |"-dump-glob" ->
+          let file = next () in
+          { oval with glob_out = Dumpglob.File file }
+
+        (* Rest *)
         | s ->
           extras := s :: !extras;
           oval
diff --git a/toplevel/coqcargs.mli b/toplevel/coqcargs.mli
index b02eeeb9ee..13bea3bf3e 100644
--- a/toplevel/coqcargs.mli
+++ b/toplevel/coqcargs.mli
@@ -24,6 +24,7 @@ type t =
   ; echo : bool
 
   ; outputstate : string option
+  ; glob_out    : Dumpglob.glob_output
   }
 
 val default : t
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 78640334e2..07466d641e 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -438,19 +438,15 @@ let rec loop ~state =
       loop ~state
 
 (* Default toplevel loop *)
-let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s))
 
 let drop_args = ref None
+
 let loop ~opts ~state =
   drop_args := Some opts;
   let open Coqargs in
   print_emacs := opts.config.print_emacs;
   (* We initialize the console only if we run the toploop_run *)
   let tl_feed = Feedback.add_feeder coqloop_feed in
-  if Dumpglob.dump () then begin
-    Flags.if_verbose warning "Dumpglob cannot be used in interactive mode.";
-    Dumpglob.noglob ()
-  end;
   let _ = loop ~state in
   (* Initialise and launch the Ocaml toplevel *)
   Coqinit.init_ocaml_path();