From 3e98d9bd37d629f90e0a5702f6deb5b835815b5a Mon Sep 17 00:00:00 2001 From: Lasse Blaauwbroek Date: Tue, 17 Mar 2020 22:59:23 +0100 Subject: Reorder the load/require cmd-options and set/unset cmd-options Make sure that all initial load vernaculars that were specified on the command line are executed before processing the options set through -set on the command line. The reason for this is that the load vernacular options can load plugins that define new Goptions. If these plugins are not loaded before the -set flags are processed, then Goptions will emit a warning that the options of that plugin don't exist and ignore the flag. --- doc/changelog/08-tools/11851-coqc-flags-fix.rst | 6 ++++ doc/sphinx/practical-tools/coq-commands.rst | 5 +++- toplevel/ccompile.ml | 37 ++++++++++++++++++++++++ toplevel/ccompile.mli | 2 ++ toplevel/coqtop.ml | 38 +------------------------ toplevel/usage.ml | 2 +- 6 files changed, 51 insertions(+), 39 deletions(-) create mode 100644 doc/changelog/08-tools/11851-coqc-flags-fix.rst diff --git a/doc/changelog/08-tools/11851-coqc-flags-fix.rst b/doc/changelog/08-tools/11851-coqc-flags-fix.rst new file mode 100644 index 0000000000..a07e48d2d8 --- /dev/null +++ b/doc/changelog/08-tools/11851-coqc-flags-fix.rst @@ -0,0 +1,6 @@ +- **Changed:** + The order in which the require/load flags `-l`, `-ri`, `-re`, `-rfrom`, etc. + and the option set flags `-set`, `-unset` are processed have been reversed. + In the new behavior, require/load flags are processed before option flags. + (`#11851 `_, + by Lasse Blaauwbroek). diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 98d222e317..aa4b6edd7d 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -227,7 +227,10 @@ and ``coqtop``, unless stated otherwise: 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. + shell syntax, Coq does not see them. Flags are processed after initialization + of the document. This includes the `Prelude` if loaded and any libraries loaded + through the `-l`, `-lv`, `-r`, `-re`, `-ri`, `rfrom`, `-refrom` and `-rifrom` + options. :-unset *string*: As ``-set`` but used to disable options and flags. :-compat *version*: Attempt to maintain some backward-compatibility with a previous version. diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index d0d6b8b0a3..a7a9b77b56 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -92,6 +92,41 @@ let create_empty_file filename = let f = open_out filename in close_out f +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 + (* Compile a vernac file *) let compile opts copts ~echo ~f_in ~f_out = let open Vernac.State in @@ -134,6 +169,7 @@ let compile opts copts ~echo ~f_in ~f_out = } in let state = { doc; sid; proof = None; time = opts.config.time } in let state = load_init_vernaculars opts ~state in + set_options opts.config.set_options; let ldir = Stm.get_ldir ~doc:state.doc in Aux_file.(start_aux_file ~aux_file:(aux_file_name_for long_f_dot_out) @@ -187,6 +223,7 @@ let compile opts copts ~echo ~f_in ~f_out = let state = { doc; sid; proof = None; time = opts.config.time } in let state = load_init_vernaculars opts ~state in + set_options opts.config.set_options; let ldir = Stm.get_ldir ~doc:state.doc in let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_in in let doc = Stm.finish ~doc:state.doc in diff --git a/toplevel/ccompile.mli b/toplevel/ccompile.mli index 8c154488d0..eb66dbaafc 100644 --- a/toplevel/ccompile.mli +++ b/toplevel/ccompile.mli @@ -17,3 +17,5 @@ val compile_files : Coqargs.t -> Coqcargs.t -> unit (** [do_vio opts] process [.vio] files in [opts] *) val do_vio : Coqargs.t -> Coqcargs.t -> unit + +val set_options : (Goptions.option_name * Coqargs.option_command) list -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 8d9b9411dd..a63cff3e6f 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -46,41 +46,6 @@ let print_memory_stat () = close_out oc with _ -> () -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 *) (******************************************************************************) @@ -236,8 +201,6 @@ let init_execution opts custom_init = Global.set_allow_sprop opts.config.logic.allow_sprop; if opts.config.logic.cumulative_sprop then Global.make_sprop_cumulative (); - set_options opts.config.set_options; - (* Native output dir *) Nativelib.output_dir := opts.config.native_output_dir; Nativelib.include_dirs := opts.config.native_include_dirs; @@ -311,6 +274,7 @@ type run_mode = Interactive | Batch let init_toploop opts = let state = init_document opts in let state = Ccompile.load_init_vernaculars opts ~state in + Ccompile.set_options opts.config.set_options; state let coqtop_init run_mode ~opts = diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 8fc1e03589..e69b21a195 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -41,7 +41,7 @@ let print_usage_common co command = \n -l f (idem)\ \n -load-vernac-source-verbose f load Coq file f.v (Load Verbose \"f\".)\ \n -lv f (idem)\ -\n -load-vernac-object lib, -r lib\ +\n -load-vernac-object lib\ \n load Coq library lib (Require lib)\ \n -rfrom root lib load Coq library lib (From root Require lib.)\ \n -require-import lib, -ri lib\ -- cgit v1.2.3