Merge PR #9876: Command-line setters for options

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares

17 files changed, 132 insertions, 64 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/ide/idetop.ml b/ide/idetop.ml
index 10b8a2cdc5..543ff924bd 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -57,9 +57,9 @@ let coqide_known_option table = List.mem table [
   ["Diffs"]]
 
 let is_known_option cmd = match Vernacprop.under_control cmd with
-  | VernacSetOption (_, o, BoolValue true)
-  | VernacSetOption (_, o, StringValue _)
-  | VernacUnsetOption (_, o) -> coqide_known_option o
+  | VernacSetOption (_, o, OptionSetTrue)
+  | VernacSetOption (_, o, OptionSetString _)
+  | VernacSetOption (_, o, OptionUnset) -> coqide_known_option o
   | _ -> false
 
 (** Check whether a command is forbidden in the IDE *)
@@ -366,12 +366,13 @@ let get_options () =
   Goptions.OptionMap.fold fold table []
 
 let set_options options =
+  let open Goptions in
   let iter (name, value) = match import_option_value value with
-  | BoolValue b -> Goptions.set_bool_option_value name b
-  | IntValue i -> Goptions.set_int_option_value name i
-  | StringValue s -> Goptions.set_string_option_value name s
-  | StringOptValue (Some s) -> Goptions.set_string_option_value name s
-  | StringOptValue None -> Goptions.unset_option_value_gen name
+  | BoolValue b -> set_bool_option_value name b
+  | IntValue i -> set_int_option_value name i
+  | StringValue s -> set_string_option_value name s
+  | StringOptValue (Some s) -> set_string_option_value name s
+  | StringOptValue None -> unset_option_value_gen name
   in
   List.iter iter options
 
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/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 0a0d9b12fa..bf7f082192 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -183,7 +183,7 @@ GRAMMAR EXTEND Gram
   GLOBAL: gallina_ext;
   gallina_ext:
    [ [ IDENT "Import"; IDENT "Prenex"; IDENT "Implicits" ->
-      { Vernacexpr.VernacUnsetOption (false, ["Printing"; "Implicit"; "Defensive"]) }
+      { Vernacexpr.VernacSetOption (false, ["Printing"; "Implicit"; "Defensive"], Vernacexpr.OptionUnset) }
    ] ]
   ;
 END
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/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 58fe923f9e..243b5c333d 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -57,6 +57,7 @@ let options_affecting_stm_scheduling =
     stm_allow_nested_proofs_option_name;
     Vernacentries.proof_mode_opt_name;
     Attributes.program_mode_option_name;
+    Proof_using.proof_using_opt_name;
   ]
 
 let classify_vernac e =
@@ -64,7 +65,7 @@ let classify_vernac e =
     (* Univ poly compatibility: we run it now, so that we can just
      * look at Flags in stm.ml.  Would be nicer to have the stm
      * look at the entire dag to detect this option. *)
-    | ( VernacSetOption (_, l,_) | VernacUnsetOption (_, l))
+    | VernacSetOption (_, l,_)
       when CList.exists (CList.equal String.equal l)
         options_affecting_stm_scheduling ->
        VtSideff [], VtNow
