Merge PR #11851: Process command line load vernaculars before command line Goptions

Reviewed-by: Zimmi48
Reviewed-by: ejgallego

6 files changed, 51 insertions, 39 deletions

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 <https://github.com/coq/coq/pull/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\