Command-line setters for options

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

4 files changed, 70 insertions, 0 deletions

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\