Command-line setters for options

TODO coqproject handling (for now it can be done through -arg I guess)

7 files changed, 86 insertions, 1 deletions

diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index eebf1f11e1..bdda35fcc0 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -210,6 +210,13 @@ and ``coqtop``, unless stated otherwise:
   is intended to be used as a linter for developments that want to be robust to
   changes in the auto-generated name scheme. The options are provided to
   facilitate tracking down problems.
+:-set *string*: Enable flags and set options. *string* should be
+   ``Option Name=value``, the value is interpreted according to the
+   type of the option. For flags ``Option Name`` is equivalent to
+   ``Option Name=true``. For instance ``-set "Universe Polymorphism"``
+   will enable :flag:`Universe Polymorphism`. Note that the quotes are
+   shell syntax, Coq does not see them.
+:-unset *string*: As ``-set`` but used to disable options and flags.
 :-compat *version*: Attempt to maintain some backward-compatibility
   with a previous version.
 :-dump-glob *file*: Dump references for global names in file *file*
diff --git a/library/goptions.mli b/library/goptions.mli
index 9925eb9e7b..2e593e9d9e 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -172,6 +172,14 @@ type option_value =
   | StringValue of string
   | StringOptValue of string option
 
+val set_option_value : ?locality:option_locality ->
+  ('a -> option_value -> option_value) -> option_name -> 'a -> unit
+(** [set_option_value ?locality f name v] sets [name] to the result of
+    applying [f] to [v] and [name]'s current value. Use for behaviour
+    depending on the type of the option, eg erroring when ['a] doesn't
+    match it. Changing the type will result in errors later so don't do
+    that. *)
+
 (** Summary of an option status *)
 type option_state = {
   opt_depr  : bool;
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index d1bd3692ab..2493b1fac4 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -139,7 +139,7 @@ module Make(T : Task) () = struct
         (* We need to pass some options with one argument *)
         | ( "-I" | "-include" | "-top" | "-topfile" | "-coqlib" | "-exclude-dir" | "-compat"
           | "-load-ml-object" | "-load-ml-source" | "-require" | "-w" | "-color" | "-init-file"
-          | "-profile-ltac-cutoff" | "-main-channel" | "-control-channel" | "-mangle-names"
+          | "-profile-ltac-cutoff" | "-main-channel" | "-control-channel" | "-mangle-names" | "-set" | "-unset"
           | "-diffs" | "-mangle-name" | "-dump-glob" | "-bytecode-compiler" | "-native-compiler" as x) :: a :: tl ->
           x :: a :: set_slave_opt tl
         (* We need to pass some options with two arguments *)
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index bf1297d661..319f5c8ad6 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -38,6 +38,8 @@ type color = [`ON | `AUTO | `OFF]
 
 type native_compiler = NativeOff | NativeOn of { ondemand : bool }
 
+type option_command = OptionSet of string option | OptionUnset
+
 type t = {
 
   load_init   : bool;
@@ -63,6 +65,8 @@ type t = {
   allow_sprop : bool;
   cumulative_sprop : bool;
 
+  set_options : (Goptions.option_name * option_command) list;
+
   stm_flags   : Stm.AsyncOpts.stm_opt;
   debug       : bool;
   diffs_set   : bool;
@@ -115,6 +119,8 @@ let default = {
   allow_sprop = false;
   cumulative_sprop = false;
 
+  set_options = [];
+
   stm_flags    = Stm.AsyncOpts.default_opts;
   debug        = false;
   diffs_set    = false;
@@ -245,6 +251,16 @@ let get_native_name s =
       Nativelib.output_dir; Library.native_name_from_filename s]
   with _ -> ""
 
+let to_opt_key = Str.(split (regexp " +"))
+
+let parse_option_set opt =
+  match String.index_opt opt '=' with
+  | None -> to_opt_key opt, None
+  | Some eqi ->
+    let len = String.length opt in
+    let v = String.sub opt (eqi+1) (len - eqi - 1) in
+    to_opt_key (String.sub opt 0 eqi), Some v
+
 (*s Parsing of the command line.
     We no longer use [Arg.parse], in order to use share [Usage.print_usage]
     between coqtop and coqc. *)
@@ -450,6 +466,16 @@ let parse_args ~help ~init arglist : t * string list =
       in
       { oval with native_compiler }
 
+    | "-set" ->
+      let opt = next() in
+      let opt, v = parse_option_set opt in
+      { oval with set_options = (opt, OptionSet v) :: oval.set_options }
+
+    | "-unset" ->
+      let opt = next() in
+      let opt = to_opt_key opt in
+      { oval with set_options = (opt, OptionUnset) :: oval.set_options }
+
     (* Options with zero arg *)
     |"-async-queries-always-delegate"
     |"-async-proofs-always-delegate"
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index 97a62e97e4..9bcfdca332 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -14,6 +14,8 @@ val default_toplevel : Names.DirPath.t
 
 type native_compiler = NativeOff | NativeOn of { ondemand : bool }
 
+type option_command = OptionSet of string option | OptionUnset
+
 type t = {
 
   load_init   : bool;
@@ -38,6 +40,8 @@ type t = {
   allow_sprop : bool;
   cumulative_sprop : bool;
 
+  set_options : (Goptions.option_name * option_command) list;
+
   stm_flags   : Stm.AsyncOpts.stm_opt;
   debug       : bool;
   diffs_set   : bool;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 626023737b..8fae561be8 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -50,6 +50,41 @@ let print_memory_stat () =
 
 let _ = at_exit print_memory_stat
 
+let interp_set_option opt v old =
+  let open Goptions in
+  let err expect =
+    let opt = String.concat " " opt in
+    let got = v in (* avoid colliding with Pp.v *)
+    CErrors.user_err
+      Pp.(str "-set: " ++ str opt ++
+          str" expects " ++ str expect ++
+          str" but got " ++ str got)
+  in
+  match old with
+  | BoolValue _ ->
+    let v = match String.trim v with
+      | "true" -> true
+      | "false" | "" -> false
+      | _ -> err "a boolean"
+    in
+    BoolValue v
+  | IntValue _ ->
+    let v = String.trim v in
+    let v = match int_of_string_opt v with
+      | Some _ as v -> v
+      | None -> if v = "" then None else err "an int"
+    in
+    IntValue v
+  | StringValue _ -> StringValue v
+  | StringOptValue _ -> StringOptValue (Some v)
+
+let set_option = let open Goptions in function
+  | opt, OptionUnset -> unset_option_value_gen ~locality:OptLocal opt
+  | opt, OptionSet None -> set_bool_option_value_gen ~locality:OptLocal opt true
+  | opt, OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v
+
+let set_options = List.iter set_option
+
 (******************************************************************************)
 (* Input/Output State                                                         *)
 (******************************************************************************)
@@ -195,6 +230,8 @@ let init_toplevel ~help ~init custom_init arglist =
   Global.set_allow_sprop opts.allow_sprop;
   if opts.cumulative_sprop then Global.make_sprop_cumulative ();
 
+  set_options opts.set_options;
+
   (* Allow the user to load an arbitrary state here *)
   inputstate opts;
 
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 513374c2af..7074215afe 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -74,6 +74,9 @@ let print_usage_common co command =
 \n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
 \n  -type-in-type          disable universe consistency checking\
 \n  -mangle-names x        mangle auto-generated names using prefix x\
+\n  -set \"Foo Bar\"       enable Foo Bar (as Set Foo Bar. in a file)\
+\n  -set \"Foo Bar=value\" set Foo Bar to value (value is interpreted according to Foo Bar's type)\
+\n  -unset \"Foo Bar\"     disable Foo Bar (as Unset Foo Bar. in a file)\
 \n  -time                  display the time taken by each command\
 \n  -profile-ltac          display the time taken by each (sub)tactic\
 \n  -m, --memory           display total heap size at program exit\