diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-04-30 09:25:44 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-04-30 09:25:44 +0200 |
| commit | 8c3d9eb165b456fc83753624efe6708832e9b52f (patch) | |
| tree | f0c7050b1b2fcaa63167e8830c535d1dde982f35 /lib | |
| parent | 14226761af6525c9848f3626cd86b0d4e47dad4d (diff) | |
| parent | ce9b17821a3be3dee7fa7e49c35edaefc658b965 (diff) | |
Merge PR #6958: [lib] Move global options to their proper place.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/flags.ml | 8 | ||||
| -rw-r--r-- | lib/flags.mli | 29 |
2 files changed, 19 insertions, 18 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index 2a1c50f52..56940f1cf 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -159,11 +159,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 53a69f356..17776d68a 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 @@ -126,13 +145,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 |