[lib] Move global options to their proper place.

Recent commits introduced global flags, but these should be
module-specific so relocating.

Global flags are deprecated, and for 8.9 `Lib.Flags` will be reduced
to the truly global stuff.

7 files changed, 35 insertions, 26 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 0766f49b3..dfc6ff23f 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -832,6 +832,8 @@ let is_univ_copy max u =
   else
     false
 
+let dump_bytecode = ref false
+
 let dump_bytecodes init code fvs =
   let open Pp in
     (str "code =" ++ fnl () ++
@@ -875,7 +877,7 @@ let compile ~fail_on_error ?universes:(universes=0) env c =
         reloc, init_code
     in
     let fv = List.rev (!(reloc.in_env).fv_rev) in
-    (if !Flags.dump_bytecode then
+    (if !dump_bytecode then
       Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
     Some (init_code,!fun_code, Array.of_list fv)
   with TooLargeInductive msg ->
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index abab58b60..1c4cdcbeb 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -25,3 +25,6 @@ val compile_constant_body : fail_on_error:bool ->
 (** Shortcut of the previous function used during module strengthening *)
 
 val compile_alias : Names.Constant.t -> body_code
+
+(** Dump the bytecode after compilation (for debugging purposes) *)
+val dump_bytecode : bool ref
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index 7b637c20e..641d424e2 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -807,7 +807,7 @@ and lambda_of_args env start args =
 
 
 (*********************************)
-
+let dump_lambda = ref false
 
 let optimize_lambda lam =
   let lam = simplify subst_id lam in
@@ -819,7 +819,7 @@ let lambda_of_constr ~optimize genv c =
   Renv.push_rels env (Array.of_list ids);
   let lam = lambda_of_constr env c in
   let lam = if optimize then optimize_lambda lam else lam in
-  if !Flags.dump_lambda then
+  if !dump_lambda then
     Feedback.msg_debug (pp_lam lam);
   lam
 
diff --git a/kernel/clambda.mli b/kernel/clambda.mli
index 89b7fd8e3..6cf46163e 100644
--- a/kernel/clambda.mli
+++ b/kernel/clambda.mli
@@ -25,3 +25,6 @@ val dynamic_int31_compilation : bool -> lambda array -> lambda
 (*spiwack: compiling function to insert dynamic decompilation before
            matching integers (in case they are in processor representation) *)
 val int31_escape_before_match : bool -> lambda -> lambda
+
+(** Dump the VM lambda code after compilation (for debugging purposes) *)
+val dump_lambda : bool ref
diff --git a/lib/flags.ml b/lib/flags.ml
index 8491873e0..2dbfac0bf 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -160,11 +160,3 @@ let print_mod_uid = ref false
 
 let profile_ltac = ref false
 let profile_ltac_cutoff = ref 2.0
-
-let dump_bytecode = ref false
-let set_dump_bytecode = (:=) dump_bytecode
-let get_dump_bytecode () = !dump_bytecode
-
-let dump_lambda = ref false
-let set_dump_lambda = (:=) dump_lambda
-let get_dump_lambda () = !dump_lambda
diff --git a/lib/flags.mli b/lib/flags.mli
index 85aaf879f..08e862e6c 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -10,6 +10,25 @@
 
 (** Global options of the system. *)
 
+(** WARNING: don't add new entries to this file!
+
+    This file is own its way to deprecation in favor of a purely
+   functional state, but meanwhile it will contain options that are
+   truly global to the system such as [compat] or [debug]
+
+    If you are thinking about adding a global flag, well, just
+   don't. First of all, options make testins exponentially more
+   expensive, due to the growth of flag combinations. So please make
+   some effort in order for your idea to work in a configuration-free
+   manner.
+
+    If you absolutely must pass an option to your new system, then do
+   so as a functional argument so flags are exposed to unit
+   testing. Then, register such parameters with the proper
+   state-handling mechanism of the top-level subsystem of Coq.
+
+ *)
+
 (** Command-line flags  *)
 
 val boot : bool ref
@@ -129,13 +148,3 @@ val print_mod_uid : bool ref
 
 val profile_ltac : bool ref
 val profile_ltac_cutoff : float ref
-
-(** Dump the bytecode after compilation (for debugging purposes) *)
-val dump_bytecode : bool ref
-val set_dump_bytecode : bool -> unit
-val get_dump_bytecode : unit -> bool
-
-(** Dump the VM lambda code after compilation (for debugging purposes) *)
-val dump_lambda : bool ref
-val set_dump_lambda : bool -> unit
-val get_dump_lambda : unit -> bool
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 5dcc170b1..503a22f54 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1468,22 +1468,22 @@ let _ =
       optkey   = ["Printing";"Universes"];
       optread  = (fun () -> !Constrextern.print_universes);
       optwrite = (fun b -> Constrextern.print_universes:=b) }
-     
+
 let _ =
   declare_bool_option
     { optdepr  = false;
       optname  = "dumping bytecode after compilation";
       optkey   = ["Dump";"Bytecode"];
-      optread  = Flags.get_dump_bytecode;
-      optwrite = Flags.set_dump_bytecode }
+      optread  = (fun () -> !Cbytegen.dump_bytecode);
+      optwrite = (:=) Cbytegen.dump_bytecode }
 
 let _ =
   declare_bool_option
     { optdepr  = false;
       optname  = "dumping VM lambda code after compilation";
       optkey   = ["Dump";"Lambda"];
-      optread  = Flags.get_dump_lambda;
-      optwrite = Flags.set_dump_lambda }
+      optread  = (fun () -> !Clambda.dump_lambda);
+      optwrite = (:=) Clambda.dump_lambda }
 
 let _ =
   declare_bool_option