@@ -91,9 +92,6 @@ let classify_vernac e =
         VtProofStep { parallel = `No;
                       proof_block_detection = Some "curly" },
         VtLater
-    (* Options changing parser *)
-    | VernacUnsetOption (_, ["Default";"Proof";"Using"])
-    | VernacSetOption (_, ["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
     (* StartProof *)
     | VernacDefinition ((Decl_kinds.DoDischarge,_),({v=i},_),ProveBody _) ->
       VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i), VtLater
@@ -156,7 +154,7 @@ let classify_vernac e =
     | VernacReserve _
     | VernacGeneralizable _
     | VernacSetOpacity _ | VernacSetStrategy _
-    | VernacUnsetOption _ | VernacSetOption _
+    | VernacSetOption _
     | VernacAddOption _ | VernacRemoveOption _
     | VernacMemOption _ | VernacPrintOption _
     | VernacGlobalCheck _
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/coqloop.ml b/toplevel/coqloop.ml
index b3de8dd85f..4129562065 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -340,9 +340,7 @@ let print_anyway_opts = [
 let print_anyway c =
   let open Vernacexpr in
   match c with
-  | VernacExpr (_, VernacSetOption (_, opt, _))
-  | VernacExpr (_, VernacUnsetOption (_, opt)) ->
-    List.mem opt print_anyway_opts
+  | VernacExpr (_, VernacSetOption (_, opt, _)) -> List.mem opt print_anyway_opts
   | _ -> false
 
 (* We try to behave better when goal printing raises an exception
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\
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 1533d0ccd3..3f491d1dd4 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -875,10 +875,10 @@ GRAMMAR EXTEND Gram
   GLOBAL: command query_command class_rawexpr gallina_ext;
 
   gallina_ext:
-    [ [ IDENT "Export"; "Set"; table = option_table; v = option_value ->
+    [ [ IDENT "Export"; "Set"; table = option_table; v = option_setting ->
         { VernacSetOption (true, table, v) }
       | IDENT "Export"; IDENT "Unset"; table = option_table ->
-          { VernacUnsetOption (true, table) }
+          { VernacSetOption (true, table, OptionUnset) }
     ] ];
 
   command:
@@ -943,10 +943,10 @@ GRAMMAR EXTEND Gram
 	  { VernacAddMLPath (true, dir) }
 
       (* For acting on parameter tables *)
-      | "Set"; table = option_table; v = option_value ->
+      | "Set"; table = option_table; v = option_setting ->
           { VernacSetOption (false, table, v) }
       | IDENT "Unset"; table = option_table ->
-          { VernacUnsetOption (false, table) }
+          { VernacSetOption (false, table, OptionUnset) }
 
       | IDENT "Print"; IDENT "Table"; table = option_table ->
 	  { VernacPrintOption table }
@@ -1057,10 +1057,10 @@ GRAMMAR EXTEND Gram
       | IDENT "Library"; qid = global -> { LocateLibrary qid }
       | IDENT "Module"; qid = global -> { LocateModule qid } ] ]
   ;
-  option_value:
-    [ [ -> { BoolValue true }
-      | n  = integer   -> { IntValue (Some n) }
-      | s  = STRING    -> { StringValue s } ] ]
+  option_setting:
+    [ [ -> { OptionSetTrue }
+      | n  = integer   -> { OptionSetInt n }
+      | s  = STRING    -> { OptionSetString s } ] ]
   ;
   option_ref_value:
     [ [ id = global   -> { QualidRefValue id }
@@ -1130,10 +1130,10 @@ GRAMMAR EXTEND Gram
 
 (* Tactic Debugger *)
       |	IDENT "Debug"; IDENT "On" ->
-          { VernacSetOption (false, ["Ltac";"Debug"], BoolValue true) }
+          { VernacSetOption (false, ["Ltac";"Debug"], OptionSetTrue) }
 
       |	IDENT "Debug"; IDENT "Off" ->
-          { VernacSetOption (false, ["Ltac";"Debug"], BoolValue false) }
+          { VernacSetOption (false, ["Ltac";"Debug"], OptionUnset) }
 
 (* registration of a custom reduction *)
 
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index b602e134da..4e4d431e89 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -173,15 +173,10 @@ open Pputils
       pr_opt (prlist_with_sep sep pr_option_ref_value) b
 
   let pr_set_option a b =
-    let pr_opt_value = function
-      | IntValue None -> assert false
-    (* This should not happen because of the grammar *)
-      | IntValue (Some n) -> spc() ++ int n
-      | StringValue s -> spc() ++ str s
-      | StringOptValue None -> mt()
-      | StringOptValue (Some s) -> spc() ++ str s
-      | BoolValue b -> mt()
-    in pr_printoption a None ++ pr_opt_value b
+    pr_printoption a None ++ (match b with
+        | OptionUnset | OptionSetTrue -> mt()
+        | OptionSetInt n -> spc() ++ int n
+        | OptionSetString s -> spc() ++ quote (str s))
 
   let pr_opt_hintbases l = match l with
     | [] -> mt()
@@ -1140,15 +1135,11 @@ open Pputils
           hov 1 (keyword "Strategy" ++ spc() ++
                    hv 0 (prlist_with_sep sep pr_line l))
         )
-      | VernacUnsetOption (export, na) ->
-        let export = if export then keyword "Export" ++ spc () else mt () in
-        return (
-          hov 1 (export ++ keyword "Unset" ++ spc() ++ pr_printoption na None)
-        )
       | VernacSetOption (export, na,v) ->
         let export = if export then keyword "Export" ++ spc () else mt () in
+        let set = if v == OptionUnset then "Unset" else "Set" in
         return (
-          hov 2 (export ++ keyword "Set" ++ spc() ++ pr_set_option na v)
+          hov 2 (export ++ keyword set ++ spc() ++ pr_set_option na v)
         )
       | VernacAddOption (na,l) ->
         return (
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index 526845084a..1d089d0a55 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -172,11 +172,12 @@ let value = ref None
 let using_to_string us = Pp.string_of_ppcmds (Ppvernac.pr_using us)
 let using_from_string us = Pcoq.Entry.parse G_vernac.section_subset_expr (Pcoq.Parsable.make (Stream.of_string us))
 
+let proof_using_opt_name = ["Default";"Proof";"Using"]
 let () =
   Goptions.(declare_stringopt_option
     { optdepr  = false;
       optname  = "default value for Proof using";
-      optkey   = ["Default";"Proof";"Using"];
+      optkey   = proof_using_opt_name;
       optread  = (fun () -> Option.map using_to_string !value);
       optwrite = (fun b -> value := Option.map using_from_string b);
     })
diff --git a/vernac/proof_using.mli b/vernac/proof_using.mli
index 7d1110aaa2..702043a4a9 100644
--- a/vernac/proof_using.mli
+++ b/vernac/proof_using.mli
@@ -21,3 +21,6 @@ val suggest_constant : Environ.env -> Names.Constant.t -> unit
 val suggest_variable : Environ.env -> Names.Id.t -> unit
 
 val get_default_proof_using : unit -> Vernacexpr.section_subset_expr option
+
+val proof_using_opt_name : string list
+(** For the stm *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6c24b9ec75..3a305c3b61 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1707,18 +1707,17 @@ let get_option_locality export local =
 let vernac_set_option0 ~local export key opt =
   let locality = get_option_locality export local in
   match opt with
-  | StringValue s -> set_string_option_value_gen ~locality key s
-  | StringOptValue (Some s) -> set_string_option_value_gen ~locality key s
-  | StringOptValue None -> unset_option_value_gen ~locality key
-  | IntValue n -> set_int_option_value_gen ~locality key n
-  | BoolValue b -> set_bool_option_value_gen ~locality key b
+  | OptionUnset -> unset_option_value_gen ~locality key
+  | OptionSetString s -> set_string_option_value_gen ~locality key s
+  | OptionSetInt n -> set_int_option_value_gen ~locality key (Some n)
+  | OptionSetTrue -> set_bool_option_value_gen ~locality key true
 
 let vernac_set_append_option ~local export key s =
   let locality = get_option_locality export local in
   set_string_option_append_value_gen ~locality key s
 
 let vernac_set_option ~local export table v = match v with
-| StringValue s ->
+| OptionSetString s ->
   (* We make a special case for warnings because appending is their
   natural semantics *)
   if CString.List.equal table ["Warnings"] then
@@ -1731,10 +1730,6 @@ let vernac_set_option ~local export table v = match v with
       vernac_set_option0 ~local export table v
 | _ -> vernac_set_option0 ~local export table v
 
-let vernac_unset_option ~local export key =
-  let locality = get_option_locality export local in
-  unset_option_value_gen ~locality key
-
 let vernac_add_option key lv =
   let f = function
     | StringRefValue s -> (get_string_table key)#add s
@@ -2462,9 +2457,6 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
   | VernacSetOption (export, key,v) ->
     vernac_set_option ~local:(only_locality atts) export key v;
     pstate
-  | VernacUnsetOption (export, key) ->
-    vernac_unset_option ~local:(only_locality atts) export key;
-    pstate
   | VernacRemoveOption (key,v) ->
     unsupported_attributes atts;
     vernac_remove_option key v;
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index c8ccd699ac..d0dae1aa53 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -109,11 +109,11 @@ type onlyparsing_flag = Flags.compat_version option
     which this notation is trying to be compatible with *)
 type locality_flag  = bool (* true = Local *)
 
-type option_value = Goptions.option_value =
-  | BoolValue of bool
-  | IntValue of int option
-  | StringValue of string
-  | StringOptValue of string option
+type option_setting =
+  | OptionUnset
+  | OptionSetTrue
+  | OptionSetInt of int
+  | OptionSetString of string
 
 type option_ref_value =
   | StringRefValue of string
@@ -363,8 +363,7 @@ type nonrec vernac_expr =
   | VernacSetOpacity of (Conv_oracle.level * qualid or_by_notation list)
   | VernacSetStrategy of
       (Conv_oracle.level * qualid or_by_notation list) list
-  | VernacUnsetOption of export_flag * Goptions.option_name
-  | VernacSetOption of export_flag * Goptions.option_name * option_value
+  | VernacSetOption of export_flag * Goptions.option_name * option_setting
   | VernacAddOption of Goptions.option_name * option_ref_value list
   | VernacRemoveOption of Goptions.option_name * option_ref_value list
   | VernacMemOption of Goptions.option_name * option_ref_value list